cprover
fence_user_def.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_user_def.h"
14 
16  const event_grapht::critical_cyclet &cycle) const
17 {
18  /* DEPRECATED: user-inserted fences now detected at cycle collection */
19  #if 0
20  /* if a fence already appears in the representation of the cycle, ok */
21  for(event_grapht::critical_cyclet::const_iterator it=cycle.begin();
22  it!=cycle.end(); ++it)
23  if(egraph[*it].is_fence())
24  return true;
25 
26  /* we collect the fences back in the graph; indeed, in the cycles we extract,
27  it is possible that some lwfence have been ignored, as they had no effect
28  (in the case of WR) */
29  #endif
30 
31  return cycle.has_user_defined_fence;
32 }
33 
35 {
36  for(std::set<event_grapht::critical_cyclet>::const_iterator
37  C_j=instrumenter.set_of_cycles.begin();
38  C_j!=instrumenter.set_of_cycles.end();
39  ++C_j)
40  {
41  if( contains_user_def(*C_j) )
42  selected_cycles.insert(C_j->id);
43  }
44 }
bool contains_user_def(const event_grapht::critical_cyclet &cycle) const
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
std::set< unsigned > selected_cycles
ILP construction for cycles containing user-placed fences and resolution.
instrumentert & instrumenter
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:289
virtual void process_cycles_selection()