Merge pull request #6145 from padhi-aws-forks/quantifiers-tests-fix

Cleanup regression tests for quantified contracts

Author: feliperodri

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

@@ -1,22 +1,20 @@
 // clang-format off
 int f1(int *arr)
-  __CPROVER_assigns(*arr)
+  __CPROVER_requires(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 8) && arr[i] == 0
+  })
   __CPROVER_ensures(__CPROVER_exists {
     int i;
-    (0 <= i && i < 10) ==> arr[i] == i
+    (0 <= i && i < 8) && arr[i] == 0
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
-
   return 0;
 }
 
 int main()
 {
-  int arr[10];
+  int arr[8];
   f1(arr);
 }

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

@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the ENSURES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.

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

@@ -0,0 +1,42 @@
+#include <stdlib.h>
+
+#define MAX_LEN 8
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_requires(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      )
+    }
+  )
+  __CPROVER_ensures(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      )
+    }
+  )
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len);
+  if(len > 0)
+    arr[0] = 0;
+
+  f1(arr, len);
+}

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

@@ -0,0 +1,16 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the REQUIRES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.