Merge pull request #5324 from danpoe/tests/cprover-memory-primitives

Add tests to check semantics of pointer primitives

Author: danpoe

regression/cbmc-primitives/dynamic-object-01/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  assert(__CPROVER_DYNAMIC_OBJECT(p));
+  assert(!__CPROVER_DYNAMIC_OBJECT(p));
+}

regression/cbmc-primitives/dynamic-object-01/test-no-cp.desc

@@ -0,0 +1,14 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is havoc'd when dynamic objects are
+deallocated. We use --no-simplify and --no-propagation to ensure that the case
+is not solved by the constant propagation and thus tests the constraint
+encoding. Recorded as ADA-526.

regression/cbmc-primitives/dynamic-object-01/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is havoc'd when dynamic objects are
+deallocated. Recorded as ADA-526.

regression/cbmc-primitives/dynamic-object-02/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+
+  assert(__CPROVER_DYNAMIC_OBJECT(p));
+  assert(!__CPROVER_DYNAMIC_OBJECT(p));
+}

regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc

@@ -0,0 +1,14 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is nondet for uninitialized pointers. We
+use --no-simplify and --no-propagation to ensure that the case is not solved by
+the constant propagation and thus tests the constraint encoding. Recorded as
+ADA-526.

regression/cbmc-primitives/dynamic-object-02/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+\[main.assertion.2\] line \d+ assertion !__CPROVER_DYNAMIC_OBJECT\(p\): FAILURE
+--
+^warning: ignoring
+--
+Check that the dynamic object property is nondet for uninitialized pointers.
+Recorded as ADA-526.

regression/cbmc-primitives/object-size-01/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  assert(__CPROVER_OBJECT_SIZE(p) == 1);
+  assert(__CPROVER_OBJECT_SIZE(p) != 1);
+
+  {
+    char c;
+    p = &c;
+  }
+
+  assert(__CPROVER_OBJECT_SIZE(p) == 1);
+  assert(__CPROVER_OBJECT_SIZE(p) != 1);
+}

regression/cbmc-primitives/object-size-01/test-no-cp.desc

@@ -0,0 +1,16 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+\[main.assertion.3\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.4\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+--
+^warning: ignoring
+--
+Check that object size is havoc'd when objects are deallocated. We use
+--no-simplify and --no-propagation to ensure that the case is not solved by the
+constant propagation and thus tests the constraint encoding. Recorded as
+ADA-527.

regression/cbmc-primitives/object-size-01/test.desc

@@ -0,0 +1,14 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+\[main.assertion.3\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) == 1: FAILURE
+\[main.assertion.4\] line \d+ assertion __CPROVER_OBJECT_SIZE\(p\) != 1: FAILURE
+--
+^warning: ignoring
+--
+Check that object size is havoc'd when objects are deallocated. Recorded as
+ADA-527.

regression/cbmc-primitives/pointer-offset-01/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+void main()
+{
+  char *p;
+  assert(__CPROVER_POINTER_OFFSET(p) >= 0);
+  assert(__CPROVER_POINTER_OFFSET(p) < 0);
+}