Add tests to check semantics of pointer primitives

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);
+}

regression/cbmc-primitives/pointer-offset-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_POINTER_OFFSET\(p\) >= 0: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
+--
+^warning: ignoring
+--
+Check that both positive and negative offsets can be chosen 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-528.

regression/cbmc-primitives/pointer-offset-01/test.desc

@@ -0,0 +1,12 @@
+FUTURE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+\[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
+--
+^warning: ignoring
+--
+Check that both positive and negative offsets can be chosen for uninitialized
+pointers. Recorded as ADA-528.

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

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  assert(__CPROVER_POINTER_OBJECT(p) == 2);
+
+  assert(
+    __CPROVER_same_object(p, (char *)((size_t)2 << (sizeof(char *) * 8 - 8))));
+  assert(
+    !__CPROVER_same_object(p, (char *)((size_t)3 << (sizeof(char *) * 8 - 8))));
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer variable, and an
+integer address pointing to the same object. 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.

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

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer variable, and an
+integer address pointing to the same object

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

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p1 = malloc(1);
+  char *p2 = malloc(1);
+
+  assert(!__CPROVER_same_object(p1, p2));
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers to different
+malloc'd objects. 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.

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

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers to different
+malloc'd objects

regression/cbmc-primitives/same-object-03/main.c

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

regression/cbmc-primitives/same-object-03/test-no-cp.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers, with one
+of them being freed before the other is allocated. 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.

regression/cbmc-primitives/same-object-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is false when given two pointers, with one
+of them being freed before the other is allocated

regression/cbmc-primitives/same-object-04/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(10);
+  char *q = p + 5;
+
+  assert(__CPROVER_same_object(p, q));
+}

regression/cbmc-primitives/same-object-04/test-no-cp.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer to the start of
+a memory block, and a pointer to within the memory block. 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.

regression/cbmc-primitives/same-object-04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that __CPROVER_same_object() is true when given a pointer to the start of
+a memory block, and a pointer to within the memory block.