From 0efab54b6143b96fea100a0546e477acd761f5f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Jun 2025 12:45:25 +0000 Subject: [PATCH] Flow-insensitive value set: don't create index expressions over non-array objects When evaluating an index expression, the value set must ignore pointed-to objects that are neither arrays nor vectors. Any appearance of such objects should produce `unknown` instead. (Trying to create an `index_exprt` with neither an array nor a vector as root object will fail an invariant.) --- src/pointer-analysis/value_set_fi.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index bf634d07264..f14c7dc7ed0 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -905,8 +905,12 @@ void value_set_fit::get_reference_set_sharing_rec( { const exprt &object = object_numbering[object_entry.first]; - if(object.id()==ID_unknown) + if( + object.id() == ID_unknown || + (object.type().id() != ID_array && object.type().id() != ID_vector)) + { insert(dest, exprt(ID_unknown, expr.type())); + } else { index_exprt index_expr(