cprover
fence_user_def.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ILP construction for cycles containing user-placed fences
4  and resolution
5 
6 Author: Vincent Nimal
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_MUSKETEER_FENCE_USER_DEF_H
14 #define CPROVER_MUSKETEER_FENCE_USER_DEF_H
15 
16 #include <set>
17 
19 
20 #include "fence_inserter.h"
21 
22 class instrumentert;
23 
25 {
26 protected:
27  std::set<unsigned> selected_cycles;
28 
29  bool contains_user_def(const event_grapht::critical_cyclet &cycle) const;
30 
31  // overload for base class
32  virtual void process_cycles_selection();
33 
34  // overload for base class
35  virtual bool filter_cycles(unsigned cycles_id) const
36  {
37  return selected_cycles.find(cycles_id)==selected_cycles.end();
38  }
39 
40 public:
42  fence_insertert(instr)
43  {
44  }
45 
47  fence_insertert(instr, _model)
48  {
49  }
50 };
51 
52 #endif // CPROVER_MUSKETEER_FENCE_USER_DEF_H
bool contains_user_def(const event_grapht::critical_cyclet &cycle) const
graph of abstract events
std::set< unsigned > selected_cycles
fence_user_def_insertert(instrumentert &instr, memory_modelt _model)
memory_modelt
Definition: wmm.h:17
virtual bool filter_cycles(unsigned cycles_id) const
fence_user_def_insertert(instrumentert &instr)
ILP construction for all cycles and resolution.
virtual void process_cycles_selection()