Skip to content

Commit bfbffdc

Browse files
Make public assign take level1t for rhs
1 parent 7289697 commit bfbffdc

File tree

5 files changed

+6
-6
lines changed

5 files changed

+6
-6
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ void goto_symex_statet::assignment(
234234
!check_renaming_l1(l1_rhs.expr), "rhs renaming failed on l1");
235235
}
236236

237-
value_set.assign(l1_lhs, l1_rhs.expr, ns, rhs_is_simplified, is_shared);
237+
value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
238238
}
239239

240240
#if 0

src/goto-symex/symex_dead.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ void goto_symext::symex_dead(statet &state)
4040

4141
level1t<exprt> l1_rhs = state.rename_level1(std::move(rhs), ns);
4242
// TODO: change assign to take a level1_exprt
43-
state.value_set.assign(l1_code, l1_rhs.expr, ns, true, false);
43+
state.value_set.assign(l1_code, l1_rhs, ns, true, false);
4444
}
4545

4646
ssa_exprt ssa_lhs = l1_code.expr;

src/goto-symex/symex_decl.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
5454
}();
5555

5656
level1t<exprt> l1_rhs = state.rename_level1(std::move(rhs), ns);
57-
state.value_set.assign(ssa, l1_rhs.expr, ns, true, false);
57+
state.value_set.assign(ssa, l1_rhs, ns, true, false);
5858
}
5959

6060
// prevent propagation

src/pointer-analysis/value_set.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1117,12 +1117,12 @@ void value_sett::get_reference_set_rec(
11171117

11181118
void value_sett::assign(
11191119
const level1t<ssa_exprt> &lhs,
1120-
const exprt &rhs,
1120+
const level1t<exprt> &rhs,
11211121
const namespacet &ns,
11221122
bool is_simplified,
11231123
bool add_to_sets)
11241124
{
1125-
assign(lhs.expr, rhs, ns, is_simplified, add_to_sets);
1125+
assign(lhs.expr, rhs.expr, ns, is_simplified, add_to_sets);
11261126
}
11271127

11281128
void value_sett::assign(

src/pointer-analysis/value_set.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -395,7 +395,7 @@ class value_sett
395395
/// `y` or `z` MAY, but not MUST, be overwritten.
396396
void assign(
397397
const level1t<ssa_exprt> &lhs,
398-
const exprt &rhs,
398+
const level1t<exprt> &rhs,
399399
const namespacet &ns,
400400
bool is_simplified,
401401
bool add_to_sets);

0 commit comments

Comments
 (0)