14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H 15 #define CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H 55 :operation(_op), thread(_th), variable(_var), id(_id),
56 source_location(_loc), local(_local)
78 source_location(_loc),
103 return (
id == other.
id);
108 return (
id < other.
id);
136 unsigned char met)
const;
175 unsigned char value = WRfence + 2*WWfence + 4*RRfence + 8*RWfence
176 + 16*WWcumul + 32*RWcumul + 64*
RRcumul;
188 #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
bool operator==(const abstract_eventt &other) const
A Template Class for Graphs.
source_locationt source_location
This class represents a node in a directed graph.
std::ostream & operator<<(std::ostream &s, const abstract_eventt &e)