cprover
partial_order_concurrencyt Class Referenceabstract

#include <partial_order_concurrency.h>

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

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 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
}
 

Public Member Functions

 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 ()
 

Static Public Member Functions

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

typedef std::vector< event_itevent_listt
 
typedef std::map< irep_idt, a_rectaddress_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 (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
 

Static Protected Member Functions

static irep_idt id (event_it event)
 

Protected Attributes

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 19 of file partial_order_concurrency.h.

Member Typedef Documentation

§ address_mapt

Definition at line 53 of file partial_order_concurrency.h.

§ event_it

typedef eventst::const_iterator partial_order_concurrencyt::event_it

Definition at line 27 of file partial_order_concurrency.h.

§ event_listt

typedef std::vector<event_it> partial_order_concurrencyt::event_listt
protected

Definition at line 45 of file partial_order_concurrency.h.

§ eventst

§ eventt

§ numberingt

typedef std::map<event_it, unsigned> partial_order_concurrencyt::numberingt
protected

Definition at line 60 of file partial_order_concurrency.h.

Member Enumeration Documentation

§ axiomt

Enumerator
AX_SC_PER_LOCATION 
AX_NO_THINAIR 
AX_OBSERVATION 
AX_PROPAGATION 

Definition at line 30 of file partial_order_concurrency.h.

Constructor & Destructor Documentation

§ partial_order_concurrencyt()

partial_order_concurrencyt::partial_order_concurrencyt ( const namespacet _ns)
explicit

Definition at line 19 of file partial_order_concurrency.cpp.

§ ~partial_order_concurrencyt()

partial_order_concurrencyt::~partial_order_concurrencyt ( )
virtual

Definition at line 24 of file partial_order_concurrency.cpp.

Member Function Documentation

§ add_constraint()

void partial_order_concurrencyt::add_constraint ( symex_target_equationt equation,
const exprt cond,
const std::string &  msg,
const symex_targett::sourcet source 
) const
protected

§ add_init_writes()

§ address()

irep_idt partial_order_concurrencyt::address ( event_it  event) const
inlineprotected

§ before() [1/2]

exprt partial_order_concurrencyt::before ( event_it  e1,
event_it  e2,
unsigned  axioms 
)
protected

§ before() [2/2]

virtual exprt partial_order_concurrencyt::before ( event_it  e1,
event_it  e2 
)
protectedpure virtual

Implemented in memory_model_sct, and memory_model_tsot.

§ build_clock_type()

void partial_order_concurrencyt::build_clock_type ( const symex_target_equationt equation)
protected

§ build_event_lists()

§ clock()

symbol_exprt partial_order_concurrencyt::clock ( event_it  e,
axiomt  axiom 
)
protected

Definition at line 141 of file partial_order_concurrency.cpp.

References clock_type, and rw_clock_id().

Referenced by before().

§ id()

static irep_idt partial_order_concurrencyt::id ( event_it  event)
inlinestaticprotected

Definition at line 64 of file partial_order_concurrency.h.

§ rw_clock_id()

irep_idt partial_order_concurrencyt::rw_clock_id ( event_it  e,
axiomt  axiom = AX_PROPAGATION 
)
static

Definition at line 127 of file partial_order_concurrency.cpp.

References id2string().

Referenced by build_goto_trace(), and clock().

Member Data Documentation

§ address_map

§ clock_type

typet partial_order_concurrencyt::clock_type
protected

Definition at line 78 of file partial_order_concurrency.h.

Referenced by build_clock_type(), and clock().

§ ns

const namespacet& partial_order_concurrencyt::ns
protected

Definition at line 43 of file partial_order_concurrency.h.

Referenced by add_constraint(), and memory_model_tsot::program_order().

§ numbering

numberingt partial_order_concurrencyt::numbering
protected

Definition at line 61 of file partial_order_concurrency.h.


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