cprover
fence_assert.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ILP construction for cycles affecting user-assertions
4  and resolution
5 
6 Author: Vincent Nimal
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_MUSKETEER_FENCE_ASSERT_H
14 #define CPROVER_MUSKETEER_FENCE_ASSERT_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 find_assert(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_ASSERT_H
virtual void process_cycles_selection()
graph of abstract events
memory_modelt
Definition: wmm.h:17
bool find_assert(const event_grapht::critical_cyclet &cycle) const
std::set< unsigned > selected_cycles
Definition: fence_assert.h:27
virtual bool filter_cycles(unsigned cycles_id) const
Definition: fence_assert.h:35
fence_assert_insertert(instrumentert &instr, memory_modelt _model)
Definition: fence_assert.h:46
ILP construction for all cycles and resolution.
fence_assert_insertert(instrumentert &instr)
Definition: fence_assert.h:41