Skip to content

Commit 5e83f8a

Browse files
Clean-up increase_generation
Add missing const, necessary narrow and insert if and else to make r_opt scoped to only the if branch.
1 parent d79f852 commit 5e83f8a

File tree

1 file changed

+6
-8
lines changed

1 file changed

+6
-8
lines changed

src/goto-symex/goto_state.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -31,19 +31,17 @@ std::size_t goto_statet::increase_generation(
3131
const ssa_exprt &lhs,
3232
std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
3333
{
34-
std::size_t n = fresh_l2_name_provider(l1_identifier);
34+
const std::size_t n = fresh_l2_name_provider(l1_identifier);
3535

36-
const auto r_opt = level2.current_names.find(l1_identifier);
37-
38-
if(!r_opt)
36+
if(const auto r_opt = level2.current_names.find(l1_identifier))
3937
{
40-
level2.current_names.insert(l1_identifier, std::make_pair(lhs, n));
38+
std::pair<ssa_exprt, unsigned> copy = r_opt->get();
39+
copy.second = narrow<unsigned>(n);
40+
level2.current_names.replace(l1_identifier, std::move(copy));
4141
}
4242
else
4343
{
44-
std::pair<ssa_exprt, unsigned> copy = r_opt->get();
45-
copy.second = n;
46-
level2.current_names.replace(l1_identifier, std::move(copy));
44+
level2.current_names.insert(l1_identifier, std::make_pair(lhs, n));
4745
}
4846

4947
return n;

0 commit comments

Comments
 (0)