Improved regression tests for invariant contract

- Moved comments from the source .c files to test case description in .desc files
- Added several new tests to check multiple loops, nested loops, loop-local index variables etc.
- Enabled one more regression test that was flagged as a buggy one

Author: SaswatPadhi

regression/contracts/invar_check_01/test.desc

@@ -1,17 +1,11 @@
-// invar_check_04
-
-// This test checks the handling of break by loop invariants.
-// This test is expected to fail along the code path where r is even before
-// entering the loop.
-
 #include <assert.h>
 
 int main()
 {
   int r;
   __CPROVER_assume(r >= 0);
 
-  while(r>0)
+  while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
   { 
     --r;
@@ -24,6 +18,7 @@ int main()
       --r;
     }
   }
+
   assert(r == 0);
 
   return 0;

regression/contracts/invar_check_02/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion r == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+This test is expected to fail along the code path where r is an even integer
+before entering the loop.
+The program is simply incompatible with the desired property in this case --
+there is no loop invariant that can establish the required assertion.

regression/contracts/invar_check_03/test.desc

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  { 
+    --r;
+    if (r <= 1)
+    {
+      break;
+    }
+    else
+    {
+      --r;
+    }
+  }
+
+  assert(r == 0 || r == 1);
+
+  return 0;
+}

regression/contracts/invar_check_04/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that conditionals and `break` are correctly handled.

regression/contracts/invar_check_04/main.c renamed to regression/contracts/invar_check_break_fail/main.c

@@ -1,7 +1,3 @@
-// invar_check_02
-
-// This test checks that loop invariants adequately handle continues.
-
 #include <assert.h>
 
 int main()

regression/contracts/invar_check_break_fail/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that conditionals and `continue` are correctly handled.