CBMC
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
SET_RETURN_VALUE
:
44
case
OTHER
:
45
case
ASSIGN
:
46
value_set
.
apply_code
(from_l->code(), ns);
47
break
;
48
49
case
FUNCTION_CALL
:
50
value_set
.
do_function_call
(function_to, from_l->call_arguments(), ns);
51
break
;
52
53
case
CATCH
:
54
case
THROW
:
55
case
DECL
:
56
case
DEAD
:
57
case
ATOMIC_BEGIN
:
58
case
ATOMIC_END
:
59
case
START_THREAD
:
60
case
END_THREAD
:
61
case
LOCATION
:
62
case
SKIP
:
63
case
ASSERT
:
64
case
ASSUME
:
65
case
INCOMPLETE_GOTO
:
66
case
NO_INSTRUCTION_TYPE
:
67
// do nothing
68
break
;
69
}
70
71
return
(
value_set
.
changed
);
72
}
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:36
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition:
goto_program.h:45
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:1276
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:31
coverage_criteriont::ASSUME
@ ASSUME
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:90
THROW
@ THROW
Definition:
goto_program.h:50
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:1338
value_set_fit::changed
bool changed
Definition:
value_set_fi.h:260
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
flow_insensitive_analysis.h:44
value_set_domain_fi.h
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
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:1325
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
src
pointer-analysis
value_set_domain_fi.cpp
Generated by
1.8.17