cprover
|
#include <memory_model_tso.h>
Public Member Functions | |
memory_model_tsot (const namespacet &_ns) | |
virtual void | operator() (symex_target_equationt &equation) |
![]() | |
memory_model_sct (const namespacet &_ns) | |
![]() | |
memory_model_baset (const namespacet &_ns) | |
virtual | ~memory_model_baset () |
![]() | |
partial_order_concurrencyt (const namespacet &_ns) | |
virtual | ~partial_order_concurrencyt () |
Definition at line 17 of file memory_model_tso.h.
|
inlineexplicit |
Definition at line 20 of file memory_model_tso.h.
Reimplemented from memory_model_sct.
Definition at line 32 of file memory_model_tso.cpp.
References partial_order_concurrencyt::AX_PROPAGATION, partial_order_concurrencyt::AX_SC_PER_LOCATION, and partial_order_concurrencyt::before().
Referenced by program_order().
|
virtual |
Reimplemented from memory_model_sct.
Reimplemented in memory_model_psot.
Definition at line 17 of file memory_model_tso.cpp.
References partial_order_concurrencyt::build_clock_type(), partial_order_concurrencyt::build_event_lists(), messaget::eom(), memory_model_sct::from_read(), program_order(), memory_model_baset::read_from(), messaget::statistics(), and memory_model_sct::write_serialization_external().
|
protected |
Definition at line 54 of file memory_model_tso.cpp.
References partial_order_concurrencyt::add_constraint(), partial_order_concurrencyt::address(), partial_order_concurrencyt::AX_PROPAGATION, partial_order_concurrencyt::AX_SC_PER_LOCATION, before(), partial_order_concurrencyt::before(), memory_model_sct::build_per_thread_map(), irept::get_bool(), exprt::is_false(), irept::is_nil(), exprt::make_false(), partial_order_concurrencyt::ns, program_order_is_relaxed(), simplify(), memory_model_sct::thread_spawn(), and to_code().
Referenced by memory_model_psot::operator()(), and operator()().
|
protectedvirtual |
Reimplemented from memory_model_sct.
Reimplemented in memory_model_psot.
Definition at line 38 of file memory_model_tso.cpp.
Referenced by program_order().