Merge pull request #5823 from tautschnig/pointer-encoding-tests

Tests demonstrating pointer-encoding unsoundness

Author: tautschnig

regression/cbmc/Pointer_Arithmetic18/main.c

@@ -0,0 +1,11 @@
+#define MB 0x00100000
+#define BASE (15 * MB)
+#define OFFSET (1 * MB)
+
+main()
+{
+  char *base = BASE;
+  int offset = OFFSET;
+  __CPROVER_assert(
+    &((char *)base)[offset] >= BASE + OFFSET, "no wrap-around expected");
+}

regression/cbmc/Pointer_Arithmetic18/test.desc

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

regression/cbmc/Pointer_comparison1/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+int main()
+{
+  if(sizeof(void *) != 8)
+    return 0;
+
+  char *p = malloc(1);
+  if(p == 0)
+    return 0;
+
+  if(
+    (unsigned long)p >
+    42) // unsoundly evaluates to true due to pointer encoding
+  {
+    return 0;
+  }
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}

regression/cbmc/Pointer_comparison1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring