We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 57bae7b commit 0affd00Copy full SHA for 0affd00
src/goto-symex/goto_symex_state.cpp
@@ -473,19 +473,17 @@ bool goto_symex_statet::l2_thread_read_encoding(
473
const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
474
if(a_s_writes!=written_in_atomic_section.end())
475
{
476
- for(a_s_w_entryt::const_iterator it=a_s_writes->second.begin();
477
- it!=a_s_writes->second.end();
478
- ++it)
+ for(const auto &guard_in_list : a_s_writes->second)
479
480
- guardt g=*it;
+ guardt g = guard_in_list;
481
g-=guard;
482
if(g.is_true())
483
// there has already been a write to l1_identifier within
484
// this atomic section under the same guard, or a guard
485
// that implies the current one
486
return false;
487
488
- write_guard|=*it;
+ write_guard |= guard_in_list;
489
}
490
491
0 commit comments