CBMC
Toggle main menu visibility
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
a
c
d
e
f
g
j
l
m
r
t
w
Functions
a
c
d
f
g
r
t
w
Typedefs
Enumerations
Classes
Class List
Class Hierarchy
Class Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Variables
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
Enumerations
a
b
c
d
e
f
g
i
k
l
m
o
p
r
s
t
u
v
w
Enumerator
a
b
c
d
e
f
h
i
k
l
m
n
o
p
q
r
s
t
u
v
Related Symbols
b
c
d
e
g
i
j
m
n
o
s
t
u
v
Files
File List
File Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
x
y
z
Variables
_
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
w
y
Typedefs
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
r
s
t
u
v
w
Enumerations
_
a
b
c
d
f
g
i
l
m
p
r
s
t
u
v
w
Enumerator
_
a
c
d
e
f
g
h
i
l
m
n
o
p
r
s
t
u
v
w
Macros
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
y
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
Loading...
Searching...
No Matches
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
}
15
bool
value_set_domain_fit::transform
( {
…
}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition
ai.h:562
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:91
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
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
LOCATION
@ LOCATION
Definition
goto_program.h:41
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
ASSUME
@ ASSUME
Definition
goto_program.h:35
value_set_domain_fi.h
Value Set (Flow Insensitive)
src
pointer-analysis
value_set_domain_fi.cpp
Generated by
1.9.8