cprover
|
#include <memory_model.h>
Public Member Functions | |
memory_model_baset (const namespacet &_ns) | |
virtual | ~memory_model_baset () |
virtual void | operator() (symex_target_equationt &)=0 |
![]() | |
partial_order_concurrencyt (const namespacet &_ns) | |
virtual | ~partial_order_concurrencyt () |
Protected Types | |
typedef std::map< std::pair< event_it, event_it >, symbol_exprt > | choice_symbolst |
typedef std::map< unsigned, event_listt > | per_thread_mapt |
![]() | |
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 | |
bool | po (event_it e1, event_it e2) |
symbol_exprt | nondet_bool_symbol (const std::string &prefix) |
void | read_from (symex_target_equationt &equation) |
![]() | |
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 (const symex_target_equationt &) |
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 |
Protected Attributes | |
unsigned | var_cnt |
choice_symbolst | choice_symbols |
![]() | |
const namespacet & | ns |
address_mapt | address_map |
numberingt | numbering |
typet | clock_type |
Additional Inherited Members | |
![]() | |
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 |
![]() | |
static irep_idt | rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION) |
![]() | |
static irep_idt | id (event_it event) |
Definition at line 17 of file memory_model.h.
|
protected |
Definition at line 36 of file memory_model.h.
|
protected |
Definition at line 42 of file memory_model.h.
|
explicit |
Definition at line 16 of file memory_model.cpp.
|
virtual |
Definition at line 22 of file memory_model.cpp.
|
protected |
Definition at line 26 of file memory_model.cpp.
References to_string(), and var_cnt.
Referenced by read_from(), and memory_model_sct::write_serialization_external().
|
pure virtual |
Implemented in memory_model_psot, memory_model_sct, and memory_model_tsot.
Definition at line 34 of file memory_model.cpp.
Referenced by memory_model_sct::from_read(), and read_from().
|
protected |
Definition at line 46 of file memory_model.cpp.
References partial_order_concurrencyt::add_constraint(), partial_order_concurrencyt::address_map, partial_order_concurrencyt::before(), choice_symbols, nondet_bool_symbol(), exprt::operands(), po(), r, partial_order_concurrencyt::a_rect::reads, 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 37 of file memory_model.h.
Referenced by memory_model_sct::from_read(), and read_from().
|
protected |
Definition at line 30 of file memory_model.h.
Referenced by nondet_bool_symbol().