Add a test for checks in the antecedent of a forall quantifier

Author: NlightNFotis

regression/cbmc-primitives/forall_6231_1/test.c

@@ -5,10 +5,9 @@
 int main() {
   char *a = malloc(1);
 
-  // lots of errors with `--pointer-check` enabled
   assert(*a == *a);
 
-  // no errors even with `--pointer-check` enabled
+  // BUG: no errors even with `--pointer-check` enabled -- now fixed.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)

regression/cbmc-primitives/forall_6231_3/test.c

@@ -9,10 +9,9 @@
 int main() {
   char *a = malloc(10);
 
-  // lots of errors with `--pointer-check` enabled
   assert(*a == *a);
 
-  // no errors even with `--pointer-check` enabled
+  // BUG: no errors even with `--pointer-check` enabled -- now fixed.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < 10) ==> *(a+i) == *(a+i)

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.c

@@ -9,10 +9,9 @@
 int main() {
   char *a = malloc(4);
 
-  // lots of errors with `--pointer-check` enabled
   assert(*a == *a);
 
-  // no errors even with `--pointer-check` enabled
+  // BUG: no errors even with `--pointer-check` enabled -- now fixed.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < 10) ==> *(a+i) == *(a+i)

regression/cbmc-primitives/forall_6231_4/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// Similar to the previous tests in forall_6231_1 but this one aims to check
+// the antecedent of the forall expression to make sure that checks are being
+// generated correctly for it.
+
+// clang-format off
+int main() {
+  char *a = malloc(10);
+  int n;
+
+  assert(
+    __CPROVER_forall {
+      int i ; (0 <= i && i < (n / 0))  /* (n / 0) should be caught by --div-by-zero-check */
+      ==> *(a+i) == *(a+i)
+    }
+  );
+}
+// clang-format on

regression/cbmc-primitives/forall_6231_4/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--div-by-zero-check
+^EXIT=10$
+^SIGNAL=0$
+\[main\.division-by-zero\.1] line \d+ division by zero in n / 0: FAILURE
+^VERIFICATION FAILED$
+--
+--
+--div-by-zero-check should catch the failure in the antecedent.
+--pointer-check doesn't but gives an pointer outside object bounds issue.