Go to the documentation of this file.
24 #ifndef CPROVER_MEMORY_MODEL_SUP_CLOCK
33 PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
34 PRECONDITION(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();
eventst::const_iterator event_it
#define PRECONDITION(CONDITION)
void read_from(symex_target_equationt &equation)
void write_serialization_external(symex_target_equationt &equation)
virtual void operator()(symex_target_equationt &equation)
void from_read(symex_target_equationt &equation)
void program_order(symex_target_equationt &equation)
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
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
mstreamt & statistics() const
irep_idt address(event_it event) const