Skip to content

Commit ba561d0

Browse files
Avoid lookup by assigning using iterator
1 parent 1401d12 commit ba561d0

File tree

1 file changed

+9
-3
lines changed

1 file changed

+9
-3
lines changed

src/goto-symex/symex_function_call.cpp

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -410,15 +410,21 @@ void goto_symext::locality(
410410
// save old L1 name for popping the frame
411411
const auto c_it = state.level1.current_names.find(l0_name);
412412

413-
if(c_it!=state.level1.current_names.end())
413+
if(c_it != state.level1.current_names.end())
414+
{
414415
frame.old_level1[l0_name]=c_it->second;
416+
c_it->second = std::make_pair(ssa, frame_nr);
417+
}
418+
else
419+
{
420+
state.level1.current_names.emplace(
421+
l0_name, std::make_pair(ssa, frame_nr));
422+
}
415423

416424
// do L1 renaming -- these need not be unique, as
417425
// identifiers may be shared among functions
418426
// (e.g., due to inlining or other code restructuring)
419427

420-
state.level1.current_names[l0_name]=
421-
std::make_pair(ssa, frame_nr);
422428
state.rename(ssa, ns, goto_symex_statet::L1);
423429

424430
irep_idt l1_name=ssa.get_identifier();

0 commit comments

Comments
 (0)