CBMC
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 void local_cfgt::build(const goto_programt &goto_program)
15 {
16  nodes.resize(goto_program.instructions.size());
17 
18  {
19  node_nrt loc_nr=0;
20 
21  for(goto_programt::const_targett it=goto_program.instructions.begin();
22  it!=goto_program.instructions.end();
23  it++, loc_nr++)
24  {
25  loc_map[it]=loc_nr;
26  nodes[loc_nr].t=it;
27  }
28  }
29 
30  for(node_nrt loc_nr=0; loc_nr<nodes.size(); loc_nr++)
31  {
32  nodet &node=nodes[loc_nr];
33  const goto_programt::instructiont &instruction=*node.t;
34 
35  switch(instruction.type())
36  {
37  case GOTO:
38  if(!instruction.condition().is_true())
39  node.successors.push_back(loc_nr+1);
40 
41  for(const auto &target : instruction.targets)
42  {
43  node_nrt l=loc_map.find(target)->second;
44  node.successors.push_back(l);
45  }
46  break;
47 
48  case START_THREAD:
49  node.successors.push_back(loc_nr+1);
50 
51  for(const auto &target : instruction.targets)
52  {
53  node_nrt l=loc_map.find(target)->second;
54  node.successors.push_back(l);
55  }
56  break;
57 
58  case THROW:
59  case END_FUNCTION:
60  case END_THREAD:
61  break; // no successor
62 
63  case CATCH:
64  case SET_RETURN_VALUE:
65  case ATOMIC_BEGIN:
66  case ATOMIC_END:
67  case LOCATION:
68  case SKIP:
69  case OTHER:
70  case ASSERT:
71  case ASSUME:
72  case FUNCTION_CALL:
73  case DECL:
74  case DEAD:
75  case ASSIGN:
76  node.successors.push_back(loc_nr + 1);
77  break;
78 
79  case INCOMPLETE_GOTO:
81  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
82  break;
83  }
84  }
85 }
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:366
targetst targets
The list of successor instructions.
Definition: goto_program.h:414
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:344
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::const_iterator const_targett
Definition: goto_program.h:615
goto_programt::const_targett t
Definition: local_cfg.h:28
successorst successors
Definition: local_cfg.h:29
nodest nodes
Definition: local_cfg.h:38
std::size_t node_nrt
Definition: local_cfg.h:22
loc_mapt loc_map
Definition: local_cfg.h:35
void build(const goto_programt &goto_program)
Definition: local_cfg.cpp:14
@ 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
CFG for One Function.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534