Add support for nested quantifiers in function contracts

This adds support for nested quantifiers in funtion contracts.
We recursively handle quantifiers that are nested within other
quantifiers or within Boolean connectives.

Author: ArenBabikian

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.