Skip to content

Commit e16f2fc

Browse files
remove_level2 function returning a level1t<exprt>
Make clearer that remove_level2 returns an expression renamed up to level 1.
1 parent a037292 commit e16f2fc

File tree

1 file changed

+4
-5
lines changed

1 file changed

+4
-5
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -212,17 +212,16 @@ void goto_symex_statet::assignment(
212212
// update value sets
213213
exprt l1_rhs(rhs);
214214
get_l1_name(l1_rhs);
215-
216-
ssa_exprt l1_lhs(lhs);
217-
l1_lhs.remove_level_2();
215+
level1t<ssa_exprt> l1_lhs = remove_level2(lhs);
218216

219217
if(run_validation_checks)
220218
{
221-
DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
219+
DATA_INVARIANT(
220+
!check_renaming_l1(l1_lhs.expr), "lhs renaming failed on l1");
222221
DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
223222
}
224223

225-
value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
224+
value_set.assign(l1_lhs.expr, l1_rhs, ns, rhs_is_simplified, is_shared);
226225
}
227226

228227
#if 0

0 commit comments

Comments
 (0)