Skip to content

Commit bc95e96

Browse files
Use ranged-for instead of iterators
1 parent 333fd46 commit bc95e96

File tree

2 files changed

+10
-11
lines changed

2 files changed

+10
-11
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -380,20 +380,18 @@ void goto_symext::phi_function(
380380
.concat(dest_state_names_range);
381381

382382
guardt diff_guard;
383-
if(!all_current_names_range.is_empty())
383+
if(!all_current_names_range.empty())
384384
{
385385
diff_guard=goto_state.guard;
386386

387387
// this gets the diff between the guards
388388
diff_guard-=dest_state.guard;
389389
}
390390

391-
for(auto it = all_current_names_range.begin();
392-
it != all_current_names_range.end();
393-
++it)
391+
for(const auto &ssa : all_current_names_range)
394392
{
395-
const irep_idt l1_identifier=it->get_identifier();
396-
const irep_idt &obj_identifier=it->get_object_name();
393+
const irep_idt l1_identifier = ssa.get_identifier();
394+
const irep_idt &obj_identifier = ssa.get_object_name();
397395

398396
if(obj_identifier==guard_identifier)
399397
continue; // just a guard, don't bother
@@ -418,11 +416,12 @@ void goto_symext::phi_function(
418416
// may have been introduced by symex_start_thread (and will
419417
// only later be removed from level2.current_names by pop_frame
420418
// once the thread is executed)
421-
if(!it->get_level_0().empty() &&
422-
it->get_level_0()!=std::to_string(dest_state.source.thread_nr))
419+
if(
420+
!ssa.get_level_0().empty() &&
421+
ssa.get_level_0() != std::to_string(dest_state.source.thread_nr))
423422
continue;
424423

425-
exprt goto_state_rhs=*it, dest_state_rhs=*it;
424+
exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
426425

427426
{
428427
goto_symex_statet::propagationt::valuest::const_iterator p_it=
@@ -470,7 +469,7 @@ void goto_symext::phi_function(
470469
do_simplify(rhs);
471470
}
472471

473-
ssa_exprt new_lhs=*it;
472+
ssa_exprt new_lhs = ssa;
474473
const bool record_events=dest_state.record_events;
475474
dest_state.record_events=false;
476475
dest_state.assignment(new_lhs, rhs, ns, true, true);

src/util/range.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,7 @@ struct ranget final
311311
concat_begin, concat_end);
312312
}
313313

314-
bool is_empty() const
314+
bool empty() const
315315
{
316316
return begin_value == end_value;
317317
}

0 commit comments

Comments
 (0)