Regression test to check pointer havocing in loops

Author: SaswatPadhi

regression/contracts/invar_check_pointer_modifies-01/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *data = malloc(1);
+  *data = 42;
+
+  unsigned i;
+  while(i > 0)
+    __CPROVER_loop_invariant(*data == 42)
+    {
+      *data = 42;
+      i--;
+    }
+
+  assert(*data = 42);
+}

regression/contracts/invar_check_pointer_modifies-01/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion \*data = 42: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
+--
+This test checks that modifications to deref-ed pointers are correctly handled.
+In such cases, pointers should not be havoc'ed, only the value should be.

regression/contracts/invar_check_pointer_modifies-02/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *copy, *data = malloc(1);
+
+  copy = data;
+  *data = 42;
+
+  unsigned i;
+  while(i > 0)
+    __CPROVER_loop_invariant(*data == 42)
+    {
+      *data = 42;
+      i--;
+    }
+
+  assert(data == copy);
+  assert(*copy = 42);
+}

regression/contracts/invar_check_pointer_modifies-02/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion data == copy: SUCCESS$
+^\[main.assertion.2\] .* assertion \*copy = 42: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
+--
+This test checks that modifications to aliased pointers are correctly handled.