CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
fence.cpp
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#include "fence.h"
15
16#include <util/namespace.h>
17#include <util/symbol.h>
18
19bool is_fence(
20 const goto_programt::instructiont &instruction,
21 const namespacet &ns)
22{
23 return (instruction.is_function_call() &&
24 ns.lookup(to_symbol_expr(instruction.call_function())).base_name ==
25 "fence")
26 /* if assembly-sensitive algorithms are not available */
27 || (instruction.is_other() &&
28 instruction.code().get_statement() == ID_fence &&
29 instruction.code().get_bool(ID_WWfence) &&
30 instruction.code().get_bool(ID_WRfence) &&
31 instruction.code().get_bool(ID_RWfence) &&
32 instruction.code().get_bool(ID_RRfence));
33}
34
35bool is_lwfence(
36 const goto_programt::instructiont &instruction,
37 const namespacet &ns)
38{
39 return (instruction.is_function_call() &&
40 ns.lookup(to_symbol_expr(instruction.call_function())).base_name ==
41 "lwfence")
42 /* if assembly-sensitive algorithms are not available */
43 || (instruction.is_other() &&
44 instruction.code().get_statement() == ID_fence &&
45 instruction.code().get_bool(ID_WWfence) &&
46 instruction.code().get_bool(ID_RWfence) &&
47 instruction.code().get_bool(ID_RRfence));
48}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition goto_program.h:181
goto_programt::instructiont::code
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Definition goto_program.h:188
goto_programt::instructiont::is_other
bool is_other() const
Definition goto_program.h:499
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition goto_program.h:272
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition goto_program.h:494
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition namespace.cpp:134
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
fence.h
Fences for instrumentation.
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
symbol.h
Symbol table entry.