Skip to content

Commit 43eb277

Browse files
Define a symex_level2t::operator()
This is to be uniform with the other levels.
1 parent 9dda74a commit 43eb277

File tree

3 files changed

+8
-1
lines changed

3 files changed

+8
-1
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ void goto_symex_statet::set_l2_indices(
260260
return;
261261
level0(ssa_expr, ns, source.thread_nr);
262262
level1(ssa_expr);
263-
ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
263+
level2(ssa_expr);
264264
}
265265

266266
template <goto_symex_statet::levelt level>

src/goto-symex/renaming_level.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,11 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr) const
5858
ssa_expr.set_level_1(it->second.second);
5959
}
6060

61+
void symex_level2t::operator()(ssa_exprt &ssa_expr) const
62+
{
63+
ssa_expr.set_level_2(current_count(ssa_expr.get_identifier()));
64+
}
65+
6166
void symex_level1t::restore_from(
6267
const symex_renaming_levelt::current_namest &other)
6368
{

src/goto-symex/renaming_level.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,8 @@ struct symex_level1t : public symex_renaming_levelt
8282
/// This is to ensure each variable is only assigned once.
8383
struct symex_level2t : public symex_renaming_levelt
8484
{
85+
void operator()(ssa_exprt &ssa_expr) const;
86+
8587
symex_level2t() = default;
8688
~symex_level2t() override = default;
8789
};

0 commit comments

Comments
 (0)