Byte offset to array index translation must use array type

When dereferencing a void* pointer, the dereferenced type would always be
considered compatible with the underlying object type. Nevertheless they are not
actually the same. If the object was an array and the byte offset non-zero, the
use of void* would yield the wrong index. The correct way to compute the index
is using the actual (array) object type.

Fixes: #1857

Author: tautschnig

regression/cbmc/memcpy3/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  int A[3] = {1, 2, 3};
+  int *p = A;
+  int v1, v2;
+
+  memcpy(&v1, p, sizeof(int));
+  ++p;
+  memcpy(&v2, p, sizeof(int));
+
+  assert(v1 == 1);
+  assert(v2 == 2);
+
+  return 0;
+}

regression/cbmc/memcpy3/test.desc

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

src/pointer-analysis/value_set_dereference.cpp

@@ -508,10 +508,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       exprt adjusted_offset;
 
       // are we doing a byte?
-      mp_integer element_size=
-        dereference_type.id()==ID_empty?
-        pointer_offset_size(char_type(), ns):
-        pointer_offset_size(dereference_type, ns);
+      mp_integer element_size =
+        pointer_offset_size(root_object_type.subtype(), ns);
 
       if(element_size==1)
       {
@@ -520,7 +518,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       }
       else if(element_size<=0)
       {
-        throw "unknown or invalid type size of:\n"+dereference_type.pretty();
+        throw "unknown or invalid type size of:\n" +
+          root_object_type.subtype().pretty();
       }
       else
       {