Add regression test using __CPROVER_POINTER_OBJECT directly

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers/pointer_object3.c

@@ -0,0 +1,19 @@
+#define NULL (void *)0
+
+int main()
+{
+  int foo;
+
+  // The identifiers are allocated deterministically, so we want to check the
+  // following properties hold:
+
+  // The pointer object of NULL is always going to be zero.
+  __CPROVER_assert(
+    __CPROVER_POINTER_OBJECT(NULL) != 0,
+    "expected to fail with object ID == 0");
+  // In the case where the program contains a single address of operation,
+  // the pointer object is going to be 1.
+  __CPROVER_assert(
+    __CPROVER_POINTER_OBJECT(&foo) != 1,
+    "expected to fail with object ID == 1");
+}

regression/cbmc-incr-smt2/pointers/pointer_object3.desc

@@ -0,0 +1,13 @@
+CORE
+pointer_object3.c
+
+\[main\.assertion\.1] line \d+ expected to fail with object ID == 0: FAILURE
+\[main\.assertion\.2] line \d+ expected to fail with object ID == 1: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that the assignment of object IDs to objects is deterministic:
+* 0 for the NULL object, and
+* 1 for the single object which is the result of an address of operation