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

Value-set based dereferencing must not take an access path through an
object that precludes a subsequent index expression from accessing a
different part of the object. Such a situation can arise when the value
set has a known (constant) offset for the pointer that would identify
one particular element in an array (within that object). The code using
value-set based dereferencing, however, may be trying to resolve a
subexpression of an index expression, where said index expression would
lead to a different element that may itself be part of a different array
within the same overall object.

Fixes: #8570

Author: tautschnig

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))
     {