cprover
|
Public Member Functions | |
fence_volatilet (messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions) | |
![]() | |
simple_insertiont (messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions) | |
virtual | ~simple_insertiont () |
void | do_it () |
Protected Member Functions | |
void | compute () |
bool | is_volatile (const typet &src) const |
we can determine whether an access is volatile just by looking at the type of the variables involved in the expression. More... | |
![]() | |
void | print_to_file () const |
Additional Inherited Members | |
![]() | |
messaget & | message |
value_setst & | value_sets |
const symbol_tablet & | symbol_table |
const namespacet | ns |
const goto_functionst & | goto_functions |
struct { | |
std::list< symbol_exprt > writes | |
std::list< symbol_exprt > reads | |
} | fenced_edges |
Definition at line 165 of file fence_shared.cpp.
|
inline |
Definition at line 172 of file fence_shared.cpp.
|
protectedvirtual |
Implements simple_insertiont.
Definition at line 225 of file fence_shared.cpp.
References CPROVER_PREFIX, messaget::debug(), messaget::eom(), simple_insertiont::fenced_edges, forall_goto_functions, forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, simple_insertiont::goto_functions, has_prefix(), id2string(), symbolt::is_thread_local, is_volatile(), symbolt::is_volatile, namespacet::lookup(), simple_insertiont::message, simple_insertiont::ns, symbolt::type, simple_insertiont::value_sets, and messaget::warning().
|
protected |
we can determine whether an access is volatile just by looking at the type of the variables involved in the expression.
We assume that the program is correctly typed (i.e., volatile-marked)
Definition at line 184 of file fence_shared.cpp.
References irept::get_bool(), typet::has_subtype(), typet::has_subtypes(), irept::id(), is_volatile(), typet::subtype(), typet::subtypes(), simple_insertiont::symbol_table, symbol_tablet::symbols, and to_symbol_type().