Add tests to check semantics of pointer primitives

Author: danpoe

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

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

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

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Check that the dynamic object property is havoc'd when dynamic objects are
+deallocated

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

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Check that the dynamic object property is havoc'd when dynamic objects are
+deallocated

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

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

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

@@ -0,0 +1,9 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Check that uninitialized pointers are not considered pointing to dynamic objects

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

@@ -0,0 +1,9 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Check that uninitialized pointers are not considered pointing to dynamic objects

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

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

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

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--no-simplify --no-propagation
+^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
+--
+^warning: ignoring
+--
+Check that object size is havoc'd when objects are deallocated

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

@@ -0,0 +1,11 @@
+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
+--
+^warning: ignoring
+--
+Check that object size is havoc'd when objects are deallocated

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

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

regression/cbmc/pointer-offset-01/test-no-cp.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--no-simplify --no-propagation
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+--
+^warning: ignoring
+--
+Check that a negative offset can be chosen for uninitialized pointers

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+--
+^warning: ignoring
+--
+Check that a negative offset can be chosen for uninitialized pointers

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

@@ -0,0 +1,11 @@
+#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))));
+}

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

@@ -0,0 +1,11 @@
+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

regression/cbmc/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/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/same-object-02/test-no-cp.desc

@@ -0,0 +1,11 @@
+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

regression/cbmc/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/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/same-object-03/test-no-cp.desc

@@ -0,0 +1,11 @@
+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

regression/cbmc/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