cprover
cfg_baset< T, P, I > Class Template Reference

A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program. More...

#include <cfg.h>

Inheritance diagram for cfg_baset< T, P, I >:
[legend]
Collaboration diagram for cfg_baset< T, P, I >:
[legend]

Classes

struct  entry_mapt
 

Public Types

typedef std::size_t entryt
 
- Public Types inherited from grapht< cfg_base_nodet< T, I > >
typedef cfg_base_nodet< T, I > nodet
 
typedef nodet::edgest edgest
 
typedef std::vector< nodetnodest
 
typedef nodet::edget edget
 
typedef nodet::node_indext node_indext
 
typedef std::list< node_indextpatht
 

Public Member Functions

 cfg_baset ()
 
virtual ~cfg_baset ()
 
void operator() (const goto_functionst &goto_functions)
 
void operator() (P &goto_program)
 
get_first_node (P &program) const
 
get_last_node (P &program) const
 
bool nodes_empty (P &program) const
 
- Public Member Functions inherited from grapht< cfg_base_nodet< T, I > >
node_indext add_node ()
 
void swap (grapht &other)
 
bool has_edge (node_indext i, node_indext j) const
 
const nodetoperator[] (node_indext n) const
 
nodetoperator[] (node_indext n)
 
void resize (node_indext s)
 
std::size_t size () const
 
bool empty () const
 
const edgestin (node_indext n) const
 
const edgestout (node_indext n) const
 
void add_edge (node_indext a, node_indext b)
 
void remove_edge (node_indext a, node_indext b)
 
edgetedge (node_indext a, node_indext b)
 
void add_undirected_edge (node_indext a, node_indext b)
 
void remove_undirected_edge (node_indext a, node_indext b)
 
void remove_in_edges (node_indext n)
 
void remove_out_edges (node_indext n)
 
void remove_edges (node_indext n)
 
void clear ()
 
void shortest_path (node_indext src, node_indext dest, patht &path) const
 
void shortest_loop (node_indext node, patht &path) const
 
void visit_reachable (node_indext src)
 
void make_chordal ()
 
std::size_t connected_subgraphs (std::vector< node_indext > &subgraph_nr)
 
std::size_t SCCs (std::vector< node_indext > &subgraph_nr)
 
bool is_dag () const
 
std::list< node_indexttopsort () const
 Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph. More...
 
void output_dot (std::ostream &out) const
 
void output_dot_node (std::ostream &out, node_indext n) const
 

Public Attributes

entry_mapt entry_map
 

Protected Member Functions

virtual void compute_edges_goto (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
 
virtual void compute_edges_catch (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
 
virtual void compute_edges_throw (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
 
virtual void compute_edges_start_thread (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
 
virtual void compute_edges_function_call (const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
 
void compute_edges (const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
 
void compute_edges (const goto_functionst &goto_functions, P &goto_program)
 
void compute_edges (const goto_functionst &goto_functions)
 
- Protected Member Functions inherited from grapht< cfg_base_nodet< T, I > >
void shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const
 
void tarjan (class tarjant &t, node_indext v)
 

Additional Inherited Members

- Protected Attributes inherited from grapht< cfg_base_nodet< T, I > >
nodest nodes
 

Detailed Description

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
class cfg_baset< T, P, I >

A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program.

An instance of cfg_baset<T> is a directed graph whose nodes inherit from a user-provided type T and store a pointer to an instruction of some goto program in the field PC. The field PC of every node points to the original GOTO instruction that gave rise to the node, and the field cfg_baset::entry_map maps every GOTO instruction to some CFG node.

The CFG is constructed on the operator() from either one goto_programt or multiple goto_programt objects (stored in a goto_functionst). The edges of the CFG are created on the method compute_edges(), and notably include:

  • Edges from location A to B if both A and B belong to the same goto_programt and A can flow into B.
  • An edge from each FUNCTION_CALL instruction and the first instruction of the called function, when that function body is available and its body is non-empty.
  • For each FUNCTION_CALL instruction found, an edge between the exit point of the called function and the instruction immediately after the FUNCTION_CALL, when the function body is available and its body is non-empty.

    Note that cfg_baset is the base class of many other subclasses and the specific edges constructed by operator() can be different in those.

Definition at line 62 of file cfg.h.

Member Typedef Documentation

◆ entryt

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
typedef std::size_t cfg_baset< T, P, I >::entryt

Definition at line 65 of file cfg.h.

Constructor & Destructor Documentation

◆ cfg_baset()

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
cfg_baset< T, P, I >::cfg_baset ( )
inline

Definition at line 134 of file cfg.h.

◆ ~cfg_baset()

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
virtual cfg_baset< T, P, I >::~cfg_baset ( )
inlinevirtual

Definition at line 138 of file cfg.h.

Member Function Documentation

◆ compute_edges() [1/3]

template<class T , typename P , typename I>
void cfg_baset< T, P, I >::compute_edges ( const goto_functionst goto_functions,
const goto_programt goto_program,
PC 
)
protected

Definition at line 338 of file cfg.h.

Referenced by cfg_baset< cfg_nodet >::operator()().

◆ compute_edges() [2/3]

template<class T , typename P, typename I>
void cfg_baset< T, P, I >::compute_edges ( const goto_functionst goto_functions,
P &  goto_program 
)
protected

Definition at line 412 of file cfg.h.

◆ compute_edges() [3/3]

template<class T , typename P, typename I>
void cfg_baset< T, P, I >::compute_edges ( const goto_functionst goto_functions)
protected

Definition at line 423 of file cfg.h.

◆ compute_edges_catch()

template<class T , typename P , typename I >
void cfg_baset< T, P, I >::compute_edges_catch ( const goto_programt goto_program,
const goto_programt::instructiont &  instruction,
goto_programt::const_targett  next_PC,
entryt entry 
)
protectedvirtual

Definition at line 212 of file cfg.h.

◆ compute_edges_function_call()

template<class T , typename P , typename I >
void cfg_baset< T, P, I >::compute_edges_function_call ( const goto_functionst goto_functions,
const goto_programt goto_program,
const goto_programt::instructiont &  instruction,
goto_programt::const_targett  next_PC,
entryt entry 
)
protectedvirtual

Definition at line 269 of file cfg.h.

◆ compute_edges_goto()

template<class T , typename P , typename I >
void cfg_baset< T, P, I >::compute_edges_goto ( const goto_programt goto_program,
const goto_programt::instructiont &  instruction,
goto_programt::const_targett  next_PC,
entryt entry 
)
protectedvirtual

Definition at line 196 of file cfg.h.

◆ compute_edges_start_thread()

template<class T , typename P , typename I >
void cfg_baset< T, P, I >::compute_edges_start_thread ( const goto_programt goto_program,
const goto_programt::instructiont &  instruction,
goto_programt::const_targett  next_PC,
entryt entry 
)
protectedvirtual

Definition at line 240 of file cfg.h.

Referenced by concurrent_cfg_baset< T, P, I >::compute_edges_start_thread().

◆ compute_edges_throw()

template<class T , typename P , typename I >
void cfg_baset< T, P, I >::compute_edges_throw ( const goto_programt goto_program,
const goto_programt::instructiont &  instruction,
goto_programt::const_targett  next_PC,
entryt entry 
)
protectedvirtual

Definition at line 230 of file cfg.h.

◆ get_first_node()

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
I cfg_baset< T, P, I >::get_first_node ( P &  program) const
inline

Definition at line 154 of file cfg.h.

◆ get_last_node()

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
I cfg_baset< T, P, I >::get_last_node ( P &  program) const
inline

Definition at line 155 of file cfg.h.

◆ nodes_empty()

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
bool cfg_baset< T, P, I >::nodes_empty ( P &  program) const
inline

Definition at line 156 of file cfg.h.

◆ operator()() [1/2]

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
void cfg_baset< T, P, I >::operator() ( const goto_functionst goto_functions)
inline

Definition at line 142 of file cfg.h.

◆ operator()() [2/2]

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
void cfg_baset< T, P, I >::operator() ( P &  goto_program)
inline

Definition at line 148 of file cfg.h.

Member Data Documentation

◆ entry_map


The documentation for this class was generated from the following file: