cprover
Loading...
Searching...
No Matches
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_offsettentry_mapt
typedef std::size_t entryt
Public Types inherited from cfg_baset< T, P, I >
typedef base_grapht::node_indext entryt
typedef base_grapht::nodet nodet
Public Types inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
typedef cfg_base_nodet< T, goto_programt::const_targettnodet
typedef nodet::edgest edgest
typedef std::vector< nodetnodest
typedef nodet::edget edget
typedef nodet::node_indext node_indext
typedef std::list< node_indextpatht
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_offsettnodet
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)
java_bytecode_convert_methodt::method_offsett get_node_index (const java_bytecode_convert_methodt::method_offsett &instruction) const
nodetget_node (const java_bytecode_convert_methodt::method_offsett &instruction)
const nodetget_node (const java_bytecode_convert_methodt::method_offsett &instruction) const
Public Member Functions inherited from cfg_baset< T, P, I >
 cfg_baset ()
virtual ~cfg_baset ()
void operator() (const goto_functionst &goto_functions)
void operator() (P &goto_program)
entryt get_node_index (const goto_programt::const_targett &program_point) const
 Get the graph node index for program_point.
nodetget_node (const goto_programt::const_targett &program_point)
 Get the CFG graph node relating to program_point.
const nodetget_node (const goto_programt::const_targett &program_point) const
 Get the CFG graph node relating to program_point.
const entry_maptentries () const
 Get a map from program points to their corresponding node indices.
Public Member Functions inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
node_indext add_node (arguments &&... values)
void swap (grapht &other)
bool has_edge (node_indext i, node_indext j) const
const nodetoperator[] (node_indext n) const
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.
void disconnect_unreachable (node_indext src)
 Removes any edges between nodes in a graph that are unreachable from a given start node.
std::vector< typename cfg_base_nodet< T, goto_programt::const_targett >::node_indextdepth_limited_search (typename cfg_base_nodet< T, goto_programt::const_targett >::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_indexttopsort () const
 Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
std::vector< node_indextget_predecessors (const node_indext &n) const
std::vector< node_indextget_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
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 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.
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.
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_indextdepth_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_indextdepth_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_indexttopsort () const
 Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
std::vector< node_indextget_predecessors (const node_indext &n) const
std::vector< node_indextget_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)
Static Public Member Functions inherited from cfg_baset< T, P, I >
static I get_first_node (P &program)
static I get_last_node (P &program)
static bool nodes_empty (P &program)

Public Attributes

entry_mapt entry_map
Public Attributes inherited from cfg_baset< T, P, I >
entry_mapt entry_map

Protected Member Functions

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, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::entryt &entry)
Protected Member Functions inherited from cfg_baset< T, P, I >
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, goto_programt::const_targett > >
void tarjan (class tarjant &t, node_indext v) const
Protected Member Functions inherited from grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > >
std::vector< typename cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett >::node_indextdepth_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
void shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const

Additional Inherited Members

Protected Attributes inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
nodest nodes
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 >

Definition at line 27 of file java_local_variable_table.cpp.

Member Typedef Documentation

◆ base_grapht

◆ entry_mapt

◆ entryt

◆ method_with_amapt

◆ nodet

Constructor & Destructor Documentation

◆ procedure_local_cfg_baset()

Member Function Documentation

◆ compute_edges_function_call()

◆ get_first_node()

◆ get_last_node()

◆ get_node() [1/2]

◆ get_node() [2/2]

◆ get_node_index()

◆ nodes_empty()

◆ operator()()

Member Data Documentation

◆ entry_map


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