cprover
|
#include <partial_order_concurrency.h>
Classes | |
struct | a_rect |
Public Types | |
enum | axiomt { AX_SC_PER_LOCATION =1, AX_NO_THINAIR =2, AX_OBSERVATION =4, AX_PROPAGATION =8 } |
typedef symex_target_equationt::SSA_stept | eventt |
typedef symex_target_equationt::SSA_stepst | eventst |
typedef eventst::const_iterator | event_it |
Public Member Functions | |
partial_order_concurrencyt (const namespacet &_ns) | |
virtual | ~partial_order_concurrencyt () |
Static Public Member Functions | |
static irep_idt | rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION) |
Protected Types | |
typedef std::vector< event_it > | event_listt |
typedef std::map< irep_idt, a_rect > | address_mapt |
typedef std::map< event_it, unsigned > | numberingt |
Protected Member Functions | |
void | build_event_lists (symex_target_equationt &) |
void | add_init_writes (symex_target_equationt &) |
irep_idt | address (event_it event) const |
symbol_exprt | clock (event_it e, axiomt axiom) |
void | build_clock_type () |
void | add_constraint (symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const |
exprt | before (event_it e1, event_it e2, unsigned axioms) |
virtual exprt | before (event_it e1, event_it e2)=0 |
Static Protected Member Functions | |
static irep_idt | id (event_it event) |
Protected Attributes | |
const namespacet & | ns |
address_mapt | address_map |
numberingt | numbering |
typet | clock_type |
Definition at line 19 of file partial_order_concurrency.h.
|
protected |
Definition at line 53 of file partial_order_concurrency.h.
typedef eventst::const_iterator partial_order_concurrencyt::event_it |
Definition at line 27 of file partial_order_concurrency.h.
|
protected |
Definition at line 45 of file partial_order_concurrency.h.
Definition at line 26 of file partial_order_concurrency.h.
Definition at line 25 of file partial_order_concurrency.h.
|
protected |
Definition at line 60 of file partial_order_concurrency.h.
Enumerator | |
---|---|
AX_SC_PER_LOCATION | |
AX_NO_THINAIR | |
AX_OBSERVATION | |
AX_PROPAGATION |
Definition at line 30 of file partial_order_concurrency.h.
|
explicit |
Definition at line 19 of file partial_order_concurrency.cpp.
|
virtual |
Definition at line 24 of file partial_order_concurrency.cpp.
|
protected |
Definition at line 206 of file partial_order_concurrency.cpp.
References symex_target_equationt::constraint(), ns, and simplify().
Referenced by memory_model_sct::from_read(), memory_model_tsot::program_order(), memory_model_sct::program_order(), memory_model_baset::read_from(), memory_model_sct::thread_spawn(), and memory_model_sct::write_serialization_external().
|
protected |
Definition at line 28 of file partial_order_concurrency.cpp.
References address(), symex_target_equationt::SSA_stept::atomic_section_id, symex_target_equationt::SSA_stept::guard, ssa_exprt::remove_level_2(), goto_trace_stept::SHARED_WRITE, symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_steps, and symex_target_equationt::SSA_stept::type.
Referenced by build_event_lists().
Definition at line 70 of file partial_order_concurrency.h.
References symbol_exprt::get_identifier(), and ssa_exprt::remove_level_2().
Referenced by add_init_writes(), build_event_lists(), memory_model_tsot::program_order(), and memory_model_psot::program_order_is_relaxed().
Definition at line 172 of file partial_order_concurrency.cpp.
References AX_NO_THINAIR, AX_OBSERVATION, AX_PROPAGATION, AX_SC_PER_LOCATION, clock(), and conjunction().
Referenced by memory_model_sct::before(), memory_model_tsot::before(), memory_model_tsot::program_order(), and memory_model_baset::read_from().
Implemented in memory_model_sct, and memory_model_tsot.
|
protected |
Definition at line 164 of file partial_order_concurrency.cpp.
References address_bits(), clock_type, and template_numberingt< Map >::size().
Referenced by memory_model_psot::operator()(), memory_model_tsot::operator()(), and memory_model_sct::operator()().
|
protected |
Definition at line 77 of file partial_order_concurrency.cpp.
References add_init_writes(), address(), address_map, messaget::eom(), partial_order_concurrencyt::a_rect::reads, symex_target_equationt::SSA_steps, messaget::statistics(), and partial_order_concurrencyt::a_rect::writes.
Referenced by memory_model_psot::operator()(), memory_model_tsot::operator()(), and memory_model_sct::operator()().
|
protected |
Definition at line 141 of file partial_order_concurrency.cpp.
References clock_type, rw_clock_id(), to_string(), and UNREACHABLE.
Referenced by before().
Definition at line 64 of file partial_order_concurrency.h.
|
static |
Definition at line 127 of file partial_order_concurrency.cpp.
References id2string(), to_string(), and UNREACHABLE.
Referenced by build_goto_trace(), and clock().
|
protected |
Definition at line 54 of file partial_order_concurrency.h.
Referenced by build_event_lists(), memory_model_sct::from_read(), memory_model_baset::read_from(), and memory_model_sct::write_serialization_external().
|
protected |
Definition at line 78 of file partial_order_concurrency.h.
Referenced by build_clock_type(), and clock().
|
protected |
Definition at line 43 of file partial_order_concurrency.h.
Referenced by add_constraint(), and memory_model_tsot::program_order().
|
protected |
Definition at line 61 of file partial_order_concurrency.h.