Fixed test descriptions to put comments in the correct place and updated some stylistic issues with test cases.

klaas · klaas · commit 9d2bfdaef8fa · 2018-06-06T17:34:56.000-04:00
diff --git a/regression/contracts/function_apply_01/main.c b/regression/contracts/function_apply_01/main.c
@@ -12,7 +12,8 @@ __CPROVER_ensures(__CPROVER_return_value == 0)
   return 1;
 }
 
-int main() {
+int main()
+{
   int x = foo();
   assert(x == 0);
   return 0;
diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # Applying code contracts currently also checks them.
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Applying code contracts currently also checks them.
diff --git a/regression/contracts/function_check_01/main.c b/regression/contracts/function_check_01/main.c
@@ -12,9 +12,12 @@ int min(int a, int b)
                    (__CPROVER_return_value == a || __CPROVER_return_value == b)
                    )
 {
-  if (a <= b) {
+  if (a <= b)
+  {
     return a;
-  } else {
+  }
+  else
+  {
     return b;
   }
 }
diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # --check-code-contracts not implemented yet.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c
@@ -8,14 +8,16 @@ __CPROVER_ensures(
   __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
 )
 {
-  for(int i = 0; i < 10; i++) {
+  for(int i = 0; i < 10; i++)
+  {
     arr[i] = i;
   }
 
   return 0;
 }
 
-int main() {
+int main()
+{
   int arr[10];
   initialize(arr);
 }
diff --git a/regression/contracts/function_check_02/test.desc b/regression/contracts/function_check_02/test.desc
@@ -1,6 +1,10 @@
-KNOWNBUG # Ensures statements currently do not allow quantified predicates unless the function has void return type.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Ensures statements currently do not allow quantified predicates unless the
+function has void return type.
diff --git a/regression/contracts/function_check_03/main.c b/regression/contracts/function_check_03/main.c
@@ -19,7 +19,8 @@ __CPROVER_ensures(
   }
 }
 
-int main() {
+int main()
+{
   int arr[10];
   initialize(arr, 10);
 }
diff --git a/regression/contracts/function_check_03/test.desc b/regression/contracts/function_check_03/test.desc
@@ -1,6 +1,10 @@
-KNOWNBUG # Loop invariants currently do not support memory reads.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariants currently do not support memory reads in at least some
+circumstances.
diff --git a/regression/contracts/function_check_04/main.c b/regression/contracts/function_check_04/main.c
@@ -11,7 +11,8 @@ __CPROVER_ensures(__CPROVER_return_value == 0)
   return 1;
 }
 
-int main() {
+int main()
+{
   int x = foo();
   assert(x == 0);
   return 0;
diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # --check-code-contracts not implemented yet.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^\[main.assertion.1\] assertion x == 0: SUCCESS$
 ^\[foo.1\] : FAILURE$
 ^VERIFICATION FAILED$
+--
+--
+--check-code-contracts not implemented yet.
diff --git a/regression/contracts/function_check_05/main.c b/regression/contracts/function_check_05/main.c
@@ -14,7 +14,8 @@ __CPROVER_ensures(__CPROVER_return_value == 1)
   return 1;
 }
 
-int main() {
+int main()
+{
   int y = 0;  
   int z = foo(&y);
   // This assert should fail.
diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc
@@ -1,8 +1,10 @@
-KNOWNBUG # Contract checking does not properly havoc function calls
+KNOWNBUG
 main.c
 --check-code-contracts
 ^\[main.assertion.1\] assertion y == 0: FAILURE$
 ^\[main.assertion.2\] assertion z == 1: SUCCESS$
 ^\[foo.1\] : SUCCESS$
-
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Contract checking does not properly havoc function calls.
diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c
@@ -10,13 +10,17 @@
 #define __CPROVER_VALID_MEM(ptr, size) \
   __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
   !__CPROVER_invalid_pointer((ptr)) && \
-  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
-  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
-  (__builtin_object_size((ptr), 1) >= (size) && __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
+  __CPROVER_POINTER_OBJECT((ptr)) != \
+  __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
+  __CPROVER_POINTER_OBJECT((ptr)) != \
+  __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
+  (__builtin_object_size((ptr), 1) >= (size) && \
+  __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
    __CPROVER_DYNAMIC_OBJECT((ptr))) && \
   (__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \
    __CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \
-   __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
+   __CPROVER_POINTER_OBJECT((ptr)) != \
+   __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
     
 typedef struct bar {
   int x;
@@ -31,7 +35,8 @@ __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
   return
 }
 
-int main() {
+int main()
+{
   bar* y;
   __CPROVER_assume(__CPROVER_VALID_MEM(y, sizeof(bar)));
   y->x = 0;
diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc
@@ -1,6 +1,10 @@
-KNOWNBUG # cbmc currently does not support assumptions about pointers.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+CBMC currently does not support assumptions about pointers in the general way
+that other assumptions are supported.
diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # --check-code-contracts not implemented yet.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # --check-code-contracts not implemented yet.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # --check-code-contracts not implemented yet.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc
@@ -1,7 +1,10 @@
-KNOWNBUG # --check-code-contracts not implemented yet.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^\[main.1\] Loop invariant violated before entry: SUCCESS$
 ^\[main.2\] Loop invariant not preserved: SUCCESS$
 ^\[main.assertion.1\] assertion r==0: FAILURE$
 ^VERIFICATION FAILED$
+--
+--
+--check-code-contracts not implemented yet.
diff --git a/regression/contracts/invar_loop_constant/main.c b/regression/contracts/invar_loop_constant/main.c
@@ -7,7 +7,8 @@
 
 #include <assert.h>
 
-int main() {
+int main()
+{
   int r;
   int s = 1;
   __CPROVER_assume(r >= 0);
diff --git a/regression/contracts/invar_loop_constant/test.desc b/regression/contracts/invar_loop_constant/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # Loop invariant checking throws away more information than needed.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariant checking throws away more information than needed.
diff --git a/regression/contracts/quicksort_contracts_01/main.c b/regression/contracts/quicksort_contracts_01/main.c
@@ -50,21 +50,26 @@ __CPROVER_ensures(
     1 == 1
   )
   {
-    if(arr[h] <= pivot && arr[l] >= pivot) {
+    if(arr[h] <= pivot && arr[l] >= pivot)
+    {
       swap(arr + h, arr + l);
-      if(pivot_idx == h) {
+      if(pivot_idx == h)
+      {
         pivot_idx = l;
         h--;
       }
-      if(pivot_idx == l) {
+      if(pivot_idx == l)
+      {
         pivot_idx = h;
         l++;
       }
     }
-    else if(arr[h] <= pivot) {
+    else if(arr[h] <= pivot)
+    {
       l++;
     }
-    else {
+    else
+    {
       h--;
     }
   }
@@ -83,7 +88,8 @@ __CPROVER_ensures(
   1 == 1
 )
 {
-  if (len <= 1) {
+  if (len <= 1)
+  {
     return;
   }
   int* new_ghost = malloc(len * sizeof(int));
@@ -99,7 +105,8 @@ __CPROVER_ensures(
   free(new_ghost);
 }
 
-int main() {
+int main()
+{
   int arr[5] = {1, 2, 3, 0, 4};
   int arr_ghost[5] = {1, 2, 3, 0, 4};
   quicksort(arr_ghost, arr, 5);
diff --git a/regression/contracts/quicksort_contracts_01/test.desc b/regression/contracts/quicksort_contracts_01/test.desc
@@ -1,6 +1,9 @@
-KNOWNBUG # Loop invariants are overzealous in deciding what counts as side effects.
+KNOWNBUG
 main.c
 --check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariants are overzealous in deciding what counts as side effects.

Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,8 @@ __CPROVER_ensures(__CPROVER_return_value == 0)`
`12`	`12`	`return 1;`
`13`	`13`	`}`
`14`	`14`
`15`		`-int main() {`
	`15`	`+int main()`
	`16`	`+{`
`16`	`17`	`int x = foo();`
`17`	`18`	`assert(x == 0);`
`18`	`19`	`return 0;`
Original file line number	Diff line number	Diff line change
`@@ -12,9 +12,12 @@ int min(int a, int b)`
`12`	`12`	`(__CPROVER_return_value == a \|\| __CPROVER_return_value == b)`
`13`	`13`	`)`
`14`	`14`	`{`
`15`		`- if (a <= b) {`
	`15`	`+ if (a <= b)`
	`16`	`+ {`
`16`	`17`	`return a;`
`17`		`- } else {`
	`18`	`+ }`
	`19`	`+ else`
	`20`	`+ {`
`18`	`21`	`return b;`
`19`	`22`	`}`
`20`	`23`	`}`
Original file line number	Diff line number	Diff line change
`@@ -8,14 +8,16 @@ __CPROVER_ensures(`
`8`	`8`	`__CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}`
`9`	`9`	`)`
`10`	`10`	`{`
`11`		`- for(int i = 0; i < 10; i++) {`
	`11`	`+ for(int i = 0; i < 10; i++)`
	`12`	`+ {`
`12`	`13`	`arr[i] = i;`
`13`	`14`	`}`
`14`	`15`
`15`	`16`	`return 0;`
`16`	`17`	`}`
`17`	`18`
`18`		`-int main() {`
	`19`	`+int main()`
	`20`	`+{`
`19`	`21`	`int arr[10];`
`20`	`22`	`initialize(arr);`
`21`	`23`	`}`
Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,8 @@ __CPROVER_ensures(`
`19`	`19`	`}`
`20`	`20`	`}`
`21`	`21`
`22`		`-int main() {`
	`22`	`+int main()`
	`23`	`+{`
`23`	`24`	`int arr[10];`
`24`	`25`	`initialize(arr, 10);`
`25`	`26`	`}`
Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,8 @@ __CPROVER_ensures(__CPROVER_return_value == 0)`
`11`	`11`	`return 1;`
`12`	`12`	`}`
`13`	`13`
`14`		`-int main() {`
	`14`	`+int main()`
	`15`	`+{`
`15`	`16`	`int x = foo();`
`16`	`17`	`assert(x == 0);`
`17`	`18`	`return 0;`
Original file line number	Diff line number	Diff line change
`@@ -14,7 +14,8 @@ __CPROVER_ensures(__CPROVER_return_value == 1)`
`14`	`14`	`return 1;`
`15`	`15`	`}`
`16`	`16`
`17`		`-int main() {`
	`17`	`+int main()`
	`18`	`+{`
`18`	`19`	`int y = 0;`
`19`	`20`	`int z = foo(&y);`
`20`	`21`	`// This assert should fail.`
Original file line number	Diff line number	Diff line change
`@@ -50,21 +50,26 @@ __CPROVER_ensures(`
`50`	`50`	`1 == 1`
`51`	`51`	`)`
`52`	`52`	`{`
`53`		`- if(arr[h] <= pivot && arr[l] >= pivot) {`
	`53`	`+ if(arr[h] <= pivot && arr[l] >= pivot)`
	`54`	`+ {`
`54`	`55`	`swap(arr + h, arr + l);`
`55`		`- if(pivot_idx == h) {`
	`56`	`+ if(pivot_idx == h)`
	`57`	`+ {`
`56`	`58`	`pivot_idx = l;`
`57`	`59`	`h--;`
`58`	`60`	`}`
`59`		`- if(pivot_idx == l) {`
	`61`	`+ if(pivot_idx == l)`
	`62`	`+ {`
`60`	`63`	`pivot_idx = h;`
`61`	`64`	`l++;`
`62`	`65`	`}`
`63`	`66`	`}`
`64`		`- else if(arr[h] <= pivot) {`
	`67`	`+ else if(arr[h] <= pivot)`
	`68`	`+ {`
`65`	`69`	`l++;`
`66`	`70`	`}`
`67`		`- else {`
	`71`	`+ else`
	`72`	`+ {`
`68`	`73`	`h--;`
`69`	`74`	`}`
`70`	`75`	`}`
`@@ -83,7 +88,8 @@ __CPROVER_ensures(`
`83`	`88`	`1 == 1`
`84`	`89`	`)`
`85`	`90`	`{`
`86`		`- if (len <= 1) {`
	`91`	`+ if (len <= 1)`
	`92`	`+ {`
`87`	`93`	`return;`
`88`	`94`	`}`
`89`	`95`	`int* new_ghost = malloc(len * sizeof(int));`
`@@ -99,7 +105,8 @@ __CPROVER_ensures(`
`99`	`105`	`free(new_ghost);`
`100`	`106`	`}`
`101`	`107`
`102`		`-int main() {`
	`108`	`+int main()`
	`109`	`+{`
`103`	`110`	`int arr[5] = {1, 2, 3, 0, 4};`
`104`	`111`	`int arr_ghost[5] = {1, 2, 3, 0, 4};`
`105`	`112`	`quicksort(arr_ghost, arr, 5);`