cprover
cycles_visitor.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: cycles visitor for computing edges involved for fencing
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_MUSKETEER_CYCLES_VISITOR_H
13 #define CPROVER_MUSKETEER_CYCLES_VISITOR_H
14 
15 #include <set>
16 
18 
19 class fence_insertert;
20 
22 {
23 protected:
25 
27 
28 public:
30  : fence_inserter(_fi)
31  {}
32 
33  /* computes po^+ edges in U{C_1, ..., C_j} */
34  void po_edges(std::set<event_idt> &edges);
35 
36  /* computes pairs that will be protected for the
37  TSO/PSO/RMO/Power/ARM by the constraints */
39  std::set<event_idt> &edges);
41  std::set<event_idt> &edges);
43  std::set<event_idt> &edges);
45  std::set<event_idt> &edges);
47  std::set<event_idt> &edges);
48 };
49 
50 #endif // CPROVER_MUSKETEER_CYCLES_VISITOR_H
graph of abstract events
void poww_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
void powr_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
void po_edges(std::set< event_idt > &edges)
cycles_visitort(fence_insertert &_fi)
void porr_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)
fence_insertert & fence_inserter
void com_constraint(const event_grapht::critical_cyclet &C_j, std::set< event_idt > &edges)
event_grapht::critical_cyclet::delayt edget