CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
fence.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Fences for instrumentation
4
5Author: Vincent Nimal
6
7Date: 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
19class namespacet;
20
21bool is_fence(
22 const goto_programt::instructiont &instruction,
23 const namespacet &ns);
24
25bool 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:91
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.