CONTRACTS: test combination of loop contracts and recursive functions

Author: Remi Delmas

regression/contracts-dfcc/recursive-function-and-loop-contracts/main.c

@@ -0,0 +1,68 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+int foo(char *arr, const size_t size, size_t offset)
+  // clang-format off
+__CPROVER_requires( 0 < size && offset <= size  && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(__CPROVER_object_whole(arr))
+// clang-format on
+{
+  if(offset == 0)
+    return 0;
+
+  // recursive call
+  foo(arr, size, offset - 1);
+
+  size_t i1 = offset;
+  while(i1 < size)
+    // clang-format off
+    __CPROVER_assigns(i1, __CPROVER_object_whole(arr))
+    __CPROVER_loop_invariant(i1 <= size)
+    __CPROVER_decreases(size - i1)
+    // clang-format on
+    {
+      static int local_static = 0;
+      local_static = 1;
+      arr[i1] = 1;
+      size_t i2 = offset;
+      while(i2 < size)
+        //clang-format off
+        __CPROVER_assigns(i2, __CPROVER_object_whole(arr))
+          __CPROVER_loop_invariant(i2 <= size) __CPROVER_decreases(size - i2)
+        //clang-format on
+        {
+          local_static = 2;
+          arr[i2] = 2;
+          i2++;
+        }
+      bool must_break = nondet_bool();
+      if(must_break)
+      {
+        size_t i3 = offset;
+        while(i3 < size)
+          // clang-format off
+          __CPROVER_assigns(i3, __CPROVER_object_whole(arr))
+          __CPROVER_loop_invariant(i3 <= size)
+          __CPROVER_decreases(size - i3)
+          // clang-format on
+          {
+            local_static = 3;
+            arr[i3] = 3;
+            i3++;
+          }
+        break;
+      }
+      i1++;
+    }
+}
+
+int main()
+{
+  char *arr;
+  size_t size;
+  size_t offset;
+  foo(arr, size, offset);
+}

regression/contracts-dfcc/recursive-function-and-loop-contracts/test.desc

@@ -0,0 +1,19 @@
+THOROUGH dfcc-only
+main.c
+--dfcc main --enforce-contract-rec foo --apply-loop-contracts --malloc-may-fail --malloc-fail-null _ --bounds-check --pointer-check --signed-overflow-check --unsigned-overflow-check --conversion-check --sat-solver cadical
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test illustrates the analysis of a function with a combination of features:
+- the function is recursive
+- the function contains loops
+- the function assigns local static variables
+
+The following write set checks are performed:
+- the write set of the recursive call is included in the caller'set
+- the write set of each loop is included in the outer write set, either the
+  function's write set or some loop's write set)
+- local statics are automatically detected and added to each write set
+- the instructions are checked against their respective write sets