cprover
memory_model_tsot Class Reference

#include <memory_model_tso.h>

Inheritance diagram for memory_model_tsot:
[legend]
Collaboration diagram for memory_model_tsot:
[legend]

Public Member Functions

 memory_model_tsot (const namespacet &_ns)
 
virtual void operator() (symex_target_equationt &equation)
 
- Public Member Functions inherited from memory_model_sct
 memory_model_sct (const namespacet &_ns)
 
- Public Member Functions inherited from memory_model_baset
 memory_model_baset (const namespacet &_ns)
 
virtual ~memory_model_baset ()
 
- Public Member Functions inherited from partial_order_concurrencyt
 partial_order_concurrencyt (const namespacet &_ns)
 
virtual ~partial_order_concurrencyt ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Member Functions

virtual exprt before (event_it e1, event_it e2)
 
virtual bool program_order_is_relaxed (partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
 
void program_order (symex_target_equationt &equation)
 
- Protected Member Functions inherited from memory_model_sct
void build_per_thread_map (const symex_target_equationt &equation, per_thread_mapt &dest) const
 
void thread_spawn (symex_target_equationt &equation, const per_thread_mapt &per_thread_map)
 
void program_order (symex_target_equationt &equation)
 
void from_read (symex_target_equationt &equation)
 
void write_serialization_external (symex_target_equationt &equation)
 
- Protected Member Functions inherited from memory_model_baset
bool po (event_it e1, event_it e2)
 
symbol_exprt nondet_bool_symbol (const std::string &prefix)
 
void read_from (symex_target_equationt &equation)
 
- Protected Member Functions inherited from partial_order_concurrencyt
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)
 

Additional Inherited Members

- Public Types inherited from partial_order_concurrencyt
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 Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from partial_order_concurrencyt
static irep_idt rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION)
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Protected Types inherited from memory_model_baset
typedef std::map< std::pair< event_it, event_it >, symbol_exprtchoice_symbolst
 
typedef std::map< unsigned, event_listtper_thread_mapt
 
- Protected Types inherited from partial_order_concurrencyt
typedef std::vector< event_itevent_listt
 
typedef std::map< irep_idt, a_rectaddress_mapt
 
typedef std::map< event_it, unsigned > numberingt
 
- Static Protected Member Functions inherited from partial_order_concurrencyt
static irep_idt id (event_it event)
 
- Protected Attributes inherited from memory_model_baset
unsigned var_cnt
 
choice_symbolst choice_symbols
 
- Protected Attributes inherited from partial_order_concurrencyt
const namespacetns
 
address_mapt address_map
 
numberingt numbering
 
typet clock_type
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 17 of file memory_model_tso.h.

Constructor & Destructor Documentation

◆ memory_model_tsot()

memory_model_tsot::memory_model_tsot ( const namespacet _ns)
inlineexplicit

Definition at line 20 of file memory_model_tso.h.

Member Function Documentation

◆ before()

exprt memory_model_tsot::before ( event_it  e1,
event_it  e2 
)
protectedvirtual

◆ operator()()

◆ program_order()

◆ program_order_is_relaxed()

bool memory_model_tsot::program_order_is_relaxed ( partial_order_concurrencyt::event_it  e1,
partial_order_concurrencyt::event_it  e2 
) const
protectedvirtual

Reimplemented from memory_model_sct.

Reimplemented in memory_model_psot.

Definition at line 38 of file memory_model_tso.cpp.

Referenced by program_order().


The documentation for this class was generated from the following files: