cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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.
code
().
get_statement
() == ID_fence &&
29
instruction.
code
().
get_bool
(ID_WWfence) &&
30
instruction.
code
().
get_bool
(ID_WRfence) &&
31
instruction.
code
().
get_bool
(ID_RWfence) &&
32
instruction.
code
().
get_bool
(ID_RRfence));
33
}
34
35
bool
is_lwfence
(
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.
code
().
get_statement
() == ID_fence &&
45
instruction.
code
().
get_bool
(ID_WWfence) &&
46
instruction.
code
().
get_bool
(ID_RWfence) &&
47
instruction.
code
().
get_bool
(ID_RRfence));
48
}
codet::get_statement
const irep_idt & get_statement() const
Definition
std_code_base.h:65
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition
goto_program.h:180
goto_programt::instructiont::code
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Definition
goto_program.h:187
goto_programt::instructiont::is_other
bool is_other() const
Definition
goto_program.h:498
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition
goto_program.h:271
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition
goto_program.h:493
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition
irep.cpp:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition
namespace.cpp:134
is_fence
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition
fence.cpp:19
is_lwfence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition
fence.cpp:35
fence.h
Fences for instrumentation.
namespace.h
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition
std_expr.h:211
symbol.h
Symbol table entry.
goto-instrument
wmm
fence.cpp
Generated by
1.17.0