Add regression tests

Author: ArenBabikian

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

@@ -0,0 +1,15 @@
+#include <assert.h>
+void main()
+{
+  int N = 64, a[64];
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+      int k;
+      (0 <= k && k < N) ==> 1 == 1
+    })
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression within
+a loop invariant.
+This test case does not check correctness of the for loop.
+Instead, it is a trivial quantified expression to ensure that
+quantifiers can be handled in loop invariants.

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

@@ -0,0 +1,21 @@
+#include <assert.h>
+void main()
+{
+  int N = 64, a[64];
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+      int k;
+      (0 <= k && k < i) ==> a[k] == 1
+    })
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+  // clang-format off
+  assert(__CPROVER_forall {
+    int k;
+    (0 <= k && k < N) ==> a[k] == 1
+  });
+  // clang-format on
+}

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

@@ -0,0 +1,16 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression within
+a loop invariant.
+In this test, the quantified variable has a symbolic upper limit.
+
+Known Bug:
+Currently, cbmc (using the SAT back-end) does not support quantified
+expressions where the quantified variable has a symbolic range.

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

@@ -0,0 +1,22 @@
+#include <assert.h>
+void main()
+{
+  int N, a[64];
+  __CPROVER_assume(0 <= N && N < 64);
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+      int k;
+      (0 <= k && k < i) ==> a[k] == 1
+    })
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+  // clang-format off
+  assert(__CPROVER_forall {
+    int k;
+    (0 <= k && k < N) ==> a[k] == 1
+  });
+  // clang-format on
+}

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

@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression within
+a loop invariant.
+In this test, the quantified variable has a symbolic upper limit.
+Additionally, the number of loop iterations is also defined by a
+symbolic value.
+
+Known Bug:
+Currently, cbmc (using the SAT back-end) does not support quantified
+expressions where the quantified variable has a symbolic range.