#include <event_graph.h>

Collaboration diagram for event_grapht:

Classes
class	critical_cyclet

class	graph_conc_explorert

class	graph_explorert

class	graph_pensieve_explorert

Public Member Functions
	event_grapht (messaget &_message)

event_idt	add_node ()

grapht< abstract_eventt >::nodet &	operator[] (event_idt n)

bool	has_po_edge (event_idt i, event_idt j) const

bool	has_com_edge (event_idt i, event_idt j) const

std::size_t	size () const

const wmm_grapht::edgest &	po_in (event_idt n) const

const wmm_grapht::edgest &	po_out (event_idt n) const

const wmm_grapht::edgest &	com_in (event_idt n) const

const wmm_grapht::edgest &	com_out (event_idt n) const

void	add_po_edge (event_idt a, event_idt b)

void	add_po_back_edge (event_idt a, event_idt b)

void	add_com_edge (event_idt a, event_idt b)

void	add_undirected_com_edge (event_idt a, event_idt b)

void	remove_po_edge (event_idt a, event_idt b)

void	remove_com_edge (event_idt a, event_idt b)

void	remove_edge (event_idt a, event_idt b)

void	explore_copy_segment (std::set< event_idt > &explored, event_idt begin, event_idt end) const
	copies the segment

event_idt	copy_segment (event_idt begin, event_idt end)

bool	is_local (event_idt a)

bool	are_po_ordered (event_idt a, event_idt b)

void	clear ()

void	print_graph ()

void	print_rec_graph (std::ofstream &file, event_idt node_id, std::set< event_idt > &visited)

void	collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)

void	collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model)

void	set_parameters_collection (unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)

void	collect_pairs ()

void	collect_pairs_naive ()

Public Attributes
bool	filter_thin_air

bool	filter_uniproc

messaget &	message

std::map< unsigned, data_dpt >	map_data_dp

std::list< event_idt >	po_order

std::list< event_idt >	poUrfe_order

std::set< std::pair< event_idt, event_idt > >	loops

std::set< std::pair< const abstract_eventt &, const abstract_eventt & > >	duplicated_bodies

Protected Attributes
wmm_grapht	po_graph

wmm_grapht	com_graph

unsigned	max_var

unsigned	max_po_trans

bool	ignore_arrays

Detailed Description

Definition at line 34 of file event_graph.h.

Constructor & Destructor Documentation

◆ event_grapht()

event_grapht::event_grapht ( messaget & _message )

inlineexplicit

Definition at line 382 of file event_graph.h.

Member Function Documentation

◆ add_com_edge()

void event_grapht::add_com_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 473 of file event_graph.h.

◆ add_node()

event_idt event_grapht::add_node ( )

inline

Definition at line 405 of file event_graph.h.

◆ add_po_back_edge()

void event_grapht::add_po_back_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 462 of file event_graph.h.

◆ add_po_edge()

void event_grapht::add_po_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 453 of file event_graph.h.

◆ add_undirected_com_edge()

void event_grapht::add_undirected_com_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 480 of file event_graph.h.

◆ are_po_ordered()

bool event_grapht::are_po_ordered	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 519 of file event_graph.h.

◆ clear()

void event_grapht::clear ( )

inline

Definition at line 538 of file event_graph.h.

◆ collect_cycles() [1/2]

void event_grapht::collect_cycles	(	std::set< critical_cyclet > &	set_of_cycles,
		memory_modelt	model
	)

inline

Definition at line 559 of file event_graph.h.

◆ collect_cycles() [2/2]

void event_grapht::collect_cycles	(	std::set< critical_cyclet > &	set_of_cycles,
		memory_modelt	model,
		const std::set< event_idt > &	filter
	)

inline

Definition at line 551 of file event_graph.h.

◆ collect_pairs()

void event_grapht::collect_pairs ( )

inline

Definition at line 578 of file event_graph.h.

◆ collect_pairs_naive()

void event_grapht::collect_pairs_naive ( )

inline

Definition at line 584 of file event_graph.h.

◆ com_in()

const wmm_grapht::edgest & event_grapht::com_in ( event_idt n ) const

inline

Definition at line 443 of file event_graph.h.

◆ com_out()

const wmm_grapht::edgest & event_grapht::com_out ( event_idt n ) const

inline

Definition at line 448 of file event_graph.h.

◆ copy_segment()

event_idt event_grapht::copy_segment	(	event_idt	begin,
		event_idt	end
	)

Definition at line 91 of file event_graph.cpp.

◆ explore_copy_segment()

void event_grapht::explore_copy_segment	(	std::set< event_idt > &	explored,
		event_idt	begin,
		event_idt	end
	)		const

copies the segment

Parameters

begin	top of the subgraph
explored	set of segments which have already been explored
end	bottom of the subgraph

Definition at line 73 of file event_graph.cpp.

◆ has_com_edge()

bool event_grapht::has_com_edge	(	event_idt	i,
		event_idt	j
	)		const

inline

Definition at line 423 of file event_graph.h.

◆ has_po_edge()

bool event_grapht::has_po_edge	(	event_idt	i,
		event_idt	j
	)		const

inline

Definition at line 418 of file event_graph.h.

◆ is_local()

bool event_grapht::is_local ( event_idt a )

inline

Definition at line 513 of file event_graph.h.

◆ operator[]()

grapht< abstract_eventt >::nodet & event_grapht::operator[] ( event_idt n )

inline

Definition at line 413 of file event_graph.h.

◆ po_in()

const wmm_grapht::edgest & event_grapht::po_in ( event_idt n ) const

inline

Definition at line 433 of file event_graph.h.

◆ po_out()

const wmm_grapht::edgest & event_grapht::po_out ( event_idt n ) const

inline

Definition at line 438 of file event_graph.h.

◆ print_graph()

void event_grapht::print_graph ( )

Definition at line 56 of file event_graph.cpp.

◆ print_rec_graph()

void event_grapht::print_rec_graph	(	std::ofstream &	file,
		event_idt	node_id,
		std::set< event_idt > &	visited
	)

Definition at line 28 of file event_graph.cpp.

◆ remove_com_edge()

void event_grapht::remove_com_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 492 of file event_graph.h.

◆ remove_edge()

void event_grapht::remove_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 497 of file event_graph.h.

◆ remove_po_edge()

void event_grapht::remove_po_edge	(	event_idt	a,
		event_idt	b
	)

inline

Definition at line 487 of file event_graph.h.

◆ set_parameters_collection()

void event_grapht::set_parameters_collection	(	unsigned	_max_var = `0`,
		unsigned	_max_po_trans = `0`,
		bool	_ignore_arrays = `false`
	)

inline

Definition at line 566 of file event_graph.h.

◆ size()

std::size_t event_grapht::size ( ) const

inline

Definition at line 428 of file event_graph.h.

Member Data Documentation

◆ com_graph

wmm_grapht event_grapht::com_graph

protected

Definition at line 241 of file event_graph.h.

◆ duplicated_bodies

std::set<std::pair<const abstract_eventt&, const abstract_eventt&> > event_grapht::duplicated_bodies

Definition at line 511 of file event_graph.h.

◆ filter_thin_air

bool event_grapht::filter_thin_air

Definition at line 392 of file event_graph.h.

◆ filter_uniproc

bool event_grapht::filter_uniproc

Definition at line 393 of file event_graph.h.

◆ ignore_arrays

bool event_grapht::ignore_arrays

protected

Definition at line 246 of file event_graph.h.

◆ loops

std::set<std::pair<event_idt, event_idt> > event_grapht::loops

Definition at line 403 of file event_graph.h.

◆ map_data_dp

std::map<unsigned, data_dpt> event_grapht::map_data_dp

Definition at line 397 of file event_graph.h.

◆ max_po_trans

unsigned event_grapht::max_po_trans

protected

Definition at line 245 of file event_graph.h.

◆ max_var

unsigned event_grapht::max_var

protected

Definition at line 244 of file event_graph.h.

◆ message

messaget& event_grapht::message

Definition at line 394 of file event_graph.h.

◆ po_graph

wmm_grapht event_grapht::po_graph

protected

Definition at line 240 of file event_graph.h.

◆ po_order

std::list<event_idt> event_grapht::po_order

Definition at line 400 of file event_graph.h.

◆ poUrfe_order

std::list<event_idt> event_grapht::poUrfe_order

Definition at line 401 of file event_graph.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/event_graph.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/event_graph.cpp

Classes

Public Member Functions

Public Attributes

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ event_grapht()

Member Function Documentation

◆ add_com_edge()

◆ add_node()

◆ add_po_back_edge()

◆ add_po_edge()

◆ add_undirected_com_edge()

◆ are_po_ordered()

◆ clear()

◆ collect_cycles() [1/2]

◆ collect_cycles() [2/2]

◆ collect_pairs()

◆ collect_pairs_naive()

◆ com_in()

◆ com_out()

◆ copy_segment()

◆ explore_copy_segment()

◆ has_com_edge()

◆ has_po_edge()

◆ is_local()

◆ operator[]()

◆ po_in()

◆ po_out()

◆ print_graph()

◆ print_rec_graph()

◆ remove_com_edge()

◆ remove_edge()

◆ remove_po_edge()

◆ set_parameters_collection()

◆ size()

Member Data Documentation

◆ com_graph

◆ duplicated_bodies

◆ filter_thin_air

◆ filter_uniproc

◆ ignore_arrays

◆ loops

◆ map_data_dp

◆ max_po_trans

◆ max_var

◆ message

◆ po_graph

◆ po_order

◆ poUrfe_order