cprover
|
Fences for instrumentation. More...
#include <goto-programs/goto_program.h>
Go to the source code of this file.
Functions | |
bool | is_fence (const goto_programt::instructiont &instruction, const namespacet &ns) |
bool | is_lwfence (const goto_programt::instructiont &instruction, const namespacet &ns) |
Fences for instrumentation.
Definition in file fence.h.
bool is_fence | ( | const goto_programt::instructiont & | instruction, |
const namespacet & | ns | ||
) |
Definition at line 18 of file fence.cpp.
References goto_programt::instructiont::code, code_function_callt::function(), irept::get_bool(), codet::get_statement(), goto_programt::instructiont::is_function_call(), goto_programt::instructiont::is_other(), namespacet::lookup(), to_code_function_call(), and to_symbol_expr().
Referenced by instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().
bool is_lwfence | ( | const goto_programt::instructiont & | instruction, |
const namespacet & | ns | ||
) |
Definition at line 36 of file fence.cpp.
References goto_programt::instructiont::code, code_function_callt::function(), irept::get_bool(), codet::get_statement(), goto_programt::instructiont::is_function_call(), goto_programt::instructiont::is_other(), namespacet::lookup(), to_code_function_call(), and to_symbol_expr().
Referenced by event_grapht::graph_explorert::backtrack(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().