cprover
|
Public Member Functions | |
fence_all_shared_aegt (messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_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 | fence_all_shared_aeg_explore (const goto_programt &code) |
![]() | |
void | print_to_file () const |
Protected Attributes | |
std::set< irep_idt > | visited_functions |
![]() | |
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 143 of file fence_shared.cpp.
|
inline |
Definition at line 155 of file fence_shared.cpp.
|
protectedvirtual |
Reimplemented from fence_all_sharedt.
Definition at line 415 of file fence_shared.cpp.
References goto_function_templatet< bodyT >::body, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), goto_functions_templatet< bodyT >::function_map, simple_insertiont::goto_functions, main(), simple_insertiont::message, and messaget::status().
|
protected |
Definition at line 432 of file fence_shared.cpp.
References CPROVER_PREFIX, messaget::debug(), rw_set_with_trackt::dereferenced_from, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), simple_insertiont::fenced_edges, forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, symbol_exprt::get_identifier(), simple_insertiont::goto_functions, has_prefix(), irept::id(), 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, to_code_function_call(), to_symbol_expr(), symbolt::type, simple_insertiont::value_sets, rw_set_baset::w_entries, and messaget::warning().
|
protected |
Definition at line 147 of file fence_shared.cpp.