Add tests of memory checks inside existential qualifiers

Author: thomasspriggs

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *a = calloc(10, sizeof(int));
+  a[5] = 25;
+
+  assert(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 20) && a[i] == i *i
+  });
+}

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

@@ -0,0 +1,11 @@
+CORE
+invalid_index_range.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 9 dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: FAILURE
+--
+--
+Check that memory checks fail for pointer dereferences inside an existential
+qualifier, for out of bounds memory access.

regression/cbmc-primitives/exists_memory_checks/negated_exists.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *a = calloc(10, sizeof(int));
+  a[5] = 25;
+
+  assert(!__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && a[i] == 42
+  });
+}

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

@@ -0,0 +1,11 @@
+CORE
+valid_index_range.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+line 9 dereference failure:.*SUCCESS
+--
+--
+Check that memory checks pass for valid pointer dereferences inside a negated
+existential qualifier.

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *a = calloc(10, sizeof(int));
+  a[5] = 25;
+
+  assert(__CPROVER_exists {
+    int i;
+    a[i] == i *i
+  });
+}

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -0,0 +1,15 @@
+CORE
+smt_missing_range_check.c
+--pointer-check -z3
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
+\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: FAILURE
+--
+--
+Check that memory checks fail for pointer dereferences inside an existential
+qualifier, for out of bounds memory access, when using the smt backend and
+the range of the index is unbound. Note that this test is not expected to work
+with the SAT backend at the time of writing, as the SAT backend does not support
+qualifiers in this form.

regression/cbmc-primitives/exists_memory_checks/valid_index_range.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *a = calloc(10, sizeof(int));
+  a[5] = 25;
+
+  assert(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && a[i] == i *i
+  });
+}

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

@@ -0,0 +1,11 @@
+CORE
+valid_index_range.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+line 9 dereference failure:.*SUCCESS
+--
+--
+Check that memory checks pass for valid pointer dereferences inside an
+existential qualifier.