Enhance checks in regression tests of issue 6231.

Also, skip the `--z3` test on machines that don't have a z3 binary installed.

Author: NlightNFotis

regression/cbmc-primitives/CMakeLists.txt

@@ -1,3 +1,11 @@
-add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
-)
+find_program(Z3_EXISTS "z3")
+message(${Z3_EXISTS})
+if(Z3_EXISTS)
+    add_test_pl_tests(
+        "$<TARGET_FILE:cbmc>"
+    )
+else()
+    add_test_pl_tests(
+        "$<TARGET_FILE:cbmc>" -X smt-backend
+    )
+endif()

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

@@ -4,6 +4,7 @@ invalid_index_range.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: SUCCESS
 line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
 --
 --

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

@@ -4,7 +4,13 @@ negated_exists.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-line 9 dereference failure:.*SUCCESS
+\[main\.assertion\.1\] line 9 assertion !__CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == 42 \}: SUCCESS
+\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
 --
 --
 Check that memory checks pass for valid pointer dereferences inside a negated

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -1,4 +1,4 @@
-CORE
+CORE smt-backend
 smt_missing_range_check.c
 --pointer-check -z3
 ^EXIT=10$

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

@@ -4,7 +4,13 @@ valid_index_range.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-line 9 dereference failure:.*SUCCESS
+\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == i \*i \}: SUCCESS
+\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
 --
 --
 Check that memory checks pass for valid pointer dereferences inside an

regression/cbmc-primitives/forall_6231_1/test.c

@@ -7,7 +7,10 @@ int main() {
 
   assert(*a == *a);
 
-  // BUG: no errors even with `--pointer-check` enabled -- now fixed.
+  // BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
+  // no checks would be performed on the derefence inside the quantified statement,
+  // even when explicitly requested via for instance `--pointer-check`, because
+  // we would simply skip over these quantified statements in goto-check.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)

regression/cbmc-primitives/forall_6231_2/test.c

@@ -5,6 +5,10 @@
 int main() {
   char *a = malloc(128);
 
+  // BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
+  // no checks would be performed on the derefence inside the quantified statement,
+  // even when explicitly requested via for instance `--pointer-check`, because
+  // we would simply skip over these quantified statements in goto-check.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)

regression/cbmc-primitives/forall_6231_2/test.desc

@@ -4,12 +4,12 @@ test.c
 ^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|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.2\] line \d dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.3\] line \d dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.4\] line \d dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.5\] line \d dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.6\] line \d dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.1\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.2\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.3\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.4\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.5\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.6\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long 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|long long) int\)j\]: SUCCESS
 \[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)j\]: SUCCESS

regression/cbmc-primitives/forall_6231_3/test.c

@@ -11,7 +11,10 @@ int main() {
 
   assert(*a == *a);
 
-  // BUG: no errors even with `--pointer-check` enabled -- now fixed.
+  // BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
+  // no checks would be performed on the derefence inside the quantified statement,
+  // even when explicitly requested via for instance `--pointer-check`, because
+  // we would simply skip over these quantified statements in goto-check.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < 10) ==> *(a+i) == *(a+i)

regression/cbmc-primitives/forall_6231_4/test.c

@@ -10,6 +10,10 @@ int main() {
   char *a = malloc(10);
   int n;
 
+  // BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
+  // no checks would be performed on the derefence inside the quantified statement,
+  // even when explicitly requested via for instance `--pointer-check`, because
+  // we would simply skip over these quantified statements in goto-check.
   assert(
     __CPROVER_forall {
       int i ; (0 <= i && i < (n / 0))  /* (n / 0) should be caught by --div-by-zero-check */