cprover
fence_assert.cpp
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 #include "fence_assert.h"
14 
16  const event_grapht::critical_cyclet &cycle) const
17 {
18  /* TODO */
19  return true;
20 }
21 
23 {
24  for(std::set<event_grapht::critical_cyclet>::const_iterator
25  C_j=instrumenter.set_of_cycles.begin();
26  C_j!=instrumenter.set_of_cycles.end();
27  ++C_j)
28  {
29  if( find_assert(*C_j) )
30  selected_cycles.insert(C_j->id);
31  }
32 }
virtual void process_cycles_selection()
bool find_assert(const event_grapht::critical_cyclet &cycle) const
ILP construction for cycles affecting user-assertions and resolution.
std::set< unsigned > selected_cycles
Definition: fence_assert.h:27
instrumentert & instrumenter
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:289