cprover
|
Public Member Functions | |
fence_all_sharedt (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 () |
![]() | |
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 127 of file fence_shared.cpp.
|
inline |
Definition at line 133 of file fence_shared.cpp.
|
protectedvirtual |
Implements simple_insertiont.
Reimplemented in fence_all_shared_aegt.
Definition at line 298 of file fence_shared.cpp.
References CPROVER_PREFIX, messaget::debug(), rw_set_with_trackt::dereferenced_from, 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_shared(), namespacet::lookup(), simple_insertiont::message, simple_insertiont::ns, rw_set_baset::entryt::object, rw_set_baset::r_entries, rw_set_with_trackt::set_reads, rw_set_baset::entryt::symbol_expr, simple_insertiont::value_sets, rw_set_baset::w_entries, and messaget::warning().