CBMC
Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | List of all members
event_grapht::graph_explorert Class Reference

#include <event_graph.h>

+ Inheritance diagram for event_grapht::graph_explorert:
+ Collaboration diagram for event_grapht::graph_explorert:

Public Member Functions

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...
 

Public Attributes

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

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...
 

Protected Attributes

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
 

Detailed Description

Definition at line 249 of file event_graph.h.

Constructor & Destructor Documentation

◆ ~graph_explorert()

virtual event_grapht::graph_explorert::~graph_explorert ( )
inlinevirtual

Definition at line 252 of file event_graph.h.

◆ graph_explorert()

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

Definition at line 293 of file event_graph.h.

Member Function Documentation

◆ backtrack()

bool event_grapht::graph_explorert::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

Definition at line 159 of file cycle_collection.cpp.

◆ collect_cycles()

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

Tarjan 1972 adapted and modified for events.

Definition at line 51 of file cycle_collection.cpp.

◆ extract_cycle()

event_grapht::critical_cyclet event_grapht::graph_explorert::extract_cycle ( event_idt  vertex,
event_idt  source,
unsigned  number 
)

extracts a (whole, unreduced) cycle from the stack.

Note: it may not be a real cycle yet – we cannot check the size before a call to this function.

Definition at line 119 of file cycle_collection.cpp.

◆ filter_thin_air()

void event_grapht::graph_explorert::filter_thin_air ( std::set< critical_cyclet > &  set_of_cycles)
protected

after the collection, eliminates the executions forbidden by an indirect thin-air

Definition at line 20 of file cycle_collection.cpp.

◆ filtering()

virtual bool event_grapht::graph_explorert::filtering ( event_idt  )
inlineprotectedvirtual

Definition at line 269 of file event_graph.h.

◆ order_filtering()

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

Definition at line 274 of file event_graph.h.

Member Data Documentation

◆ cycle_nb

unsigned event_grapht::graph_explorert::cycle_nb
protected

Definition at line 281 of file event_graph.h.

◆ egraph

event_grapht& event_grapht::graph_explorert::egraph
protected

Definition at line 257 of file event_graph.h.

◆ events_per_thread

std::map<unsigned, unsigned char> event_grapht::graph_explorert::events_per_thread
protected

Definition at line 266 of file event_graph.h.

◆ mark

std::map<event_idt, bool> event_grapht::graph_explorert::mark

Definition at line 305 of file event_graph.h.

◆ marked_stack

std::stack<event_idt> event_grapht::graph_explorert::marked_stack

Definition at line 306 of file event_graph.h.

◆ max_po_trans

unsigned event_grapht::graph_explorert::max_po_trans
protected

Definition at line 261 of file event_graph.h.

◆ max_var

unsigned event_grapht::graph_explorert::max_var
protected

Definition at line 260 of file event_graph.h.

◆ point_stack

std::stack<event_idt> event_grapht::graph_explorert::point_stack

Definition at line 307 of file event_graph.h.

◆ reads_per_variable

std::map<irep_idt, unsigned char> event_grapht::graph_explorert::reads_per_variable
protected

Definition at line 265 of file event_graph.h.

◆ skip_tracked

std::set<event_idt> event_grapht::graph_explorert::skip_tracked

Definition at line 309 of file event_graph.h.

◆ thin_air_events

std::set<event_idt> event_grapht::graph_explorert::thin_air_events
protected

Definition at line 286 of file event_graph.h.

◆ writes_per_variable

std::map<irep_idt, unsigned char> event_grapht::graph_explorert::writes_per_variable
protected

Definition at line 264 of file event_graph.h.

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