CBMC
local_cfg.h
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 #ifndef CPROVER_ANALYSES_LOCAL_CFG_H
13 #define CPROVER_ANALYSES_LOCAL_CFG_H
14 
16 
17 #include <map>
18 
20 {
21 public:
22  typedef std::size_t node_nrt;
23  typedef std::vector<node_nrt> successorst;
24 
25  class nodet
26  {
27  public:
30  };
31 
32  typedef std::
33  map<goto_programt::const_targett, node_nrt, goto_programt::target_less_than>
36 
37  typedef std::vector<nodet> nodest;
39 
40  explicit local_cfgt(const goto_programt &_goto_program)
41  {
42  build(_goto_program);
43  }
44 
45 protected:
46  void build(const goto_programt &goto_program);
47 };
48 
49 #endif // CPROVER_ANALYSES_LOCAL_CFG_H
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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::map< goto_programt::const_targett, node_nrt, goto_programt::target_less_than > loc_mapt
Definition: local_cfg.h:34
std::vector< nodet > nodest
Definition: local_cfg.h:37
std::size_t node_nrt
Definition: local_cfg.h:22
loc_mapt loc_map
Definition: local_cfg.h:35
std::vector< node_nrt > successorst
Definition: local_cfg.h:23
local_cfgt(const goto_programt &_goto_program)
Definition: local_cfg.h:40
void build(const goto_programt &goto_program)
Definition: local_cfg.cpp:14
Concrete Goto Program.