cprover
|
#include <memory_model_sc.h>
Public Member Functions | |
memory_model_sct (const namespacet &_ns) | |
virtual void | operator() (symex_target_equationt &equation) |
![]() | |
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_sc.h.
|
inlineexplicit |
Definition at line 20 of file memory_model_sc.h.
Implements partial_order_concurrencyt.
Reimplemented in memory_model_tsot.
Definition at line 29 of file memory_model_sc.cpp.
References partial_order_concurrencyt::AX_PROPAGATION, and partial_order_concurrencyt::before().
Referenced by from_read(), program_order(), thread_spawn(), and write_serialization_external().
|
protected |
Definition at line 45 of file memory_model_sc.cpp.
References symex_target_equationt::SSA_steps.
Referenced by memory_model_tsot::program_order(), and program_order().
|
protected |
Definition at line 248 of file memory_model_sc.cpp.
References partial_order_concurrencyt::add_constraint(), partial_order_concurrencyt::address_map, before(), memory_model_baset::choice_symbols, exprt::is_false(), irept::is_not_nil(), irept::make_nil(), memory_model_baset::po(), program_order_is_relaxed(), r, and partial_order_concurrencyt::a_rect::writes.
Referenced by memory_model_psot::operator()(), memory_model_tsot::operator()(), and operator()().
|
virtual |
Implements memory_model_baset.
Reimplemented in memory_model_psot, and memory_model_tsot.
Definition at line 16 of file memory_model_sc.cpp.
References partial_order_concurrencyt::build_clock_type(), partial_order_concurrencyt::build_event_lists(), messaget::eom(), from_read(), program_order(), memory_model_baset::read_from(), messaget::statistics(), and write_serialization_external().
|
protected |
Definition at line 149 of file memory_model_sc.cpp.
References partial_order_concurrencyt::add_constraint(), before(), build_per_thread_map(), symex_target_equationt::SSA_steps, and thread_spawn().
Referenced by operator()().
|
protectedvirtual |
Reimplemented in memory_model_tsot, and memory_model_psot.
Definition at line 35 of file memory_model_sc.cpp.
Referenced by from_read().
|
protected |
Definition at line 66 of file memory_model_sc.cpp.
References partial_order_concurrencyt::add_constraint(), before(), next_thread_id, and symex_target_equationt::SSA_steps.
Referenced by memory_model_tsot::program_order(), and program_order().
|
protected |
Definition at line 196 of file memory_model_sc.cpp.
References partial_order_concurrencyt::add_constraint(), partial_order_concurrencyt::address_map, before(), memory_model_baset::nondet_bool_symbol(), and partial_order_concurrencyt::a_rect::writes.
Referenced by memory_model_psot::operator()(), memory_model_tsot::operator()(), and operator()().