#include <event_graph.h>
|
| 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) |
|
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...
|
|
Definition at line 332 of file event_graph.h.
◆ 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 |
◆ filtering()
bool event_grapht::graph_conc_explorert::filtering |
( |
event_idt |
u | ) |
|
|
inline |
◆ initial_filtering()
std::list<event_idt>* event_grapht::graph_conc_explorert::initial_filtering |
( |
std::list< event_idt > * |
order | ) |
|
|
inline |
◆ filter
const std::set<event_idt>& event_grapht::graph_conc_explorert::filter |
|
protected |
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/event_graph.h