cprover
points_to.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-sensitive, location-insensitive points-to analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "points_to.h"
13
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
33void 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
54bool 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 {
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:
92 break;
93 }
94
95 return result;
96}
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition: cfg.h:259
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
void fixedpoint()
Definition: points_to.cpp:14
bool transform(const cfgt::nodet &)
Definition: points_to.cpp:54
cfgt cfg
Definition: points_to.h:50
value_mapt value_map
Definition: points_to.h:53
void output(std::ostream &out) const
Definition: points_to.cpp:33
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
Field-sensitive, location-insensitive points-to analysis.