Adjusts regresison tests according to code review

Author: ArenBabikian

regression/contracts/function_check_02/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --enforce-all-contracts
 ^EXIT=0$

regression/contracts/quantifiers-exists-ensures-01/main.c

@@ -1,7 +1,9 @@
+// clang-format off
 int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
   int i;
-  (0 <= i && i < 10) && arr[i] == i
+  (0 <= i && i < 10) ==> arr[i] == i
 })
+// clang-format on
 {
   for(int i = 0; i < 10; i++)
   {

regression/contracts/quantifiers-exists-ensures-01/test.desc

@@ -6,5 +6,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Verification:
-This test asserts the postconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_exists
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, 
+goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.

regression/contracts/quantifiers-exists-ensures-02/main.c

@@ -1,7 +1,9 @@
+// clang-format off
 int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
   int i;
-  (0 <= i && i < 10) && arr[i] != 0
+  (0 <= i && i < 10) ==> arr[i] != 0
 })
+// clang-format on
 {
   for(int i = 0; i < 10; i++)
   {

regression/contracts/quantifiers-exists-ensures-02/test.desc

@@ -1,10 +1,19 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 --
-Verification:
-This test asserts the postconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_exists
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, 
+goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.
+
+Known Bug:
+We expect verification to fail because arr[i] is always equal to 0 for
+[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
+range for i. However, in the current implementation of quantifier handling,
+the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
+instead, as part of a logic formula, which causes verification to succeed.

regression/contracts/quantifiers-exists-requires-01/main.c

@@ -1,7 +1,9 @@
+// clang-format off
 int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
   int i;
-  (0 <= i && i < 10) && arr[i] == 4
+  (0 <= i && i < 10) ==> arr[i] == 4
 }) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
 {
   return 0;
 }

regression/contracts/quantifiers-exists-requires-01/test.desc

@@ -6,5 +6,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Verification:
-This test asserts the preconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_exists
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.

regression/contracts/quantifiers-exists-requires-02/main.c

@@ -1,7 +1,9 @@
+// clang-format off
 int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
   int i;
-  (0 <= i && i < 10) && arr[i] == 1
+  (0 <= i && i < 10) ==> arr[i] == 1
 }) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
 {
   return 0;
 }

regression/contracts/quantifiers-exists-requires-02/test.desc

@@ -1,10 +1,19 @@
-CORE
+KNOWNBUG
 main.c
 --replace-all-calls-with-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 --
-Verification:
-This test asserts the preconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_exists
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.
+
+Known Bug:
+We expect verification to fail because arr[i] is never equal to 1 for
+[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
+range for i. However, in the current implementation of quantifier handling,
+the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
+instead, as part of a logic formula, which causes verification to succeed.

regression/contracts/quantifiers-forall-ensures-01/test.desc

@@ -1,10 +1,12 @@
 CORE
 main.c
---replace-all-calls-with-contracts
+--enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Verification:
-This test asserts the preconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_forall
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts
+flag, goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.

regression/contracts/quantifiers-forall-ensures-02/test.desc

@@ -6,5 +6,7 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Verification:
-This test asserts the postconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_forall
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts
+flag, goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.

regression/contracts/quantifiers-forall-requires-01/test.desc

@@ -6,5 +6,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Verification:
-This test asserts the preconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_forall
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.

regression/contracts/quantifiers-forall-requires-02/test.desc

@@ -6,5 +6,7 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Verification:
-This test asserts the preconditions of f1.
+The purpose of this test is to ensure that we can safety use __CPROVER_forall
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.