24 #ifndef CPROVER_MEMORY_MODEL_SUP_CLOCK 33 assert(e1->is_shared_read() || e1->is_shared_write());
34 assert(e2->is_shared_read() || e2->is_shared_write());
37 if(e1->atomic_section_id!=0 &&
38 e1->atomic_section_id==e2->atomic_section_id)
42 if(e1->is_shared_write() && e2->is_shared_write() &&
47 return e1->is_shared_write();
void read_from(symex_target_equationt &equation)
irep_idt address(event_it event) const
void from_read(symex_target_equationt &equation)
Memory models for partial order concurrency.
void build_clock_type(const symex_target_equationt &)
static mstreamt & eom(mstreamt &m)
void build_event_lists(symex_target_equationt &)
virtual bool program_order_is_relaxed(partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
void program_order(symex_target_equationt &equation)
void write_serialization_external(symex_target_equationt &equation)
eventst::const_iterator event_it
virtual void operator()(symex_target_equationt &equation)