cprover
points_to.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Field-sensitive, location-insensitive points-to analysis
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
points_to.h
"
13
14
void
points_tot::fixedpoint
()
15
{
16
// this loop iterates until fixed-point
17
18
bool
added;
19
20
do
21
{
22
added=
false
;
23
24
for
(cfgt::entry_mapt::iterator
25
e_it=
cfg
.
entry_map
.begin();
26
e_it!=
cfg
.
entry_map
.end();
27
e_it++)
28
{
29
if
(
transform
(
cfg
[e_it->second]))
30
added=
true
;
31
}
32
}
33
while
(added);
34
}
35
36
void
points_tot::output
(std::ostream &out)
const
37
{
38
for
(value_mapt::const_iterator
39
v_it=
value_map
.begin();
40
v_it!=
value_map
.end();
41
v_it++)
42
{
43
out << v_it->first <<
":"
;
44
45
for
(object_id_sett::const_iterator
46
o_it=v_it->second.begin();
47
o_it!=v_it->second.end();
48
o_it++)
49
{
50
out <<
" "
<< *o_it;
51
}
52
53
out <<
'\n'
;
54
}
55
}
56
57
bool
points_tot::transform
(
const
cfgt::nodet &e)
58
{
59
bool
result=
false
;
60
const
goto_programt::instructiont
&instruction=*(e.PC);
61
62
switch
(instruction.
type
)
63
{
64
case
RETURN
:
65
// TODO
66
break
;
67
68
case
ASSIGN
:
69
{
70
// const code_assignt &code_assign=to_code_assign(instruction.code);
71
}
72
break
;
73
74
case
FUNCTION_CALL
:
75
// these are like assignments for the arguments
76
break
;
77
78
default
:
79
{
80
}
81
}
82
83
return
result;
84
}
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition:
goto_program.h:190
points_tot::fixedpoint
void fixedpoint()
Definition:
points_to.cpp:14
points_tot::cfg
cfgt cfg
Definition:
points_to.h:50
points_tot::transform
bool transform(const cfgt::nodet &)
Definition:
points_to.cpp:57
points_tot::value_map
value_mapt value_map
Definition:
points_to.h:53
RETURN
Definition:
goto_program.h:45
cfg_baset::entry_map
entry_mapt entry_map
Definition:
cfg.h:106
ASSIGN
Definition:
goto_program.h:46
points_to.h
FUNCTION_CALL
Definition:
goto_program.h:49
points_tot::output
void output(std::ostream &out) const
Definition:
points_to.cpp:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition:
goto_program.h:178
goto-instrument
points_to.cpp
Generated by
1.8.16