Adds quantifiers regression tests for requires.

Author: ArenBabikian

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

@@ -0,0 +1,14 @@
+int f1(int *arr)
+  __CPROVER_requires(
+    __CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == 4}
+  )
+  __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0,1,2,3,4,5,6,7,8,9};
+  f1(arr);
+}

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test asserts the preconditions of f1.

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

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

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test asserts the preconditions of f1.

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

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

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test asserts the preconditions of f1.

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

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

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test asserts the preconditions of f1.