Add test for __CPROVER_same_object() with pointer pointing within memory block

Author: danpoe

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