cprover
|
#include <event_graph.h>
Public Member Functions | |
graph_pensieve_explorert (event_grapht &_egraph, unsigned _max_var, unsigned _max_po_trans) | |
void | set_naive () |
void | collect_pairs (namespacet &ns) |
![]() | |
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 Member Functions | |
bool | find_second_event (event_idt source) |
![]() | |
virtual bool | filtering (event_idt u) |
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 | |
std::set< event_idt > | visited_nodes |
bool | naive |
![]() | |
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 | |
![]() | |
std::map< event_idt, bool > | mark |
std::stack< event_idt > | marked_stack |
std::stack< event_idt > | point_stack |
std::set< event_idt > | skip_tracked |
Definition at line 328 of file event_graph.h.
|
inline |
Definition at line 337 of file event_graph.h.
void event_grapht::graph_pensieve_explorert::collect_pairs | ( | namespacet & | ns | ) |
Definition at line 25 of file pair_collection.cpp.
References event_grapht::com_out(), messaget::debug(), event_grapht::graph_explorert::egraph, messaget::eom(), find_second_event(), source_locationt::get_file(), source_locationt::get_line(), event_grapht::message, naive, abstract_eventt::operation, OUTPUT, event_grapht::po_order, abstract_eventt::source_location, abstract_eventt::variable, visited_nodes, and messaget::warning().
Referenced by event_grapht::collect_pairs(), and event_grapht::collect_pairs_naive().
|
protected |
Definition at line 67 of file pair_collection.cpp.
Referenced by collect_pairs().
|
inline |
Definition at line 342 of file event_graph.h.
References naive.
Referenced by event_grapht::collect_pairs_naive().
|
protected |
Definition at line 332 of file event_graph.h.
Referenced by collect_pairs(), and set_naive().
|
protected |
Definition at line 331 of file event_graph.h.
Referenced by collect_pairs().