Test showing that loop-freeness check detects loops.

Author: Remi Delmas

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

@@ -0,0 +1,16 @@
+// clang-format off
+int foo(int *arr)
+  __CPROVER_assigns(*arr)
+// clang-format on
+{
+  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\(goto_program\)$
+^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$
+^EXIT=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.