cprover
Loading...
Searching...
No Matches
local_cfg.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: CFG for One Function
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "local_cfg.h"
13
14void 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.get_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:
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:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
targetst targets
The list of successor instructions.
Definition: goto_program.h:403
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
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:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
goto_programt::const_targett t
Definition: local_cfg.h:28
successorst successors
Definition: local_cfg.h:29
nodest nodes
Definition: local_cfg.h:36
std::size_t node_nrt
Definition: local_cfg.h:22
loc_mapt loc_map
Definition: local_cfg.h:33
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
@ LOCATION
Definition: goto_program.h:41
@ 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
@ ASSUME
Definition: goto_program.h:35
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:510