CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
event_grapht::graph_pensieve_explorert Class Reference

#include <event_graph.h>

+ Inheritance diagram for event_grapht::graph_pensieve_explorert:
+ Collaboration diagram for event_grapht::graph_pensieve_explorert:

Public Member Functions

 graph_pensieve_explorert (event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans)
 
void set_naive ()
 
void collect_pairs ()
 
- 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.
 
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
 
void collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
 Tarjan 1972 adapted and modified for events.
 

Protected Member Functions

bool find_second_event (event_idt source)
 
- 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
 

Protected Attributes

std::set< event_idt > visited_nodes
 
bool naive
 
- 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
 

Detailed Description

Definition at line 363 of file event_graph.h.

Constructor & Destructor Documentation

◆ graph_pensieve_explorert()

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

Definition at line 372 of file event_graph.h.

Member Function Documentation

◆ collect_pairs()

void event_grapht::graph_pensieve_explorert::collect_pairs ( )

Definition at line 25 of file pair_collection.cpp.

◆ find_second_event()

bool event_grapht::graph_pensieve_explorert::find_second_event ( event_idt  source)
protected

Definition at line 67 of file pair_collection.cpp.

◆ set_naive()

void event_grapht::graph_pensieve_explorert::set_naive ( )
inline

Definition at line 377 of file event_graph.h.

Member Data Documentation

◆ naive

bool event_grapht::graph_pensieve_explorert::naive
protected

Definition at line 367 of file event_graph.h.

◆ visited_nodes

std::set<event_idt> event_grapht::graph_pensieve_explorert::visited_nodes
protected

Definition at line 366 of file event_graph.h.

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