Tighten regression tests for pointer subtraction.

This is to make sure that we get reasonable results from a pointer subtraction
operation, and that the invariants between the different base types are observed.

Author: NlightNFotis

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.c

@@ -1,15 +1,10 @@
-#define NULL (void *)0
-
+#include <stdlib.h>
 int main()
 {
-  int *x;
-  int *y;
-  int *z = x - y;
-  __CPROVER_assume(x != NULL);
-  __CPROVER_assume(y != NULL);
-  __CPROVER_assume(x != y);
-
-  __CPROVER_assert(z == x, "expected failure after pointer manipulation");
-  __CPROVER_assert(z == y, "expected failure after pointer manipulation");
-  __CPROVER_assert(y != x, "expected succesful after pointer manipulation");
+  int *x = malloc(sizeof(int));
+  int *y = x + 3;
+  int z = y - x;
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(z == 3, "expected successful after pointer manipulation");
+  __CPROVER_assert(z != 3, "expected failure after pointer manipulation");
 }

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc

@@ -1,9 +1,10 @@
 CORE
 pointer_subtraction.c
 --trace
-\[main\.assertion\.1] line \d+ expected failure after pointer manipulation: FAILURE
-\[main\.assertion\.2] line \d+ expected failure after pointer manipulation: FAILURE
-\[main\.assertion\.3] line \d+ expected succesful after pointer manipulation: SUCCESS
+\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS
+\[main\.assertion\.3\] line \d+ expected failure after pointer manipulation: FAILURE
+z=3
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+int main()
+{
+  int *x = malloc(sizeof(int));
+  float *y = x + 3;
+  int z = y - x;
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(z == 3, "expected successful after pointer manipulation");
+  __CPROVER_assert(z != 3, "expected failure after pointer manipulation");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc

@@ -0,0 +1,10 @@
+CORE
+pointer_subtraction_diff_types.c
+--trace
+^Reason: only pointers of the same object type can be subtracted.
+^EXIT=134$
+^SIGNAL=0$
+--
+--
+This test is for making sure that we only subtract pointers with the
+same underlying (base) type.