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 }
const irep_idt & get_statement() const
Definition: std_code.h:40
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
exprt & function()
Definition: std_code.h:878
Fences for instrumentation.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:36