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 
28 {
29  nodes.resize(goto_program.instructions.size());
30 
31  {
32  node_nrt loc_nr=0;
33 
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 }
void build(const goto_programt &goto_program)
Definition: local_cfg.cpp:27
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
loc_mapt loc_map
Definition: local_cfg.h:33
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
Deprecated expression utility functions.
bool is_true() const
Definition: expr.cpp:124
std::size_t node_nrt
Definition: local_cfg.h:22
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
CFG for One Function.
nodest nodes
Definition: local_cfg.h:36
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
goto_programt::const_targett t
Definition: local_cfg.h:28
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
goto_programt & goto_program
Definition: cover.cpp:63
successorst successors
Definition: local_cfg.h:29