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
bool
value_set_domain_fit::transform
(
16
const
namespacet
&ns,
17
const
irep_idt
&function_from,
18
locationt
from_l,
19
const
irep_idt
&function_to,
20
locationt
to_l)
21
{
22
value_set
.
changed
=
false
;
23
24
value_set
.
set_from
(function_from, from_l->location_number);
25
value_set
.
set_to
(function_to, 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
SET_RETURN_VALUE
:
42
case
OTHER
:
43
case
ASSIGN
:
44
value_set
.
apply_code
(from_l->code(), ns);
45
break
;
46
47
case
FUNCTION_CALL
:
48
value_set
.
do_function_call
(function_to, from_l->call_arguments(), ns);
49
break
;
50
51
case
CATCH
:
52
case
THROW
:
53
case
DECL
:
54
case
DEAD
:
55
case
ATOMIC_BEGIN
:
56
case
ATOMIC_END
:
57
case
START_THREAD
:
58
case
END_THREAD
:
59
case
LOCATION
:
60
case
SKIP
:
61
case
ASSERT
:
62
case
ASSUME
:
63
case
INCOMPLETE_GOTO
:
64
case
NO_INSTRUCTION_TYPE
:
65
// do nothing
66
break
;
67
}
68
69
return
(
value_set
.
changed
);
70
}
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:38
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition:
flow_insensitive_analysis.cpp:31
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
flow_insensitive_analysis.h:44
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:94
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:15
value_set_domain_fit::value_set
value_set_fit value_set
Definition:
value_set_domain_fi.h:23
value_set_fit::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition:
value_set_fi.h:44
value_set_fit::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition:
value_set_fi.h:50
value_set_fit::apply_code
void apply_code(const codet &code, const namespacet &ns)
Definition:
value_set_fi.cpp:1379
value_set_fit::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition:
value_set_fi.cpp:1366
value_set_fit::changed
bool changed
Definition:
value_set_fi.h:252
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:1317
coverage_criteriont::LOCATION
@ LOCATION
coverage_criteriont::ASSUME
@ ASSUME
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
END_FUNCTION
@ END_FUNCTION
Definition:
goto_program.h:42
ASSIGN
@ ASSIGN
Definition:
goto_program.h:46
ASSERT
@ ASSERT
Definition:
goto_program.h:36
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition:
goto_program.h:45
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition:
goto_program.h:43
CATCH
@ CATCH
Definition:
goto_program.h:51
END_THREAD
@ END_THREAD
Definition:
goto_program.h:40
SKIP
@ SKIP
Definition:
goto_program.h:38
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition:
goto_program.h:33
START_THREAD
@ START_THREAD
Definition:
goto_program.h:39
THROW
@ THROW
Definition:
goto_program.h:50
DECL
@ DECL
Definition:
goto_program.h:47
OTHER
@ OTHER
Definition:
goto_program.h:37
GOTO
@ GOTO
Definition:
goto_program.h:34
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition:
goto_program.h:52
value_set_domain_fi.h
Value Set (Flow Insensitive)
src
pointer-analysis
value_set_domain_fi.cpp
Generated by
1.9.1