cprover
|
Public Member 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 | |
virtual void | compute ()=0 |
void | print_to_file () const |
Protected Attributes | |
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 35 of file fence_shared.cpp.
|
inlineexplicit |
Definition at line 108 of file fence_shared.cpp.
|
inlinevirtual |
Definition at line 117 of file fence_shared.cpp.
|
protectedpure virtual |
Implemented in fence_volatilet, fence_all_shared_aegt, and fence_all_sharedt.
Referenced by do_it().
|
inline |
Definition at line 119 of file fence_shared.cpp.
References compute(), and print_to_file().
Referenced by fence_all_shared(), fence_all_shared_aeg(), and fence_volatile().
|
inlineprotected |
Definition at line 53 of file fence_shared.cpp.
References fenced_edges, namespacet::lookup(), ns, and OUTPUT.
Referenced by do_it().
struct { ... } simple_insertiont::fenced_edges |
|
protected |
Definition at line 42 of file fence_shared.cpp.
Referenced by fence_all_sharedt::compute(), fence_all_shared_aegt::compute(), fence_volatilet::compute(), and fence_all_shared_aegt::fence_all_shared_aeg_explore().
|
protected |
Definition at line 38 of file fence_shared.cpp.
Referenced by fence_all_sharedt::compute(), fence_all_shared_aegt::compute(), fence_volatilet::compute(), and fence_all_shared_aegt::fence_all_shared_aeg_explore().
|
protected |
Definition at line 41 of file fence_shared.cpp.
Referenced by fence_all_sharedt::compute(), fence_volatilet::compute(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), and print_to_file().
std::list<symbol_exprt> simple_insertiont::reads |
Definition at line 47 of file fence_shared.cpp.
|
protected |
Definition at line 40 of file fence_shared.cpp.
Referenced by fence_volatilet::is_volatile().
|
protected |
Definition at line 39 of file fence_shared.cpp.
Referenced by fence_all_sharedt::compute(), fence_volatilet::compute(), and fence_all_shared_aegt::fence_all_shared_aeg_explore().
std::list<symbol_exprt> simple_insertiont::writes |
Definition at line 46 of file fence_shared.cpp.