Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithms. More...

#include <class_hierarchy.h>

Inheritance diagram for class_hierarchy_grapht:

Collaboration diagram for class_hierarchy_grapht:

Public Types
typedef std::vector< irep_idt >	idst

typedef std::unordered_map< irep_idt, node_indext >	nodes_by_namet
	Maps class identifiers onto node indices. More...

Public Types inherited from grapht< class_hierarchy_graph_nodet >
typedef class_hierarchy_graph_nodet	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
void	populate (const symbol_tablet &)
	Populate the class hierarchy graph, such that there is a node for every struct type in the symbol table and an edge representing each superclass <-> subclass relationship, pointing from parent to child. More...

const nodes_by_namet &	get_nodes_by_class_identifier () const
	Get map from class identifier to node index. More...

idst	get_direct_children (const irep_idt &c) const
	Get all the classes that directly (i.e. More...

idst	get_children_trans (const irep_idt &c) const
	Get all the classes that inherit (directly or indirectly) from class c. More...

idst	get_parents_trans (const irep_idt &c) const
	Get all the classes that class c inherits from (directly or indirectly). More...

Public Member Functions inherited from grapht< class_hierarchy_graph_nodet >
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. More...

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. 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 class_hierarchy_graph_nodet ::node_indext >	depth_limited_search (typename class_hierarchy_graph_nodet ::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 class_hierarchy_graph_nodet ::node_indext >	depth_limited_search (std::vector< typename class_hierarchy_graph_nodet ::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_indext >	topsort () 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_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

Private Member Functions
idst	ids_from_indices (const std::vector< node_indext > &nodes) const
	Helper function that converts a vector of node_indext to a vector of ids that are stored in the corresponding nodes in the graph. More...

idst	get_other_reachable_ids (const irep_idt &c, bool forwards) const
	Helper function for `get_children_trans` and `get_parents_trans` More...

Private Attributes
nodes_by_namet	nodes_by_name
	Maps class identifiers onto node indices. More...

Additional Inherited Members
Protected Member Functions inherited from grapht< class_hierarchy_graph_nodet >
void	shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const

std::vector< typename class_hierarchy_graph_nodet ::node_indext >	depth_limited_search (std::vector< typename class_hierarchy_graph_nodet ::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. More...

void	tarjan (class tarjant &t, node_indext v) const

Protected Attributes inherited from grapht< class_hierarchy_graph_nodet >
nodest	nodes

Detailed Description

Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithms.

Definition at line 102 of file class_hierarchy.h.

Member Typedef Documentation

◆ idst

typedef std::vector<irep_idt> class_hierarchy_grapht::idst

Definition at line 105 of file class_hierarchy.h.

◆ nodes_by_namet

typedef std::unordered_map<irep_idt, node_indext> class_hierarchy_grapht::nodes_by_namet

Maps class identifiers onto node indices.

Definition at line 108 of file class_hierarchy.h.

Member Function Documentation

◆ get_children_trans()

class_hierarchy_grapht::idst class_hierarchy_grapht::get_children_trans ( const irep_idt & c ) const

Get all the classes that inherit (directly or indirectly) from class c.

Parameters

c	The class to consider

Returns: A list containing ids of all classes that eventually inherit from c.

Definition at line 115 of file class_hierarchy.cpp.

◆ get_direct_children()

class_hierarchy_grapht::idst class_hierarchy_grapht::get_direct_children ( const irep_idt & c ) const

Get all the classes that directly (i.e.

in one step) inherit from class c.

Parameters

c	The class to consider

Returns: A list containing ids of all direct children of c.

Definition at line 85 of file class_hierarchy.cpp.

◆ get_nodes_by_class_identifier()

const nodes_by_namet& class_hierarchy_grapht::get_nodes_by_class_identifier ( ) const

inline

Get map from class identifier to node index.

Returns: map from class identifier to node index

Definition at line 114 of file class_hierarchy.h.

◆ get_other_reachable_ids()

class_hierarchy_grapht::idst class_hierarchy_grapht::get_other_reachable_ids	(	const irep_idt &	c,
		bool	forwards
	)		const

private

Helper function for get_children_trans and get_parents_trans

Definition at line 93 of file class_hierarchy.cpp.

◆ get_parents_trans()

class_hierarchy_grapht::idst class_hierarchy_grapht::get_parents_trans ( const irep_idt & c ) const

Get all the classes that class c inherits from (directly or indirectly).

Parameters

c	The class to consider

Returns: A list of class ids that c eventually inherits from.

Definition at line 124 of file class_hierarchy.cpp.

◆ ids_from_indices()

class_hierarchy_grapht::idst class_hierarchy_grapht::ids_from_indices ( const std::vector< node_indext > & nodes ) const

private

Helper function that converts a vector of node_indext to a vector of ids that are stored in the corresponding nodes in the graph.

Definition at line 67 of file class_hierarchy.cpp.

◆ populate()

void class_hierarchy_grapht::populate ( const symbol_tablet & symbol_table )

Populate the class hierarchy graph, such that there is a node for every struct type in the symbol table and an edge representing each superclass <-> subclass relationship, pointing from parent to child.

Parameters

symbol_table global symbol table, which will be searched for struct types.

Definition at line 29 of file class_hierarchy.cpp.

Member Data Documentation

◆ nodes_by_name

nodes_by_namet class_hierarchy_grapht::nodes_by_name

private

Maps class identifiers onto node indices.

Definition at line 127 of file class_hierarchy.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/class_hierarchy.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/class_hierarchy.cpp

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ idst

◆ nodes_by_namet

Member Function Documentation

◆ get_children_trans()

◆ get_direct_children()

◆ get_nodes_by_class_identifier()

◆ get_other_reachable_ids()

◆ get_parents_trans()

◆ ids_from_indices()

◆ populate()

Member Data Documentation

◆ nodes_by_name