Skip to content

Commit b5ae64b

Browse files
Make symex_level2t::operator() return a renamedt
This makes it in the type the result has been renamed and a level 1 expression is expected as argument.
1 parent 4bb3472 commit b5ae64b

File tree

3 files changed

+12
-7
lines changed

3 files changed

+12
-7
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -261,9 +261,9 @@ void goto_symex_statet::set_l2_indices(
261261
{
262262
if(!ssa_expr.get_level_2().empty())
263263
return;
264-
renamedt<ssa_exprt, L1> l1 =
265-
level1(level0(std::move(ssa_expr), ns, source.thread_nr);
266-
ssa_expr = level2(l1.get());
264+
renamedt<ssa_exprt, L2> l2 =
265+
level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
266+
ssa_expr = l2.get();
267267
}
268268

269269
template <levelt level>
@@ -287,6 +287,8 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
287287
/// Ensure `rename_ssa` gets compiled for L0
288288
template ssa_exprt
289289
goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
290+
template ssa_exprt
291+
goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
290292

291293
template <levelt level>
292294
exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
@@ -369,6 +371,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
369371
return expr;
370372
}
371373

374+
template exprt goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
375+
372376
/// thread encoding
373377
bool goto_symex_statet::l2_thread_read_encoding(
374378
ssa_exprt &expr,

src/goto-symex/renaming_level.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -60,10 +60,11 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
6060
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
6161
}
6262

63-
ssa_exprt symex_level2t::operator()(ssa_exprt ssa_expr) const
63+
renamedt<ssa_exprt, L2> symex_level2t::
64+
operator()(renamedt<ssa_exprt, L1> l1_expr) const
6465
{
65-
ssa_expr.set_level_2(current_count(ssa_expr.get_identifier()));
66-
return ssa_expr;
66+
l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier()));
67+
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
6768
}
6869

6970
void symex_level1t::restore_from(

src/goto-symex/renaming_level.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ struct symex_level1t : public symex_renaming_levelt
121121
/// This is to ensure each variable is only assigned once.
122122
struct symex_level2t : public symex_renaming_levelt
123123
{
124-
ssa_exprt operator()(ssa_exprt ssa_expr) const;
124+
renamedt<ssa_exprt, L2> operator()(renamedt<ssa_exprt, L1> l1_expr) const;
125125

126126
symex_level2t() = default;
127127
~symex_level2t() override = default;

0 commit comments

Comments
 (0)