Skip to content

Commit b49354d

Browse files
Make set_l0_indices return a renamedt
This makes explicit that the result is a renamed expression and can be propagated in through other functions.
1 parent a151280 commit b49354d

File tree

2 files changed

+5
-8
lines changed

2 files changed

+5
-8
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -235,13 +235,10 @@ void goto_symex_statet::assignment(
235235
#endif
236236
}
237237

238-
void goto_symex_statet::set_l0_indices(
239-
ssa_exprt &ssa_expr,
240-
const namespacet &ns)
238+
renamedt<ssa_exprt, L0>
239+
goto_symex_statet::set_l0_indices(ssa_exprt ssa_expr, const namespacet &ns)
241240
{
242-
renamedt<ssa_exprt, L0> renamed =
243-
level0(std::move(ssa_expr), ns, source.thread_nr);
244-
ssa_expr = renamed.get();
241+
return level0(std::move(ssa_expr), ns, source.thread_nr);
245242
}
246243

247244
void goto_symex_statet::set_l1_indices(
@@ -275,7 +272,7 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
275272
level == L0 || level == L1,
276273
"rename_ssa can only be used for levels L0 and L1");
277274
if(level == L0)
278-
set_l0_indices(ssa, ns);
275+
ssa = set_l0_indices(std::move(ssa), ns).get();
279276
else if(level == L1)
280277
set_l1_indices(ssa, ns);
281278
else

src/goto-symex/goto_symex_state.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ class goto_symex_statet final : public goto_statet
114114
void rename_address(exprt &expr, const namespacet &ns);
115115

116116
/// Update level 0 values.
117-
void set_l0_indices(ssa_exprt &expr, const namespacet &ns);
117+
renamedt<ssa_exprt, L0> set_l0_indices(ssa_exprt expr, const namespacet &ns);
118118

119119
/// Update level 0 and 1 values.
120120
void set_l1_indices(ssa_exprt &expr, const namespacet &ns);

0 commit comments

Comments
 (0)