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 |
Additional Inherited Members |
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.
|
protected |
Definition at line 28 of file partial_order_concurrency.cpp.
Definition at line 70 of file partial_order_concurrency.h.
Definition at line 172 of file partial_order_concurrency.cpp.
Implemented in memory_model_sct, and memory_model_tsot.
|
protected |
Definition at line 164 of file partial_order_concurrency.cpp.
|
protected |
Definition at line 77 of file partial_order_concurrency.cpp.
|
protected |
Definition at line 141 of file partial_order_concurrency.cpp.
Definition at line 64 of file partial_order_concurrency.h.
|
static |
Definition at line 127 of file partial_order_concurrency.cpp.
|
protected |
Definition at line 54 of file partial_order_concurrency.h.
|
protected |
Definition at line 78 of file partial_order_concurrency.h.
|
protected |
Definition at line 43 of file partial_order_concurrency.h.
|
protected |
Definition at line 61 of file partial_order_concurrency.h.