Merge pull request #5326 from danpoe/tests/integer-pointer

Add regression test for object accessed through integer pointer

Author: tautschnig

regression/cbmc/integer-pointer/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  __CPROVER_assume(__CPROVER_POINTER_OBJECT(p) == 2);
+  assert(0); // fails as expected
+
+  // 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,13 @@
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] .*: FAILURE
+\[main.assertion.2\] .*: FAILURE
+--
+^warning: ignoring
+--
+The assertion should fail as q has the same value as p. However since q was
+initialized via an integer literal it points into __CPROVER_memory, and not to
+the malloced memory. Issue #5327.