Skip to content

Commit 1401d12

Browse files
Use emplace to avoid double lookup
1 parent f701467 commit 1401d12

File tree

2 files changed

+4
-9
lines changed

2 files changed

+4
-9
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -185,8 +185,7 @@ void goto_symex_statet::assignment(
185185
#endif
186186

187187
// do the l2 renaming
188-
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
189-
level2.current_names[l1_identifier]=std::make_pair(lhs, 0);
188+
level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
190189
level2.increase_counter(l1_identifier);
191190
set_l2_indices(lhs, ns);
192191

@@ -440,8 +439,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
440439

441440
if(a_s_read.second.empty())
442441
{
443-
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
444-
level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
442+
level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0));
445443
level2.increase_counter(l1_identifier);
446444
a_s_read.first=level2.current_count(l1_identifier);
447445
}
@@ -478,8 +476,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
478476
return true;
479477
}
480478

481-
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
482-
level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
479+
level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0));
483480

484481
// No event and no fresh index, but avoid constant propagation
485482
if(!record_events)

src/goto-symex/symex_decl.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,9 +68,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
6868
// L2 renaming
6969
// inlining may yield multiple declarations of the same identifier
7070
// within the same L1 context
71-
if(state.level2.current_names.find(l1_identifier)==
72-
state.level2.current_names.end())
73-
state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
71+
state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0));
7472
state.level2.increase_counter(l1_identifier);
7573
const bool record_events=state.record_events;
7674
state.record_events=false;

0 commit comments

Comments
 (0)