cprover
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned > Struct Template Reference
Inheritance diagram for procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >:
[legend]
Collaboration diagram for procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >:
[legend]

Public Types

typedef java_bytecode_convert_methodt::method_with_amapt method_with_amapt
 
typedef std::map< unsigned, unsigned > entry_mapt
 
- Public Types inherited from grapht< cfg_base_nodet< T, unsigned > >
typedef cfg_base_nodet< T, unsigned > 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

 procedure_local_cfg_baset ()
 
void operator() (const method_with_amapt &args)
 
unsigned get_first_node (const method_with_amapt &args) const
 
unsigned get_last_node (const method_with_amapt &args) const
 
bool nodes_empty (const method_with_amapt &args) const
 
- Public Member Functions inherited from grapht< cfg_base_nodet< T, unsigned > >
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)
 
std::vector< node_indextget_reachable (node_indext src, bool forwards) const
 Run depth-first search on the graph, starting from a single source node. More...
 
std::vector< node_indextget_reachable (const std::vector< node_indext > &src, bool forwards) const
 Run depth-first search on the graph, starting from multiple source nodes. More...
 
void disconnect_unreachable (node_indext src)
 Removes any edges between nodes in a graph that are unreachable from a given start node. More...
 
void disconnect_unreachable (const std::vector< node_indext > &src)
 Removes any edges between nodes in a graph that are unreachable from a vector of start nodes. More...
 
std::vector< typename cfg_base_nodet< T, unsigned > ::node_indextdepth_limited_search (typename cfg_base_nodet< T, unsigned > ::node_indext src, std::size_t limit) const
 Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...
 
std::vector< typename cfg_base_nodet< T, unsigned > ::node_indextdepth_limited_search (std::vector< typename cfg_base_nodet< T, unsigned > ::node_indext > &src, std::size_t limit) const
 Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...
 
void make_chordal ()
 Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges. More...
 
std::size_t connected_subgraphs (std::vector< node_indext > &subgraph_nr)
 Find connected subgraphs in an undirected graph. More...
 
std::size_t SCCs (std::vector< node_indext > &subgraph_nr) const
 Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes to components indices. More...
 
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...
 
std::vector< node_indextget_successors (const node_indext &n) const
 
void output_dot (std::ostream &out) const
 
void for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const
 

Public Attributes

entry_mapt entry_map
 

Additional Inherited Members

- Protected Member Functions inherited from grapht< cfg_base_nodet< T, unsigned > >
void shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const
 
std::vector< typename cfg_base_nodet< T, unsigned > ::node_indextdepth_limited_search (std::vector< typename cfg_base_nodet< T, unsigned > ::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const
 Run recursive depth-limited search on the graph, starting. More...
 
void tarjan (class tarjant &t, node_indext v) const
 
- Protected Attributes inherited from grapht< cfg_base_nodet< T, unsigned > >
nodest nodes
 

Detailed Description

template<class T>
struct procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >

Definition at line 28 of file java_local_variable_table.cpp.

Member Typedef Documentation

◆ entry_mapt

template<class T >
typedef std::map<unsigned, unsigned> procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >::entry_mapt

Definition at line 35 of file java_local_variable_table.cpp.

◆ method_with_amapt

Constructor & Destructor Documentation

◆ procedure_local_cfg_baset()

Member Function Documentation

◆ get_first_node()

template<class T >
unsigned procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >::get_first_node ( const method_with_amapt args) const
inline

Definition at line 85 of file java_local_variable_table.cpp.

◆ get_last_node()

template<class T >
unsigned procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >::get_last_node ( const method_with_amapt args) const
inline

Definition at line 90 of file java_local_variable_table.cpp.

◆ nodes_empty()

template<class T >
bool procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >::nodes_empty ( const method_with_amapt args) const
inline

Definition at line 95 of file java_local_variable_table.cpp.

◆ operator()()

Member Data Documentation

◆ entry_map

Definition at line 36 of file java_local_variable_table.cpp.


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