Add regression tests for quantifier checks.

These are checked against `--pointer-check` and one of them is
sourced from the code reported in #6231.

Author: NlightNFotis

regression/cbmc-primitives/forall_6231_1/test.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main() {
+  char *a = malloc(1);
+
+  // lots of errors with `--pointer-check` enabled
+  assert(*a == *a);
+
+  // no errors even with `--pointer-check` enabled
+  assert(
+    __CPROVER_forall {
+      int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
+    }
+  );
+}

regression/cbmc-primitives/forall_6231_1/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
+\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is fixing an issue first reported in https://github.com/diffblue/cbmc/issues/6231

regression/cbmc-primitives/forall_6231_2/test.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main() {
+  char *a = malloc(128);
+
+  assert(
+    __CPROVER_forall {
+      int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
+    }
+  );
+
+  assert(
+  __CPROVER_forall {
+    int j; !(0 <= j && j < 1) || (j == 0 && *(a+j) == *(a+j))
+  });
+}

regression/cbmc-primitives/forall_6231_2/test.desc

@@ -0,0 +1,23 @@
+CORE
+test.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
+\[main\.pointer_dereference\.1\] line \d dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.2\] line \d dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.3\] line \d dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.4\] line \d dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.5\] line \d dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.6\] line \d dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
+\[main\.assertion.2] line \d+ assertion __CPROVER_forall \{ int j; \!\(0 <= j && j < 1\) || \(j == 0 && \*\(a\+j\) == \*\(a+j\)\) \}: SUCCESS
+\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[\(signed long int\)j\]: SUCCESS
+\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed long int\)j\]: SUCCESS
+\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[\(signed long int\)j\]: SUCCESS
+\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[\(signed long int\)j\]: SUCCESS
+\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[\(signed long int\)j\]: SUCCESS
+\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)j\]: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is fixing an issue first reported in https://github.com/diffblue/cbmc/issues/6231