Merge pull request #8578 from tautschnig/bugfixes/8570-pointer-and-array

Value-set based dereferencing: fix simplified handling of *(p + i)

regression/cbmc/Pointer_array8/main.c

@@ -0,0 +1,21 @@
+#pragma pack(push)
+#pragma pack(1)
+typedef struct
+{
+  int data[2];
+} arr;
+
+typedef struct
+{
+  arr vec[2];
+} arrvec;
+#pragma pack(pop)
+
+int main()
+{
+  arrvec A;
+  arrvec *x = &A;
+  __CPROVER_assume(x->vec[1].data[0] < 42);
+  unsigned k;
+  __CPROVER_assert(k != 2 || ((int *)x)[k] < 42, "");
+}

regression/cbmc/Pointer_array8/test.desc

@@ -0,0 +1,8 @@
+CORE no-new-smt
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/array-cell-sensitivity15/test.desc

@@ -3,9 +3,8 @@ access.c
 --program-only
 ^EXIT=0$
 ^SIGNAL=0$
-s!0@1#2\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
+s!0@1#2\.\.n ==.*\{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] \}
 --
-byte_update
 --
 This tests applying field-sensitivity to a pointer to an array that is part of a struct. See cbmc issue #5397 and PR #5418 for more detail.
 Disabled for paths-lifo mode, which does not support --program-only.

src/pointer-analysis/value_set_dereference.cpp

@@ -196,6 +196,7 @@ exprt value_set_dereferencet::dereference(
 
     if(
       can_cast_type<pointer_typet>(pointer_expr.type()) &&
+      pointer_expr.id() != ID_typecast &&
       !can_cast_type<pointer_typet>(offset_expr.type()) &&
       !can_cast_expr<constant_exprt>(offset_expr))
     {

src/util/pointer_offset_size.cpp

@@ -564,14 +564,7 @@ std::optional<exprt> get_subexpression_at_offset(
   const namespacet &ns)
 {
   if(offset_bytes == 0 && expr.type() == target_type_raw)
-  {
-    exprt result = expr;
-
-    if(expr.type() != target_type_raw)
-      result.type() = target_type_raw;
-
-    return result;
-  }
+    return expr;
 
   if(
     offset_bytes == 0 && expr.type().id() == ID_pointer &&