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 #include <util/symbol.h>
18 
19 bool 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.get_code().get_statement() == ID_fence &&
29  instruction.get_code().get_bool(ID_WWfence) &&
30  instruction.get_code().get_bool(ID_WRfence) &&
31  instruction.get_code().get_bool(ID_RWfence) &&
32  instruction.get_code().get_bool(ID_RRfence));
33 }
34 
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.get_code().get_statement() == ID_fence &&
45  instruction.get_code().get_bool(ID_WWfence) &&
46  instruction.get_code().get_bool(ID_RWfence) &&
47  instruction.get_code().get_bool(ID_RRfence));
48 }
is_lwfence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:35
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:535
namespace.h
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:185
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
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
symbol.h
Symbol table entry.
fence.h
Fences for instrumentation.
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:69
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:361