Loading...
Searching...
No Matches
Public Types |
Public Member Functions |
Static Public Member Functions |
Public Attributes |
List of all members
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett > Struct Template Reference
Inheritance diagram for procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >: Collaboration diagram for procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >:Public Types | |
| typedef grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > | base_grapht |
| typedef base_grapht::nodet | nodet |
| typedef java_bytecode_convert_methodt::method_with_amapt | method_with_amapt |
| typedef std::map< java_bytecode_convert_methodt::method_offsett, java_bytecode_convert_methodt::method_offsett > | entry_mapt |
| typedef std::size_t | entryt |
| Public Types inherited from grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > | |
| typedef cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > | 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 |
Public Member Functions | |
| procedure_local_cfg_baset () | |
| void | operator() (const method_with_amapt &args) |
| java_bytecode_convert_methodt::method_offsett | get_node_index (const java_bytecode_convert_methodt::method_offsett &instruction) const |
| nodet & | get_node (const java_bytecode_convert_methodt::method_offsett &instruction) |
| const nodet & | get_node (const java_bytecode_convert_methodt::method_offsett &instruction) const |
| Public Member Functions inherited from grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > | |
| node_indext | add_node (arguments &&... values) |
| 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) |
| std::vector< node_indext > | get_reachable (node_indext src, bool forwards) const |
| Run depth-first search on the graph, starting from a single source node. | |
| std::vector< node_indext > | get_reachable (const std::vector< node_indext > &src, bool forwards) const |
| Run depth-first search on the graph, starting from multiple source nodes. | |
| void | disconnect_unreachable (node_indext src) |
| Removes any edges between nodes in a graph that are unreachable from a given start node. | |
| 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. | |
| std::vector< typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::node_indext > | depth_limited_search (typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::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. | |
| std::vector< typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::node_indext > | depth_limited_search (std::vector< typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::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. | |
| void | make_chordal () |
| Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges. | |
| std::size_t | connected_subgraphs (std::vector< node_indext > &subgraph_nr) |
| Find connected subgraphs in an undirected graph. | |
| 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. | |
| 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. | |
| std::vector< node_indext > | get_predecessors (const node_indext &n) const |
| std::vector< node_indext > | get_successors (const node_indext &n) const |
| void | output_dot (std::ostream &out) const |
| void | for_each_predecessor (const node_indext &n, std::function< void(const node_indext &)> f) const |
| void | for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const |
Static Public Member Functions | |
| static java_bytecode_convert_methodt::method_offsett | get_first_node (const method_with_amapt &args) |
| static java_bytecode_convert_methodt::method_offsett | get_last_node (const method_with_amapt &args) |
| static bool | nodes_empty (const method_with_amapt &args) |
Public Attributes | |
| entry_mapt | entry_map |
Additional Inherited Members | |
| Protected Member Functions inherited from grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > | |
| void | shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const |
| std::vector< typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::node_indext > | depth_limited_search (std::vector< typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const |
| Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. | |
| void | tarjan (class tarjant &t, node_indext v) const |
| Protected Attributes inherited from grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > | |
| nodest | nodes |
Detailed Description
template<class T>
struct procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >
struct procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >
Definition at line 27 of file java_local_variable_table.cpp.
Member Typedef Documentation
◆ base_grapht
template<class T >
Definition at line 36 of file java_local_variable_table.cpp.
◆ entry_mapt
template<class T >
Definition at line 41 of file java_local_variable_table.cpp.
◆ entryt
template<class T >
| std::size_t procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::entryt |
Definition at line 42 of file java_local_variable_table.cpp.
◆ method_with_amapt
template<class T >
| java_bytecode_convert_methodt::method_with_amapt procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::method_with_amapt |
Definition at line 38 of file java_local_variable_table.cpp.
◆ nodet
template<class T >
| base_grapht::nodet procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::nodet |
Definition at line 37 of file java_local_variable_table.cpp.
Constructor & Destructor Documentation
◆ procedure_local_cfg_baset()
template<class T >
|
inline |
Definition at line 45 of file java_local_variable_table.cpp.
Member Function Documentation
◆ get_first_node()
template<class T >
|
inlinestatic |
Definition at line 110 of file java_local_variable_table.cpp.
◆ get_last_node()
template<class T >
|
inlinestatic |
Definition at line 116 of file java_local_variable_table.cpp.
◆ get_node() [1/2]
template<class T >
|
inline |
Definition at line 99 of file java_local_variable_table.cpp.
◆ get_node() [2/2]
template<class T >
|
inline |
Definition at line 103 of file java_local_variable_table.cpp.
◆ get_node_index()
template<class T >
|
inline |
Definition at line 92 of file java_local_variable_table.cpp.
◆ nodes_empty()
template<class T >
|
inlinestatic |
Definition at line 121 of file java_local_variable_table.cpp.
◆ operator()()
template<class T >
|
inline |
Definition at line 47 of file java_local_variable_table.cpp.
Member Data Documentation
◆ entry_map
template<class T >
| entry_mapt procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::entry_map |
Definition at line 43 of file java_local_variable_table.cpp.
The documentation for this struct was generated from the following file:
- /builddir/build/BUILD/cbmc-6.4.1-build/cbmc-cbmc-6.4.1/jbmc/src/java_bytecode/java_local_variable_table.cpp
