cprover
local_cfg.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CFG for One Function
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "local_cfg.h"
13 
14 #if 0
15 #include <iterator>
16 #include <algorithm>
17 
18 #include <util/std_expr.h>
19 #include <util/std_code.h>
20 #include <util/expr_util.h>
21 
22 #include <util/c_types.h>
23 #include <langapi/language_util.h>
24 
25 #endif
26 
27 void local_cfgt::build(const goto_programt &goto_program)
28 {
29  nodes.resize(goto_program.instructions.size());
30 
31  {
32  node_nrt loc_nr=0;
33 
34  for(goto_programt::const_targett it=goto_program.instructions.begin();
35  it!=goto_program.instructions.end();
36  it++, loc_nr++)
37  {
38  loc_map[it]=loc_nr;
39  nodes[loc_nr].t=it;
40  }
41  }
42 
43  for(node_nrt loc_nr=0; loc_nr<nodes.size(); loc_nr++)
44  {
45  nodet &node=nodes[loc_nr];
46  const goto_programt::instructiont &instruction=*node.t;
47 
48  switch(instruction.type)
49  {
50  case GOTO:
51  if(!instruction.guard.is_true())
52  node.successors.push_back(loc_nr+1);
53 
54  for(const auto &target : instruction.targets)
55  {
56  node_nrt l=loc_map.find(target)->second;
57  node.successors.push_back(l);
58  }
59  break;
60 
61  case START_THREAD:
62  node.successors.push_back(loc_nr+1);
63 
64  for(const auto &target : instruction.targets)
65  {
66  node_nrt l=loc_map.find(target)->second;
67  node.successors.push_back(l);
68  }
69  break;
70 
71  case THROW:
72  case END_FUNCTION:
73  case END_THREAD:
74  break; // no successor
75 
76  default:
77  node.successors.push_back(loc_nr+1);
78  }
79  }
80 }
local_cfgt::build
void build(const goto_programt &goto_program)
Definition: local_cfg.cpp:27
local_cfgt::loc_map
loc_mapt loc_map
Definition: local_cfg.h:33
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
THROW
@ THROW
Definition: goto_program.h:50
GOTO
@ GOTO
Definition: goto_program.h:34
language_util.h
local_cfg.h
local_cfgt::nodes
nodest nodes
Definition: local_cfg.h:36
local_cfgt::nodet
Definition: local_cfg.h:25
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
std_code.h
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
expr_util.h
Deprecated expression utility functions.
local_cfgt::node_nrt
std::size_t node_nrt
Definition: local_cfg.h:22
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
local_cfgt::nodet::successors
successorst successors
Definition: local_cfg.h:29
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
local_cfgt::nodet::t
goto_programt::const_targett t
Definition: local_cfg.h:28
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
c_types.h
END_THREAD
@ END_THREAD
Definition: goto_program.h:40