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
const
irep_idt
&function_from,
20
locationt
from_l,
21
const
irep_idt
&function_to,
22
locationt
to_l)
23
{
24
value_set
.
changed
=
false
;
25
26
value_set
.
set_from
(function_from, from_l->location_number);
27
value_set
.
set_to
(function_to, to_l->location_number);
28
29
// std::cout << "transforming: " <<
30
// from_l->function << " " << from_l->location_number << " to " <<
31
// to_l->function << " " << to_l->location_number << '\n';
32
33
switch
(from_l->type)
34
{
35
case
GOTO
:
36
// ignore for now
37
break
;
38
39
case
END_FUNCTION
:
40
value_set
.
do_end_function
(
get_return_lhs
(to_l), ns);
41
break
;
42
43
case
RETURN
:
44
case
OTHER
:
45
case
ASSIGN
:
46
value_set
.
apply_code
(from_l->code, ns);
47
break
;
48
49
case
FUNCTION_CALL
:
50
{
51
const
code_function_callt
&code = from_l->get_function_call();
52
53
value_set
.
do_function_call
(function_to, code.
arguments
(), ns);
54
break
;
55
}
56
57
case
CATCH
:
58
case
THROW
:
59
case
DECL
:
60
case
DEAD
:
61
case
ATOMIC_BEGIN
:
62
case
ATOMIC_END
:
63
case
START_THREAD
:
64
case
END_THREAD
:
65
case
LOCATION
:
66
case
SKIP
:
67
case
ASSERT
:
68
case
ASSUME
:
69
case
INCOMPLETE_GOTO
:
70
case
NO_INSTRUCTION_TYPE
:
71
// do nothing
72
break
;
73
}
74
75
return
(
value_set
.
changed
);
76
}
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
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:1264
value_set_domain_fit::value_set
value_set_fit value_set
Definition:
value_set_domain_fi.h:23
value_set_domain_fit::transform
bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
Definition:
value_set_domain_fi.cpp:17
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition:
flow_insensitive_analysis.cpp:33
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
THROW
@ THROW
Definition:
goto_program.h:50
code_function_callt
codet representation of a function call statement.
Definition:
std_code.h:1183
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition:
goto_program.h:34
value_set_fit::apply_code
void apply_code(const codet &code, const namespacet &ns)
Definition:
value_set_fi.cpp:1326
value_set_fit::changed
bool changed
Definition:
value_set_fi.h:266
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
flow_insensitive_analysis.h:44
value_set_domain_fi.h
Value Set (Flow Insensitive)
value_set_fit::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition:
value_set_fi.h:44
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition:
goto_program.h:33
OTHER
@ OTHER
Definition:
goto_program.h:37
END_FUNCTION
@ END_FUNCTION
Definition:
goto_program.h:42
SKIP
@ SKIP
Definition:
goto_program.h:38
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition:
std_code.h:1228
RETURN
@ RETURN
Definition:
goto_program.h:45
ASSIGN
@ ASSIGN
Definition:
goto_program.h:46
CATCH
@ CATCH
Definition:
goto_program.h:51
DECL
@ DECL
Definition:
goto_program.h:47
value_set_fit::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition:
value_set_fi.cpp:1313
ASSUME
@ ASSUME
Definition:
goto_program.h:35
START_THREAD
@ START_THREAD
Definition:
goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition:
goto_program.h:49
ATOMIC_END
@ ATOMIC_END
Definition:
goto_program.h:44
DEAD
@ DEAD
Definition:
goto_program.h:48
value_set_fit::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition:
value_set_fi.h:50
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition:
goto_program.h:43
ASSERT
@ ASSERT
Definition:
goto_program.h:36
END_THREAD
@ END_THREAD
Definition:
goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition:
goto_program.h:52
pointer-analysis
value_set_domain_fi.cpp
Generated by
1.8.20