39 PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
40 PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
51 for(eventst::const_iterator
57 if(!e_it->is_shared_read() &&
58 !e_it->is_shared_write() &&
60 !e_it->is_memory_barrier())
continue;
62 dest[e_it->source.thread_nr].push_back(e_it);
74 for(eventst::const_iterator
81 per_thread_mapt::const_iterator next_thread=
83 if(next_thread==per_thread_map.end())
88 for(event_listt::const_iterator
89 n_it=next_thread->second.begin();
90 n_it!=next_thread->second.end();
93 if(!(*n_it)->is_memory_barrier())
107 const per_thread_mapt &per_thread_map)
113 for(eventst::const_iterator
120 per_thread_mapt::const_iterator next_thread=
122 if(next_thread==per_thread_map.end())
130 event_listt::const_iterator n_it=next_thread->second.begin();
132 n_it!=next_thread->second.end() &&
133 (*n_it)->is_memory_barrier();
138 if(n_it!=next_thread->second.end())
159 for(per_thread_mapt::const_iterator
160 t_it=per_thread_map.begin();
161 t_it!=per_thread_map.end();
170 for(event_listt::const_iterator
175 if((*e_it)->is_memory_barrier())
199 for(address_mapt::const_iterator
204 const a_rect &a_rec=a_it->second;
209 for(event_listt::const_iterator
210 w_it1=a_rec.
writes.begin();
211 w_it1!=a_rec.
writes.end();
214 event_listt::const_iterator next=w_it1;
217 for(event_listt::const_iterator w_it2=next;
218 w_it2!=a_rec.
writes.end();
222 if((*w_it1)->source.thread_nr==
223 (*w_it2)->source.thread_nr)
252 for(address_mapt::const_iterator
257 const a_rect &a_rec=a_it->second;
260 for(event_listt::const_iterator
261 w_prime=a_rec.
writes.begin();
262 w_prime!=a_rec.
writes.end();
265 event_listt::const_iterator next=w_prime;
268 for(event_listt::const_iterator w=next;
274 if(
po(*w_prime, *w) &&
280 else if(
po(*w, *w_prime) &&
293 for(choice_symbolst::const_iterator
299 exprt rf=c_it->second;
303 if(c_it->first.second==*w_prime && !ws1.
is_false())
315 else if(c_it->first.second==*w && !ws2.
is_false())
324 and_exprt(
r->guard, (*w_prime)->guard, ws2, rf),
330 cond,
"fr",
r->source);