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() && ns.lookup(
23  to_code_function_call(instruction.code).function()).base_name == "fence")
24  /* if assembly-sensitive algorithms are not available */
25  || (instruction.is_other() && instruction.code.get_statement()==ID_fence
26  && instruction.code.get_bool(ID_WWfence)
27  && instruction.code.get_bool(ID_WRfence)
28  && instruction.code.get_bool(ID_RWfence)
29  && instruction.code.get_bool(ID_RRfence));
30 }
31 
33  const goto_programt::instructiont &instruction,
34  const namespacet &ns)
35 {
36  return (instruction.is_function_call() && ns.lookup(
37  to_code_function_call(instruction.code).function()).base_name == "lwfence")
38  /* if assembly-sensitive algorithms are not available */
39  || (instruction.is_other() && instruction.code.get_statement()==ID_fence
40  && instruction.code.get_bool(ID_WWfence)
41  && instruction.code.get_bool(ID_RWfence)
42  && instruction.code.get_bool(ID_RRfence));
43 }
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
TO_BE_DOCUMENTED.
Definition: namespace.h:62
exprt & function()
Definition: std_code.h:677
Fences for instrumentation.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:32