cprover
|
#include <cycles_visitor.h>
Public Member Functions | |
cycles_visitort (fence_insertert &_fi) | |
void | po_edges (std::set< event_idt > &edges) |
void | powr_constraint (const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges) |
void | poww_constraint (const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges) |
void | porw_constraint (const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges) |
void | porr_constraint (const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges) |
void | com_constraint (const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges) |
Protected Types | |
typedef event_grapht::critical_cyclet::delayt | edget |
Protected Attributes | |
fence_insertert & | fence_inserter |
Definition at line 21 of file cycles_visitor.h.
|
protected |
Definition at line 24 of file cycles_visitor.h.
|
inlineexplicit |
Definition at line 29 of file cycles_visitor.h.
References com_constraint(), po_edges(), porr_constraint(), porw_constraint(), powr_constraint(), and poww_constraint().
void cycles_visitort::com_constraint | ( | const event_grapht::critical_cyclet & | C_j, |
std::set< event_idt > & | edges | ||
) |
Definition at line 329 of file cycles_visitor.cpp.
References fence_insertert::add_invisible_edge(), fence_insertert::constraints_number, instrumentert::egraph, fence_inserter, fence_insertert::instrumenter, abstract_eventt::operation, abstract_eventt::Read, abstract_eventt::thread, event_grapht::critical_cyclet::unsafe_pairs, and abstract_eventt::Write.
Referenced by cycles_visitort(), and fence_insertert::preprocess().
void cycles_visitort::po_edges | ( | std::set< event_idt > & | edges | ) |
Definition at line 25 of file cycles_visitor.cpp.
References fence_insertert::add_edge(), event_grapht::are_po_ordered(), const_graph_visitort::const_graph_explore(), const_graph_visitort::const_graph_explore_AC(), const_graph_visitort::const_graph_explore_BC(), fence_insertert::const_graph_visitor, instrumentert::egraph, fence_inserter, fence_insertert::filter_cycles(), event_grapht::critical_cyclet::delayt::first, fence_insertert::instrumenter, is_fence(), event_grapht::critical_cyclet::delayt::is_po, fence_insertert::model, event_grapht::po_in(), event_grapht::po_out(), Power, event_grapht::critical_cyclet::delayt::second, instrumentert::set_of_cycles, and Unknown.
Referenced by cycles_visitort(), and fence_insertert::preprocess().
void cycles_visitort::porr_constraint | ( | const event_grapht::critical_cyclet & | C_j, |
std::set< event_idt > & | edges | ||
) |
Definition at line 309 of file cycles_visitor.cpp.
References fence_insertert::add_edge(), fence_insertert::constraints_number, instrumentert::egraph, fence_inserter, fence_insertert::instrumenter, abstract_eventt::Read, and event_grapht::critical_cyclet::unsafe_pairs.
Referenced by cycles_visitort(), and fence_insertert::preprocess().
void cycles_visitort::porw_constraint | ( | const event_grapht::critical_cyclet & | C_j, |
std::set< event_idt > & | edges | ||
) |
Definition at line 289 of file cycles_visitor.cpp.
References fence_insertert::add_edge(), fence_insertert::constraints_number, instrumentert::egraph, fence_inserter, fence_insertert::instrumenter, abstract_eventt::Read, event_grapht::critical_cyclet::unsafe_pairs, and abstract_eventt::Write.
Referenced by cycles_visitort(), and fence_insertert::preprocess().
void cycles_visitort::powr_constraint | ( | const event_grapht::critical_cyclet & | C_j, |
std::set< event_idt > & | edges | ||
) |
Definition at line 249 of file cycles_visitor.cpp.
References fence_insertert::add_edge(), fence_insertert::constraints_number, instrumentert::egraph, fence_inserter, fence_insertert::instrumenter, abstract_eventt::Read, event_grapht::critical_cyclet::unsafe_pairs, and abstract_eventt::Write.
Referenced by cycles_visitort(), and fence_insertert::preprocess().
void cycles_visitort::poww_constraint | ( | const event_grapht::critical_cyclet & | C_j, |
std::set< event_idt > & | edges | ||
) |
Definition at line 269 of file cycles_visitor.cpp.
References fence_insertert::add_edge(), fence_insertert::constraints_number, instrumentert::egraph, fence_inserter, fence_insertert::instrumenter, event_grapht::critical_cyclet::unsafe_pairs, and abstract_eventt::Write.
Referenced by cycles_visitort(), and fence_insertert::preprocess().
|
protected |
Definition at line 26 of file cycles_visitor.h.
Referenced by com_constraint(), po_edges(), porr_constraint(), porw_constraint(), powr_constraint(), and poww_constraint().