14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H 15 #define CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H 114 return (
id == other.
id);
119 return (
id < other.
id);
147 unsigned char met)
const;
192 static unsigned char uc(
bool truth_value)
194 return truth_value ? 1u : 0u;
205 #endif // CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
bool unsafe_pair_lwfence_param(const abstract_eventt &next, memory_modelt model, bool lwsync_met) const
bool operator<(const abstract_eventt &other) const
bool unsafe_pair_asm(const abstract_eventt &next, memory_modelt model, unsigned char met) const
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
unsigned char fence_value() const
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 is_corresponding_fence(const abstract_eventt &first, const abstract_eventt &second) const
bool unsafe_pair_lwfence(const abstract_eventt &next, memory_modelt model) const
abstract_eventt(operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local)
std::string get_operation() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool operator==(const abstract_eventt &other) const
A Template Class for Graphs.
static unsigned char uc(bool truth_value)
source_locationt source_location
This class represents a node in a directed graph.
std::ostream & operator<<(std::ostream &s, const abstract_eventt &e)