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 }
void build(const goto_programt &goto_program)
Definition: local_cfg.cpp:27
loc_mapt loc_map
Definition: local_cfg.h:33
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
std::size_t node_nrt
Definition: local_cfg.h:22
CFG for One Function.
nodest nodes
Definition: local_cfg.h:36
instructionst::const_iterator const_targett
API to expression classes.
goto_programt::const_targett t
Definition: local_cfg.h:28
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
successorst successors
Definition: local_cfg.h:29