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 
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