cprover
value_set_domain_fi.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Value Set Domain (Flow Insensitive)
4
5
Author: Daniel Kroening, kroening@kroening.com
6
CM Wintersteiger
7
8
\*******************************************************************/
9
12
13
#include "
value_set_domain_fi.h
"
14
15
#include <
util/std_code.h
>
16
17
bool
value_set_domain_fit::transform
(
18
const
namespacet
&ns,
19
locationt
from_l,
20
locationt
to_l)
21
{
22
value_set
.
changed
=
false
;
23
24
value_set
.
set_from
(from_l->function, from_l->location_number);
25
value_set
.
set_to
(to_l->function, to_l->location_number);
26
27
// std::cout << "transforming: " <<
28
// from_l->function << " " << from_l->location_number << " to " <<
29
// to_l->function << " " << to_l->location_number << '\n';
30
31
switch
(from_l->type)
32
{
33
case
GOTO
:
34
// ignore for now
35
break
;
36
37
case
END_FUNCTION
:
38
value_set
.
do_end_function
(
get_return_lhs
(to_l), ns);
39
break
;
40
41
case
RETURN
:
42
case
OTHER
:
43
case
ASSIGN
:
44
value_set
.
apply_code
(from_l->code, ns);
45
break
;
46
47
case
FUNCTION_CALL
:
48
{
49
const
code_function_callt
&code=
50
to_code_function_call
(from_l->code);
51
52
value_set
.
do_function_call
(to_l->function, code.
arguments
(), ns);
53
}
54
break
;
55
56
default
:
57
{
58
// do nothing
59
}
60
}
61
62
return
(
value_set
.
changed
);
63
}
value_set_fit::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition:
value_set_fi.h:42
END_FUNCTION
Definition:
goto_program.h:40
value_set_fit::apply_code
void apply_code(const exprt &code, const namespacet &ns)
Definition:
value_set_fi.cpp:1409
std_code.h
value_set_fit::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition:
value_set_fi.h:48
code_function_callt::arguments
argumentst & arguments()
Definition:
std_code.h:890
RETURN
Definition:
goto_program.h:43
value_set_domain_fi.h
Value Set (Flow Insensitive)
value_set_fit::changed
bool changed
Definition:
value_set_fi.h:265
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:74
value_set_fit::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition:
value_set_fi.cpp:1347
code_function_callt
A function call.
Definition:
std_code.h:858
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
flow_insensitive_analysis.h:33
value_set_domain_fit::value_set
value_set_fit value_set
Definition:
value_set_domain_fi.h:23
value_set_fit::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition:
value_set_fi.cpp:1396
ASSIGN
Definition:
goto_program.h:44
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition:
flow_insensitive_analysis.cpp:40
FUNCTION_CALL
Definition:
goto_program.h:47
value_set_domain_fit::transform
virtual bool transform(const namespacet &ns, locationt from_l, locationt to_l)
Definition:
value_set_domain_fi.cpp:17
OTHER
Definition:
goto_program.h:35
GOTO
Definition:
goto_program.h:32
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition:
std_code.h:909
pointer-analysis
value_set_domain_fi.cpp
Generated by
1.8.14