cprover
|
#include <cfg.h>
Additional Inherited Members | |
![]() | |
typedef std::size_t | entryt |
![]() | |
typedef cfg_base_nodet< T, I > | nodet |
typedef nodet::edgest | edgest |
typedef std::vector< nodet > | nodest |
typedef nodet::edget | edget |
typedef nodet::node_indext | node_indext |
typedef std::list< node_indext > | patht |
![]() | |
cfg_baset () | |
virtual | ~cfg_baset () |
void | operator() (const goto_functionst &goto_functions) |
void | operator() (P &goto_program) |
I | get_first_node (P &program) const |
I | get_last_node (P &program) const |
bool | nodes_empty (P &program) const |
![]() | |
node_indext | add_node () |
void | swap (grapht &other) |
bool | has_edge (node_indext i, node_indext j) const |
const nodet & | operator[] (node_indext n) const |
nodet & | operator[] (node_indext n) |
void | resize (node_indext s) |
std::size_t | size () const |
bool | empty () const |
const edgest & | in (node_indext n) const |
const edgest & | out (node_indext n) const |
void | add_edge (node_indext a, node_indext b) |
void | remove_edge (node_indext a, node_indext b) |
edget & | edge (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_indext > | topsort () 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 |
![]() | |
entry_mapt | entry_map |
![]() | |
virtual void | compute_edges_start_thread (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, typename cfg_baset< T, P, I >::entryt &entry) |
![]() | |
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) |
![]() | |
void | shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const |
void | tarjan (class tarjant &t, node_indext v) |
![]() | |
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, typename cfg_baset< T, P, I >::entryt &entry) |
![]() | |
nodest | nodes |