Add regression test for __CPROVER_POINTER_OFFSET

Author: NlightNFotis

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

@@ -0,0 +1,16 @@
+int main()
+{
+  int a;
+  int *p = &a;
+  int *q = &a;
+
+  __CPROVER_assert(
+    __CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q),
+    "expected failure because offsets should be the same");
+
+  // TODO: Remove comments once pointer arithmetic works:
+
+  // *q = p + 2;
+
+  // __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q), "expected failure");
+}

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

@@ -0,0 +1,16 @@
+CORE
+pointer_offset.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure because offsets should be the same: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that the pointer offset bits of two pointers pointing to
+the same object are equal.
+
+The test also contains a fragment of the test which doesn't work
+for now, but would be good to be added as soon as we get pointer
+arithmetic to work, so we can make sure that pointer offset fails
+appropriately.