Test showing that loop-freeness check detects loops.

Author: Remi Delmas

regression/contracts/loop-freeness-check/main.c

@@ -0,0 +1,16 @@
+int foo(int *arr)
+  // clang-format off
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
+// clang-format off
+{
+  for(int i = 0; i < 10; i++)
+    arr[i] = i;
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  foo(arr);
+}

regression/contracts/loop-freeness-check/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo
+^--- begin invariant violation report ---$
+^Invariant check failed$
+^Condition: is_loop_free\(.*\)
+^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+This test checks that loops that remain in the program when attempting to 
+instrument assigns clauses are detected and trigger an INVARIANT.