Merge pull request #5968 from ArenBabikian/contracts-quantifiers-nested

Support nested quantifiers within function contracts

Author: SaswatPadhi

regression/contracts/quantifiers-nested-01/main.c

@@ -0,0 +1,24 @@
+// clang-format off
+int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  __CPROVER_forall
+  {
+    int j;
+    (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j]
+  }
+})
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-nested-01/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression
+nested within another forall expression.

regression/contracts/quantifiers-nested-02/main.c

@@ -0,0 +1,19 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  0 <= i && i < 9 ==> __CPROVER_forall
+  {
+    int j;
+    (i <= j && j < 10) ==> arr[i] <= arr[j]
+  }
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-nested-02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression
+nested within an implication.

regression/contracts/quantifiers-nested-03/main.c

@@ -0,0 +1,19 @@
+int f1(int *arr)
+  __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == i
+  })
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-nested-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of an exists expression
+nested within a conjunction.

regression/contracts/quantifiers-nested-04/main.c

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

regression/contracts/quantifiers-nested-04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of both a forall expression
+and an exists expression nested within a disjunction.

regression/contracts/quantifiers-nested-05/main.c

@@ -0,0 +1,15 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(!__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == 0
+  }) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-nested-05/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression
+nested within a negation.