Inheritance diagram for event_grapht::graph_conc_explorert:

Collaboration diagram for event_grapht::graph_conc_explorert:

Public Member Functions
	graph_conc_explorert (event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans, const std::set< event_idt > &_filter)

bool	filtering (event_idt u)

std::list< event_idt > *	initial_filtering (std::list< event_idt > *order)

Public Member Functions inherited from event_grapht::graph_explorert
virtual	~graph_explorert ()

	graph_explorert (event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)

critical_cyclet	extract_cycle (event_idt vertex, event_idt source, unsigned number_of_cycles)
	extracts a (whole, unreduced) cycle from the stack. More...

bool	backtrack (std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwsync_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model)
	see event_grapht::collect_cycles More...

void	collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
	Tarjan 1972 adapted and modified for events. More...

Protected Attributes
const std::set< event_idt > &	filter

Protected Attributes inherited from event_grapht::graph_explorert
event_grapht &	egraph

unsigned	max_var

unsigned	max_po_trans

std::map< irep_idt, unsigned char >	writes_per_variable

std::map< irep_idt, unsigned char >	reads_per_variable

std::map< unsigned, unsigned char >	events_per_thread

unsigned	cycle_nb

std::set< event_idt >	thin_air_events

Additional Inherited Members
Public Attributes inherited from event_grapht::graph_explorert
std::map< event_idt, bool >	mark

std::stack< event_idt >	marked_stack

std::stack< event_idt >	point_stack

std::set< event_idt >	skip_tracked

Protected Member Functions inherited from event_grapht::graph_explorert
virtual bool	filtering (event_idt)

virtual std::list< event_idt > *	order_filtering (std::list< event_idt > *order)

void	filter_thin_air (std::set< critical_cyclet > &set_of_cycles)
	after the collection, eliminates the executions forbidden by an indirect thin-air More...

Detailed Description

Definition at line 332 of file event_graph.h.

Constructor & Destructor Documentation

event_grapht::graph_conc_explorert::graph_conc_explorert	(	event_grapht &	_egraph,
		unsigned	_max_var,
		unsigned	_max_po_trans,
		const std::set< event_idt > &	_filter
	)

inline

Definition at line 338 of file event_graph.h.

bool event_grapht::graph_conc_explorert::filtering ( event_idt u )

inline

Definition at line 344 of file event_graph.h.

std::list<event_idt>* event_grapht::graph_conc_explorert::initial_filtering ( std::list< event_idt > * order )

inline

Definition at line 349 of file event_graph.h.

const std::set<event_idt>& event_grapht::graph_conc_explorert::filter

protected

Definition at line 335 of file event_graph.h.

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

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