Skip to content

Commit 3b8fa07

Browse files
committed
Value sets: try to extract pointers from any other expression
We must not lose information when seeing expressions we don't have a specific case for. An example of such an expression is concatenation.
1 parent 35dc5e7 commit 3b8fa07

File tree

1 file changed

+16
-1
lines changed

1 file changed

+16
-1
lines changed

src/pointer-analysis/value_set.cpp

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1071,7 +1071,22 @@ void value_sett::get_value_set_rec(
10711071
}
10721072
else
10731073
{
1074-
insert(dest, exprt(ID_unknown, original_type));
1074+
object_mapt pointer_expr_set;
1075+
for(const auto &op : expr.operands())
1076+
get_value_set_rec(op, pointer_expr_set, "", original_type, ns);
1077+
1078+
for(const auto &object_map_entry : pointer_expr_set.read())
1079+
{
1080+
offsett offset = object_map_entry.second;
1081+
1082+
// kill any offset
1083+
offset.reset();
1084+
1085+
insert(dest, object_map_entry.first, offset);
1086+
}
1087+
1088+
if(pointer_expr_set.read().empty())
1089+
insert(dest, exprt(ID_unknown, original_type));
10751090
}
10761091

10771092
#ifdef DEBUG

0 commit comments

Comments
 (0)