CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
local_cfg.h
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#ifndef CPROVER_ANALYSES_LOCAL_CFG_H
13#define CPROVER_ANALYSES_LOCAL_CFG_H
14
16
17#include <map>
18
20{
21public:
22 typedef std::size_t node_nrt;
23 typedef std::vector<node_nrt> successorst;
24
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
41 {
43 }
44
45protected:
46 void build(const goto_programt &goto_program);
47};
48
49#endif // CPROVER_ANALYSES_LOCAL_CFG_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
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.