Skip to content

Commit 71896a6

Browse files
Replace use of get_l1_object by remove_level_2
1 parent d5b3b89 commit 71896a6

File tree

2 files changed

+5
-2
lines changed

2 files changed

+5
-2
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 4 additions & 2 deletions
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-
const std::vector<exprt> value_set_elements =
104-
value_set.get_value_set(ssa_symbol_expr->get_l1_object(), ns);
103+
ssa_exprt l1_expr{*ssa_symbol_expr};
104+
l1_expr.remove_level_2();
105+
const std::vector<exprt> value_set_elements = value_set.get_value_set(
106+
l1_expr, ns);
105107

106108
bool constant_found = false;
107109

src/util/ssa_expr.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ class ssa_exprt:public symbol_exprt
4242

4343
irep_idt get_object_name() const;
4444

45+
/// TODO: this is not correct for array field sensitivity
4546
const ssa_exprt get_l1_object() const;
4647

4748
const irep_idt get_l1_object_identifier() const;

0 commit comments

Comments
 (0)