27 #ifndef CPROVER_MEMORY_MODEL_SUP_CLOCK 42 assert(e1->is_shared_read() || e1->is_shared_write());
43 assert(e2->is_shared_read() || e2->is_shared_write());
46 if(e1->atomic_section_id!=0 &&
47 e1->atomic_section_id==e2->atomic_section_id)
51 return e1->is_shared_write() && e2->is_shared_read();
64 for(per_thread_mapt::const_iterator
65 t_it=per_thread_map.begin();
66 t_it!=per_thread_map.end();
73 for(event_listt::const_iterator
78 if((*e_it)->is_memory_barrier())
81 event_listt::const_iterator next=e_it;
84 exprt mb_guard_r, mb_guard_w;
88 for(event_listt::const_iterator
93 if(((*e_it)->is_spawn() && !(*e_it2)->is_memory_barrier()) ||
102 if((*e_it2)->is_spawn())
108 if((*e_it2)->is_memory_barrier())
112 if((*e_it)->is_shared_read() &&
116 else if((*e_it)->is_shared_write() &&
123 mb_guard_r=
or_exprt(mb_guard_r, (*e_it2)->guard);
127 mb_guard_w=
or_exprt(mb_guard_w, (*e_it2)->guard);
142 if((*e_it2)->is_shared_read())
void read_from(symex_target_equationt &equation)
irep_idt address(event_it event) const
void from_read(symex_target_equationt &equation)
std::map< unsigned, event_listt > per_thread_mapt
exprt before(event_it e1, event_it e2, unsigned axioms)
void build_clock_type(const symex_target_equationt &)
static mstreamt & eom(mstreamt &m)
void build_event_lists(symex_target_equationt &)
bool get_bool(const irep_namet &name) const
The boolean constant true.
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)
virtual exprt before(event_it e1, event_it e2)
API to expression classes.
virtual void operator()(symex_target_equationt &equation)
void write_serialization_external(symex_target_equationt &equation)
void build_per_thread_map(const symex_target_equationt &equation, per_thread_mapt &dest) const
void thread_spawn(symex_target_equationt &equation, const per_thread_mapt &per_thread_map)
eventst::const_iterator event_it
Base class for all expressions.
const codet & to_code(const exprt &expr)
Memory models for partial order concurrency.
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
std::vector< event_it > event_listt
A statement in a programming language.
mstreamt & statistics() const
bool simplify(exprt &expr, const namespacet &ns)