cprover
Loading...
Searching...
No Matches
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
(
const
auto
&instruction_and_entry :
cfg
.entries())
25
{
26
if
(
transform
(
cfg
[instruction_and_entry.second]))
27
added=
true
;
28
}
29
}
30
while
(added);
31
}
32
33
void
points_tot::output
(std::ostream &out)
const
34
{
35
for
(value_mapt::const_iterator
36
v_it=
value_map
.begin();
37
v_it!=
value_map
.end();
38
v_it++)
39
{
40
out << v_it->first <<
":"
;
41
42
for
(object_id_sett::const_iterator
43
o_it=v_it->second.begin();
44
o_it!=v_it->second.end();
45
o_it++)
46
{
47
out <<
" "
<< *o_it;
48
}
49
50
out <<
'\n'
;
51
}
52
}
53
54
bool
points_tot::transform
(
const
cfgt::nodet
&e)
55
{
56
bool
result=
false
;
57
const
goto_programt::instructiont
&instruction=*(e.PC);
58
59
switch
(instruction.
type
())
60
{
61
case
SET_RETURN_VALUE
:
62
// TODO
63
break
;
64
65
case
ASSIGN
:
66
{
67
// const code_assignt &code_assign=to_code_assign(instruction.code);
68
}
69
break
;
70
71
case
FUNCTION_CALL
:
72
// these are like assignments for the arguments
73
break
;
74
75
case
CATCH
:
76
case
THROW
:
77
case
GOTO
:
78
case
DEAD
:
79
case
DECL
:
80
case
ATOMIC_BEGIN
:
81
case
ATOMIC_END
:
82
case
START_THREAD
:
83
case
END_THREAD
:
84
case
END_FUNCTION
:
85
case
LOCATION
:
86
case
OTHER
:
87
case
SKIP
:
88
case
ASSERT
:
89
case
ASSUME
:
90
case
INCOMPLETE_GOTO
:
91
case
NO_INSTRUCTION_TYPE
:
92
break
;
93
}
94
95
return
result;
96
}
cfg_baset< empty_cfg_nodet >::nodet
base_grapht::nodet nodet
Definition
cfg.h:92
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition
goto_program.h:181
goto_programt::instructiont::type
goto_program_instruction_typet type() const
What kind of instruction?
Definition
goto_program.h:344
points_tot::fixedpoint
void fixedpoint()
Definition
points_to.cpp:14
points_tot::transform
bool transform(const cfgt::nodet &)
Definition
points_to.cpp:54
points_tot::cfg
cfgt cfg
Definition
points_to.h:50
points_tot::value_map
value_mapt value_map
Definition
points_to.h:53
points_tot::output
void output(std::ostream &out) const
Definition
points_to.cpp:33
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
points_to.h
Field-sensitive, location-insensitive points-to analysis.
goto-instrument
points_to.cpp
Generated by
1.13.2