Go to the documentation of this file.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
source_locationt source_location
std::string get_operation() const
static unsigned char uc(bool truth_value)
bool unsafe_pair_asm(const abstract_eventt &next, memory_modelt model, unsigned char met) const
std::ostream & operator<<(std::ostream &s, const abstract_eventt &e)
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
void operator()(const abstract_eventt &other)
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)
This class represents a node in a directed graph.
bool operator<(const abstract_eventt &other) const
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
bool unsafe_pair_lwfence_param(const abstract_eventt &next, memory_modelt model, bool lwsync_met) const
abstract_eventt(operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local)
unsigned char fence_value() const
bool operator==(const abstract_eventt &other) const