CBMC
event_grapht::graph_conc_explorert Class Reference

#include <event_graph.h>

+ 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_graphtegraph
 
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_idtthin_air_events
 

Additional Inherited Members

- Public Attributes inherited from event_grapht::graph_explorert
std::map< event_idt, bool > mark
 
std::stack< event_idtmarked_stack
 
std::stack< event_idtpoint_stack
 
std::set< event_idtskip_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

◆ graph_conc_explorert()

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.

Member Function Documentation

◆ filtering()

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

Definition at line 344 of file event_graph.h.

◆ initial_filtering()

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.

Member Data Documentation

◆ filter

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: