#include <cfg.h>

Inheritance diagram for concurrent_cfg_baset< T, P, I >:

Collaboration diagram for concurrent_cfg_baset< T, P, I >:

Protected Member Functions
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)

Protected Member Functions inherited from cfg_baset< T, const goto_programt, goto_programt::const_targett >
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, goto_programt::const_targett PC)

void	compute_edges (const goto_functionst &goto_functions, const goto_programt &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	shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const

std::vector< typename N::node_indext >	depth_limited_search (std::vector< typename N::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

Additional Inherited Members
Public Types inherited from cfg_baset< T, const goto_programt, goto_programt::const_targett >
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_targett >	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 inherited from cfg_baset< T, const goto_programt, goto_programt::const_targett >
	cfg_baset ()

virtual	~cfg_baset ()

void	operator() (const goto_functionst &goto_functions)

void	operator() (const goto_programt &goto_program)

entryt	get_node_index (const goto_programt::const_targett &program_point) const
	Get the graph node index for `program_point`. More...

nodet &	get_node (const goto_programt::const_targett &program_point)
	Get the CFG graph node relating to `program_point`. More...

const nodet &	get_node (const goto_programt::const_targett &program_point) const
	Get the CFG graph node relating to `program_point`. More...

const entry_mapt &	entries () const
	Get a map from program points to their corresponding node indices. More...

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 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 N::node_indext >	depth_limited_search (typename N::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 N::node_indext >	depth_limited_search (std::vector< typename N::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

Static Public Member Functions inherited from cfg_baset< T, const goto_programt, goto_programt::const_targett >
static goto_programt::const_targett	get_first_node (const goto_programt &program)

static goto_programt::const_targett	get_last_node (const goto_programt &program)

static bool	nodes_empty (const goto_programt &program)

Public Attributes inherited from cfg_baset< T, const goto_programt, goto_programt::const_targett >
entry_mapt	entry_map

Protected Attributes inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
nodest	nodes

Detailed Description

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
class concurrent_cfg_baset< T, P, I >

Definition at line 281 of file cfg.h.

Member Function Documentation

◆ compute_edges_start_thread()

template<class T , typename P , typename I >

void concurrent_cfg_baset< T, P, I >::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
	)

protectedvirtual

Definition at line 371 of file cfg.h.

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

/home/runner/work/cbmc/cbmc/src/goto-programs/cfg.h

Protected Member Functions

Additional Inherited Members

Detailed Description

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett> class concurrent_cfg_baset< T, P, I >

Member Function Documentation

◆ compute_edges_start_thread()

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
class concurrent_cfg_baset< T, P, I >