cprover
abstract_eventt Class Reference

#include <abstract_event.h>

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

Public Types

enum  operationt {
  operationt::Write, operationt::Read, operationt::Fence, operationt::Lwfence,
  operationt::ASMfence
}
 
- Public Types inherited from graph_nodet< empty_edget >
typedef std::size_t node_indext
 
typedef empty_edget edget
 
typedef std::map< node_indext, edgetedgest
 

Public Member Functions

 abstract_eventt ()
 
 abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local)
 
 abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local, bool WRf, bool WWf, bool RRf, bool RWf, bool WWc, bool RWc, bool RRc)
 
void operator() (const abstract_eventt &other)
 
bool operator== (const abstract_eventt &other) const
 
bool operator< (const abstract_eventt &other) const
 
bool is_fence () const
 
bool unsafe_pair (const abstract_eventt &next, memory_modelt model) const
 
bool unsafe_pair_lwfence (const abstract_eventt &next, memory_modelt model) const
 
bool unsafe_pair_asm (const abstract_eventt &next, memory_modelt model, unsigned char met) const
 
std::string get_operation () const
 
bool is_corresponding_fence (const abstract_eventt &first, const abstract_eventt &second) const
 
bool is_direct () const
 
bool is_cumul () const
 
unsigned char fence_value () const
 
- Public Member Functions inherited from graph_nodet< empty_edget >
void add_in (node_indext n)
 
void add_out (node_indext n)
 
void erase_in (node_indext n)
 
void erase_out (node_indext n)
 

Public Attributes

operationt operation
 
unsigned thread
 
irep_idt variable
 
unsigned id
 
source_locationt source_location
 
bool local
 
bool WRfence
 
bool WWfence
 
bool RRfence
 
bool RWfence
 
bool WWcumul
 
bool RWcumul
 
bool RRcumul
 
- Public Attributes inherited from graph_nodet< empty_edget >
edgest in
 
edgest out
 

Protected Member Functions

bool unsafe_pair_lwfence_param (const abstract_eventt &next, memory_modelt model, bool lwsync_met) const
 

Detailed Description

Definition at line 22 of file abstract_event.h.

Member Enumeration Documentation

◆ operationt

Enumerator
Write 
Read 
Fence 
Lwfence 
ASMfence 

Definition at line 30 of file abstract_event.h.

Constructor & Destructor Documentation

◆ abstract_eventt() [1/3]

abstract_eventt::abstract_eventt ( )
inline

Definition at line 48 of file abstract_event.h.

◆ abstract_eventt() [2/3]

abstract_eventt::abstract_eventt ( operationt  _op,
unsigned  _th,
irep_idt  _var,
unsigned  _id,
source_locationt  _loc,
bool  _local 
)
inline

Definition at line 52 of file abstract_event.h.

◆ abstract_eventt() [3/3]

abstract_eventt::abstract_eventt ( operationt  _op,
unsigned  _th,
irep_idt  _var,
unsigned  _id,
source_locationt  _loc,
bool  _local,
bool  WRf,
bool  WWf,
bool  RRf,
bool  RWf,
bool  WWc,
bool  RWc,
bool  RRc 
)
inline

Definition at line 60 of file abstract_event.h.

Member Function Documentation

◆ fence_value()

unsigned char abstract_eventt::fence_value ( ) const
inline

Definition at line 173 of file abstract_event.h.

References RRcumul, RRfence, RWcumul, RWfence, WRfence, WWcumul, and WWfence.

Referenced by event_grapht::critical_cyclet::print_name().

◆ get_operation()

◆ is_corresponding_fence()

bool abstract_eventt::is_corresponding_fence ( const abstract_eventt first,
const abstract_eventt second 
) const
inline

Definition at line 152 of file abstract_event.h.

References operation, Read, RRcumul, RRfence, RWcumul, RWfence, WRfence, Write, WWcumul, and WWfence.

◆ is_cumul()

bool abstract_eventt::is_cumul ( ) const
inline

Definition at line 171 of file abstract_event.h.

References RRcumul, RWcumul, and WWcumul.

◆ is_direct()

bool abstract_eventt::is_direct ( ) const
inline

Definition at line 170 of file abstract_event.h.

References RRfence, RWfence, WRfence, and WWfence.

◆ is_fence()

bool abstract_eventt::is_fence ( ) const
inline

Definition at line 111 of file abstract_event.h.

References ASMfence, Fence, Lwfence, and operation.

Referenced by event_grapht::critical_cyclet::hide_internals().

◆ operator()()

void abstract_eventt::operator() ( const abstract_eventt other)
inline

Definition at line 91 of file abstract_event.h.

References id, local, operation, source_location, thread, and variable.

◆ operator<()

bool abstract_eventt::operator< ( const abstract_eventt other) const
inline

Definition at line 106 of file abstract_event.h.

References id.

◆ operator==()

bool abstract_eventt::operator== ( const abstract_eventt other) const
inline

Definition at line 101 of file abstract_event.h.

References id.

◆ unsafe_pair()

bool abstract_eventt::unsafe_pair ( const abstract_eventt next,
memory_modelt  model 
) const
inline

◆ unsafe_pair_asm()

bool abstract_eventt::unsafe_pair_asm ( const abstract_eventt next,
memory_modelt  model,
unsigned char  met 
) const

◆ unsafe_pair_lwfence()

bool abstract_eventt::unsafe_pair_lwfence ( const abstract_eventt next,
memory_modelt  model 
) const
inline

Definition at line 126 of file abstract_event.h.

References unsafe_pair_lwfence_param().

Referenced by event_grapht::critical_cyclet::is_unsafe().

◆ unsafe_pair_lwfence_param()

bool abstract_eventt::unsafe_pair_lwfence_param ( const abstract_eventt next,
memory_modelt  model,
bool  lwsync_met 
) const
protected

Definition at line 16 of file abstract_event.cpp.

References ASMfence, Fence, local, Lwfence, operation, Power, PSO, Read, RMO, thread, TSO, Unknown, variable, and Write.

Referenced by unsafe_pair(), and unsafe_pair_lwfence().

Member Data Documentation

◆ id

unsigned abstract_eventt::id

◆ local

◆ operation

◆ RRcumul

bool abstract_eventt::RRcumul

Definition at line 46 of file abstract_event.h.

Referenced by fence_value(), is_corresponding_fence(), and is_cumul().

◆ RRfence

bool abstract_eventt::RRfence

Definition at line 42 of file abstract_event.h.

Referenced by fence_value(), is_corresponding_fence(), and is_direct().

◆ RWcumul

bool abstract_eventt::RWcumul

Definition at line 45 of file abstract_event.h.

Referenced by fence_value(), is_corresponding_fence(), and is_cumul().

◆ RWfence

bool abstract_eventt::RWfence

Definition at line 43 of file abstract_event.h.

Referenced by fence_value(), is_corresponding_fence(), and is_direct().

◆ source_location

◆ thread

◆ variable

◆ WRfence

bool abstract_eventt::WRfence

◆ WWcumul

bool abstract_eventt::WWcumul

Definition at line 44 of file abstract_event.h.

Referenced by fence_value(), is_corresponding_fence(), and is_cumul().

◆ WWfence

bool abstract_eventt::WWfence

Definition at line 41 of file abstract_event.h.

Referenced by fence_value(), is_corresponding_fence(), and is_direct().


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