Add more tests, including failing test cases for the forall case

Author: NlightNFotis

regression/cbmc-primitives/forall_6231_1/test.c

@@ -1,6 +1,7 @@
 #include <assert.h>
 #include <stdlib.h>
 
+// clang-format off
 int main() {
   char *a = malloc(1);
 
@@ -14,3 +15,4 @@ int main() {
     }
   );
 }
+// clang-format on

regression/cbmc-primitives/forall_6231_2/test.c

@@ -1,6 +1,7 @@
 #include <assert.h>
 #include <stdlib.h>
 
+// clang-format off
 int main() {
   char *a = malloc(128);
 
@@ -15,3 +16,4 @@ int main() {
     int j; !(0 <= j && j < 1) || (j == 0 && *(a+j) == *(a+j))
   });
 }
+// clang-format on

regression/cbmc-primitives/forall_6231_3/test.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// This is essentially the same file as in test `forall_6231_1`, with the difference
+// being that the forall statement contains a bigger bound, so that we are to have
+// more concrete instantiations of the bound variable.
+
+// clang-format off
+int main() {
+  char *a = malloc(10);
+
+  // 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 < 10) ==> *(a+i) == *(a+i)
+    }
+  );
+}
+// clang-format on

regression/cbmc-primitives/forall_6231_3/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 < 10\) ==> \*\(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_3/test_malloc_less_than_bound.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// Similar to our test in `test.c` of this folder, with the difference being
+// that the malloc size is less than the bound checked, which implies that the
+// check for the pointer being outside the object bounds is expected to fail.
+
+// clang-format off
+int main() {
+  char *a = malloc(4);
+
+  // 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 < 10) ==> *(a+i) == *(a+i)
+    }
+  );
+}
+// clang-format on

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

@@ -0,0 +1,16 @@
+CORE
+test_malloc_less_than_bound.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(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\]: FAILURE
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
+^VERIFICATION FAILED$
+--
+--
+This is fixing an issue first reported in https://github.com/diffblue/cbmc/issues/6231