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
Memory models for partial order concurrency.
void read_from(symex_target_equationt &equation)
For each read r from every address we collect the choice symbols S via register_read_from_choice_symb...
void write_serialization_external(symex_target_equationt &equation)
void build_clock_type()
Initialize the clock_type so that it can be used to number events.
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 &)
First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (w...
#define PRECONDITION(CONDITION)
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
Produce an address ID for an event.