Add regression test for object accessed through integer pointer

Author: danpoe

regression/cbmc/integer-pointer/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  assert(__CPROVER_POINTER_OBJECT(p) == 2);
+
+  // same value as the malloc'd pointer above
+  char *q = (char *)((size_t)2 << sizeof(char *) * 8 - 8);
+
+  *p = 1;
+  *q = 2;
+
+  assert(*p == 1); // currently succeeds
+}

regression/cbmc/integer-pointer/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring