cprover
value_set_domain_fivrns.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Value Set Domain (Flow Insensitive, Validity Regions)
4
5
Author: Daniel Kroening, kroening@kroening.com
6
CM Wintersteiger
7
8
\*******************************************************************/
9
12
13
#include "
value_set_domain_fivrns.h
"
14
15
#include <
util/std_code.h
>
16
17
bool
value_set_domain_fivrnst::transform
(
18
const
namespacet
&ns,
19
locationt
from_l,
20
locationt
to_l)
21
{
22
value_set
.
set_from
(from_l->function, from_l->location_number);
23
value_set
.
set_to
(to_l->function, to_l->location_number);
24
25
#if 0
26
std::cout <<
"Transforming: "
<<
27
from_l->function <<
" "
<< from_l->location_number <<
" to "
<<
28
to_l->function <<
" "
<< to_l->location_number <<
'\n'
;
29
#endif
30
31
switch
(from_l->type)
32
{
33
case
END_FUNCTION
:
34
value_set
.
do_end_function
(
get_return_lhs
(to_l), ns);
35
break
;
36
37
case
RETURN
:
38
case
OTHER
:
39
case
ASSIGN
:
40
value_set
.
apply_code
(from_l->code, ns);
41
break
;
42
43
case
FUNCTION_CALL
:
44
{
45
const
code_function_callt
&code=
46
to_code_function_call
(from_l->code);
47
48
value_set
.
do_function_call
(to_l->function, code.
arguments
(), ns);
49
break
;
50
}
51
52
default
:
53
{
54
}
55
}
56
57
return
value_set
.
handover
();
58
}
value_set_domain_fivrnst::value_set
value_set_fivrnst value_set
Definition:
value_set_domain_fivrns.h:24
value_set_fivrnst::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition:
value_set_fivrns.cpp:1063
value_set_fivrnst::apply_code
void apply_code(const exprt &code, const namespacet &ns)
Definition:
value_set_fivrns.cpp:1144
END_FUNCTION
Definition:
goto_program.h:42
value_set_domain_fivrns.h
Value Set Domain (Flow Insensitive, Validity Regions)
value_set_fivrnst::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition:
value_set_fivrns.h:46
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition:
std_code.h:1109
RETURN
Definition:
goto_program.h:45
value_set_fivrnst::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition:
value_set_fivrns.cpp:1129
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
code_function_callt
codet representation of a function call statement.
Definition:
std_code.h:1036
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
flow_insensitive_analysis.h:44
value_set_domain_fivrnst::transform
virtual bool transform(const namespacet &ns, locationt from_l, locationt to_l)
Definition:
value_set_domain_fivrns.cpp:17
ASSIGN
Definition:
goto_program.h:46
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition:
flow_insensitive_analysis.cpp:37
FUNCTION_CALL
Definition:
goto_program.h:49
value_set_fivrnst::handover
bool handover()
Definition:
value_set_fivrns.cpp:1412
OTHER
Definition:
goto_program.h:37
value_set_fivrnst::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition:
value_set_fivrns.h:40
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition:
std_code.h:1173
pointer-analysis
value_set_domain_fivrns.cpp
Generated by
1.8.15