cprover
Loading...
Searching...
No Matches
abstract_eventt Class Reference

#include <abstract_event.h>

Inheritance diagram for abstract_eventt:
Collaboration diagram for abstract_eventt:

Public Types

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

Public Member Functions

 abstract_eventt ()
 abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, irep_idt _function_id, bool _local)
 abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, irep_idt _function_id, 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)
std::string pretty (const node_indext &idx) const
virtual ~graph_nodet ()

Public Attributes

operationt operation
unsigned thread
irep_idt variable
unsigned id
source_locationt source_location
irep_idt function_id
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

Static Private Member Functions

static unsigned char uc (bool truth_value)

Detailed Description

Definition at line 22 of file abstract_event.h.

Member Enumeration Documentation

◆ operationt

enum class abstract_eventt::operationt
strong
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 49 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,
irep_idt _function_id,
bool _local )
inline

Definition at line 64 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,
irep_idt _function_id,
bool _local,
bool WRf,
bool WWf,
bool RRf,
bool RWf,
bool WWc,
bool RWc,
bool RRc )
inline

Definition at line 82 of file abstract_event.h.

Member Function Documentation

◆ fence_value()

unsigned char abstract_eventt::fence_value ( ) const
inline

Definition at line 198 of file abstract_event.h.

◆ get_operation()

std::string abstract_eventt::get_operation ( ) const
inline

Definition at line 163 of file abstract_event.h.

◆ is_corresponding_fence()

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

Definition at line 177 of file abstract_event.h.

◆ is_cumul()

bool abstract_eventt::is_cumul ( ) const
inline

Definition at line 196 of file abstract_event.h.

◆ is_direct()

bool abstract_eventt::is_direct ( ) const
inline

Definition at line 195 of file abstract_event.h.

◆ is_fence()

bool abstract_eventt::is_fence ( ) const
inline

Definition at line 136 of file abstract_event.h.

◆ operator()()

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

Definition at line 115 of file abstract_event.h.

◆ operator<()

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

Definition at line 131 of file abstract_event.h.

◆ operator==()

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

Definition at line 126 of file abstract_event.h.

◆ uc()

unsigned char abstract_eventt::uc ( bool truth_value)
inlinestaticprivate

Definition at line 206 of file abstract_event.h.

◆ unsafe_pair()

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

Definition at line 146 of file abstract_event.h.

◆ unsafe_pair_asm()

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

Definition at line 101 of file abstract_event.cpp.

◆ unsafe_pair_lwfence()

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

Definition at line 151 of file abstract_event.h.

◆ 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.

Member Data Documentation

◆ function_id

irep_idt abstract_eventt::function_id

Definition at line 37 of file abstract_event.h.

◆ id

unsigned abstract_eventt::id

Definition at line 35 of file abstract_event.h.

◆ local

bool abstract_eventt::local

Definition at line 38 of file abstract_event.h.

◆ operation

operationt abstract_eventt::operation

Definition at line 32 of file abstract_event.h.

◆ RRcumul

bool abstract_eventt::RRcumul

Definition at line 47 of file abstract_event.h.

◆ RRfence

bool abstract_eventt::RRfence

Definition at line 43 of file abstract_event.h.

◆ RWcumul

bool abstract_eventt::RWcumul

Definition at line 46 of file abstract_event.h.

◆ RWfence

bool abstract_eventt::RWfence

Definition at line 44 of file abstract_event.h.

◆ source_location

source_locationt abstract_eventt::source_location

Definition at line 36 of file abstract_event.h.

◆ thread

unsigned abstract_eventt::thread

Definition at line 33 of file abstract_event.h.

◆ variable

irep_idt abstract_eventt::variable

Definition at line 34 of file abstract_event.h.

◆ WRfence

bool abstract_eventt::WRfence

Definition at line 41 of file abstract_event.h.

◆ WWcumul

bool abstract_eventt::WWcumul

Definition at line 45 of file abstract_event.h.

◆ WWfence

bool abstract_eventt::WWfence

Definition at line 42 of file abstract_event.h.

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