Skip to content

Commit 2c34886

Browse files
Replace use of get_l1_object by remove_level_2
get_l1_object suggests we are comparing the address of the object, but the actually should interpret the symbol itself as a pointer. A unit test for the case of the issue that is fixed will be added in a following commit.
1 parent 1c01ee7 commit 2c34886

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,10 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
100100
const ssa_exprt *ssa_symbol_expr =
101101
expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
102102

103+
ssa_exprt l1_expr{*ssa_symbol_expr};
104+
l1_expr.remove_level_2();
103105
const std::vector<exprt> value_set_elements =
104-
value_set.get_value_set(ssa_symbol_expr->get_l1_object(), ns);
106+
value_set.get_value_set(l1_expr, ns);
105107

106108
bool constant_found = false;
107109

0 commit comments

Comments
 (0)