cprover
|
#include <memory_model_pso.h>
Public Member Functions | |
memory_model_psot (const namespacet &_ns) | |
virtual void | operator() (symex_target_equationt &equation) |
![]() | |
memory_model_tsot (const namespacet &_ns) | |
![]() | |
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_pso.h.
|
inlineexplicit |
Definition at line 20 of file memory_model_pso.h.
References operator()(), and program_order_is_relaxed().
|
virtual |
Reimplemented from memory_model_tsot.
Definition at line 14 of file memory_model_pso.cpp.
References partial_order_concurrencyt::build_clock_type(), partial_order_concurrencyt::build_event_lists(), messaget::eom(), memory_model_sct::from_read(), memory_model_tsot::program_order(), memory_model_baset::read_from(), messaget::statistics(), and memory_model_sct::write_serialization_external().
Referenced by memory_model_psot().
|
protectedvirtual |
Reimplemented from memory_model_tsot.
Definition at line 29 of file memory_model_pso.cpp.
References partial_order_concurrencyt::address().
Referenced by memory_model_psot().