Adds tests for --expand-pointer-predicates

Author: klaas

regression/goto-instrument/expand-pointer-predicates1/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x));
+  *x = 1;
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates2/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int)));
+  *x = 1;
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates3/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int)));
+  __CPROVER_assert(
+    __CPROVER_points_to_valid_memory(x, sizeof(int)), "Assert matches assume");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates4/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x;
+  int *y = &x;
+  __CPROVER_assert(__CPROVER_points_to_valid_memory(y), "Assert works on &");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates5/main.c

@@ -0,0 +1,19 @@
+struct bar
+{
+  int w;
+  int x;
+  int y;
+  int z;
+};
+
+int main()
+{
+  struct bar s;
+  s.z = 5;
+  int *x_pointer = &(s.x);
+  __CPROVER_assert(
+    __CPROVER_points_to_valid_memory(x_pointer, 3 * sizeof(int)),
+    "Variable length assert");
+  assert(x_pointer[2] == 5);
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates5/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.assertion.1\] Variable length assert: SUCCESS$
+^\[main.assertion.2\] assertion x_pointer\[\(signed long( long)? int\)2\] == 5: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates6/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+struct my_struct
+{
+  int *field1;
+  int *field2;
+};
+
+void example(struct my_struct *s)
+{
+  s->field2 = malloc(sizeof(*(s->field2)));
+}
+
+int main()
+{
+  struct my_struct *s;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s));
+  example(s);
+  __CPROVER_assert(__CPROVER_points_to_valid_memory(s->field2), "");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates6/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.assertion.1\] : SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates7/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+struct my_struct
+{
+  int *field;
+};
+
+void example(struct my_struct *s)
+{
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s));
+  size_t size;
+  __CPROVER_assume(size == sizeof(*(s->field)));
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s->field, size));
+  int read = *(s->field);
+}
+
+int main()
+{
+  struct my_struct *s;
+  example(s);
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates7/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates8/main.c

@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *x;
+  int *y;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, 2 * sizeof(int)));
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(y, 2 * sizeof(int) - 1));
+  (void)(x[0]);  // Should succeed
+  (void)(x[1]);  // Should succeed
+  (void)(x[2]);  // Should fail
+  (void)(x[-1]); // Should fail
+  (void)(y[0]);  // Should succeed
+  (void)(y[1]);  // Should fail
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates8/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)1\]: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

regression/goto-instrument/expand-pointer-predicates9/main.c

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x));
+  (void)(*x);       // Should succeed
+  (void)(*(x + 1)); // Should fail
+  (void)(*(x - 1)); // Should fail
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates9/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--