Finalizes quantifiers regression tests for ensures.

Author: Aren Babikian

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

@@ -0,0 +1,18 @@
+int f1(int *arr)
+  __CPROVER_ensures(
+    __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-exists-ensures-01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted

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

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

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

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

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

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

regression/contracts/quantifiers-forall-ensures-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-ensures-02/main.c

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

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

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