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(to_symbol_expr(instruction.get_function_call().function()))
24  .base_name == "fence")
25  /* if assembly-sensitive algorithms are not available */
26  || (instruction.is_other() &&
27  instruction.get_code().get_statement() == ID_fence &&
28  instruction.get_code().get_bool(ID_WWfence) &&
29  instruction.get_code().get_bool(ID_WRfence) &&
30  instruction.get_code().get_bool(ID_RWfence) &&
31  instruction.get_code().get_bool(ID_RRfence));
32 }
33 
35  const goto_programt::instructiont &instruction,
36  const namespacet &ns)
37 {
38  return (instruction.is_function_call() &&
39  ns.lookup(to_symbol_expr(instruction.get_function_call().function()))
40  .base_name == "lwfence")
41  /* if assembly-sensitive algorithms are not available */
42  || (instruction.is_other() &&
43  instruction.get_code().get_statement() == ID_fence &&
44  instruction.get_code().get_bool(ID_WWfence) &&
45  instruction.get_code().get_bool(ID_RWfence) &&
46  instruction.get_code().get_bool(ID_RRfence));
47 }
is_lwfence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:34
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:450
namespace.h
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
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:141
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:319
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
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:445
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
code_function_callt::function
exprt & function()
Definition: std_code.h:1250