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.get_condition().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  case CATCH:
77  case RETURN:
78  case ATOMIC_BEGIN:
79  case ATOMIC_END:
80  case LOCATION:
81  case SKIP:
82  case OTHER:
83  case ASSERT:
84  case ASSUME:
85  case FUNCTION_CALL:
86  case DECL:
87  case DEAD:
88  case ASSIGN:
89  node.successors.push_back(loc_nr + 1);
90  break;
91 
92  case INCOMPLETE_GOTO:
94  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
95  break;
96  }
97  }
98 }
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:272
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:306
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
THROW
@ THROW
Definition: goto_program.h:50
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
language_util.h
local_cfg.h
CFG for One Function.
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
local_cfgt::nodes
nodest nodes
Definition: local_cfg.h:36
OTHER
@ OTHER
Definition: goto_program.h:37
local_cfgt::nodet
Definition: local_cfg.h:26
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
std_code.h
RETURN
@ RETURN
Definition: goto_program.h:45
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
expr_util.h
Deprecated expression utility functions.
local_cfgt::node_nrt
std::size_t node_nrt
Definition: local_cfg.h:22
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
CATCH
@ CATCH
Definition: goto_program.h:51
DECL
@ DECL
Definition: goto_program.h:47
ASSUME
@ ASSUME
Definition: goto_program.h:35
local_cfgt::nodet::successors
successorst successors
Definition: local_cfg.h:29
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
DEAD
@ DEAD
Definition: goto_program.h:48
local_cfgt::nodet::t
goto_programt::const_targett t
Definition: local_cfg.h:28
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
c_types.h
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52