Added detailed description to regression tests.

Author: klaas

regression/contracts/function_apply_01/main.c

@@ -1,8 +1,11 @@
-#include <assert.h>
+// function_apply_01
 
-// Note that this is supposed to have an incorrect contract.
+// Note that this test is supposed to have an incorrect contract.
 // We verify that applying (without checking) the contract yields success,
 // and that checking the contract yields failure.
+
+#include <assert.h>
+
 int foo() 
 __CPROVER_ensures(__CPROVER_return_value == 0)
 {

regression/contracts/function_check_01/main.c

@@ -1,3 +1,8 @@
+// function_check_01
+
+// This tests a simple example of a function with requires and
+// ensures which should both be satisfied.
+
 #include <assert.h>
 
 int min(int a, int b)

regression/contracts/function_check_02/main.c

@@ -1,3 +1,8 @@
+// function_check_02
+
+// This test checks the use of quantifiers in ensures clauses.
+// A known bug causes the use of quantifiers in ensures to fail.
+
 int initialize(int* arr)
 __CPROVER_ensures(
   __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}

regression/contracts/function_check_03/main.c

@@ -1,3 +1,10 @@
+// function_check_03
+
+// This extends function_check_02's test of quantifiers in ensures
+// and adds in a loop invariant which can be used to prove the ensures.
+// This currently fails because side-effect checking in loop invariants is
+// incorrect.
+
 void initialize(int* arr, int len)
 __CPROVER_ensures(
   __CPROVER_forall {int i; (0 <= i && i < len) ==> arr[i] == i}

regression/contracts/function_check_04/main.c

@@ -1,8 +1,10 @@
+// function_check_04
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that checking this faulty contract (correctly) yields a failure.
+
 #include <assert.h>
 
-// Note that this is supposed to have an incorrect contract.
-// We verify that applying (without checking) the contract yields success,
-// and that checking the contract yields failure.
 int foo() 
 __CPROVER_ensures(__CPROVER_return_value == 0)
 {

regression/contracts/function_check_05/main.c

@@ -1,3 +1,10 @@
+// function_check_05
+
+// This test checks that when a function call is replaced by an invariant,
+// it adequately havocs the locations modified by the function.
+// This test currently fails because the analysis of what is modified by
+// a function is flawed.
+
 #include <assert.h>
 
 int foo(int* x) 

regression/contracts/function_check_mem_01/main.c

@@ -1,3 +1,10 @@
+// function_check_mem_01
+
+// This test checks the use of pointer-related predicates in assumptions and
+// requires.
+// This test currently fails because of the lack of support for assuming
+// pointer predicates.
+
 #include <stddef.h>
 
 #define __CPROVER_VALID_MEM(ptr, size) \

regression/contracts/invar_check_01/main.c

@@ -1,3 +1,8 @@
+// invar_check_01
+
+// This test checks that a basic loop invariant can be proven and used in
+// combination with the negation of the loop guard to get a result.
+
 #include <assert.h>
 
 int main()

regression/contracts/invar_check_02/main.c

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

regression/contracts/invar_check_03/main.c

@@ -1,3 +1,10 @@
+// invar_check_03
+
+// This test checks the use of loop invariants on a larger problem --- in this
+// case, the partition portion of quicksort, applied to a fixed-length array.
+// This serves as a stop-gap test until issues to do with quantifiers and
+// side-effects in loop invariants are fixed.
+
 #include <stdio.h>
 #include <assert.h>
 

regression/contracts/invar_check_04/main.c

@@ -1,3 +1,9 @@
+// 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()

regression/contracts/invar_loop_constant/main.c

@@ -1,9 +1,16 @@
+// invar_loop_constant
+
+// This test checks to see whether loop invariant checking discards sufficiently
+// little information to be aware after the loop that s is necessarily 1.
+// This test currently fails due to excessive havocking in checking loop
+// invariants, but is not an obstacle to soundness of contract checking.
+
 #include <assert.h>
 
 int main() {
   int r;
-  int s;
-  __CPROVER_assume(r > 0);
+  int s = 1;
+  __CPROVER_assume(r >= 0);
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
   {

regression/contracts/quicksort_contracts_01/main.c

@@ -1,3 +1,13 @@
+// quicksort_contracts_01
+
+// This test checks the correctness of a quicksort implementation using explicit
+// ghost state.
+
+// This test currently fails for a variety of reasons, including:
+// (1) Lack of support for quantifiers in ensures statements.
+// (2) Lack of support for reading from memory in loop invariants (under some
+// circumstances)
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -32,13 +42,13 @@ __CPROVER_ensures(
   int pivot = arr[pivot_idx];
 
   while(h > l)
-/*  __CPROVER_loop_invariant(
+  __CPROVER_loop_invariant(
     0 <= l && l <= pivot_idx && pivot_idx <= h && h < len &&
     arr[pivot_idx] == pivot &&
     __CPROVER_forall {int i; (0 <= i && i < l) ==> arr[i] <= pivot} &&
     __CPROVER_forall {int i; (h < i && i < len) ==> pivot <= arr[i]} &&
     1 == 1
-  )*/
+  )
   {
     if(arr[h] <= pivot && arr[l] >= pivot) {
       swap(arr + h, arr + l);