CBMC
fence.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fences for instrumentation
4 
5 Author: Vincent Nimal
6 
7 Date: February 2012
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_FENCE_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_FENCE_H
16 
17 #include <goto-programs/goto_program.h>
18 
19 class namespacet;
20 
21 bool is_fence(
22  const goto_programt::instructiont &instruction,
23  const namespacet &ns);
24 
25 bool is_lwfence(
26  const goto_programt::instructiont &instruction,
27  const namespacet &ns);
28 
29 #endif // CPROVER_GOTO_INSTRUMENT_WMM_FENCE_H
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
is_fence
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:19
is_lwfence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:35
goto_program.h
Concrete Goto Program.