cprover
fence.cpp
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 #include "fence.h"
15 
16 #include <util/namespace.h>
17 
18 bool is_fence(
19  const goto_programt::instructiont &instruction,
20  const namespacet &ns)
21 {
22  return (instruction.is_function_call() &&
23  ns.lookup(
25  to_code_function_call(instruction.code).function()))
26  .base_name == "fence")
27  /* if assembly-sensitive algorithms are not available */
28  || (instruction.is_other() &&
29  instruction.code.get_statement() == ID_fence &&
30  instruction.code.get_bool(ID_WWfence) &&
31  instruction.code.get_bool(ID_WRfence) &&
32  instruction.code.get_bool(ID_RWfence) &&
33  instruction.code.get_bool(ID_RRfence));
34 }
35 
37  const goto_programt::instructiont &instruction,
38  const namespacet &ns)
39 {
40  return (instruction.is_function_call() &&
41  ns.lookup(
43  to_code_function_call(instruction.code).function()))
44  .base_name == "lwfence")
45  /* if assembly-sensitive algorithms are not available */
46  || (instruction.is_other() &&
47  instruction.code.get_statement() == ID_fence &&
48  instruction.code.get_bool(ID_WWfence) &&
49  instruction.code.get_bool(ID_RWfence) &&
50  instruction.code.get_bool(ID_RRfence));
51 }
is_lwfence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:36
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:466
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
is_fence
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
fence.h
Fences for instrumentation.
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
code_function_callt::function
exprt & function()
Definition: std_code.h:1218