Add regression tests for the subtraction of two pointer values

Author: NlightNFotis

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

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+int main()
+{
+  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

@@ -0,0 +1,13 @@
+CORE
+pointer_subtraction.c
+--trace
+\[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$
+--
+--
+This test is testing that the subtraction between two pointers (giving us the
+increment between the two pointers) works as it should.

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|127)$
+^SIGNAL=0$
+--
+--
+This test is for making sure that we only subtract pointers with the
+same underlying (base) type.

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

@@ -0,0 +1,15 @@
+#define NULL (void *)0
+
+int main()
+{
+  int *x;
+  unsigned int z;
+  __CPROVER_assume(z < 3);
+  __CPROVER_assume(z > 1);
+  int *y = x - z;
+  __CPROVER_assume(x != NULL);
+  __CPROVER_assume(y != NULL);
+
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(y != x, "expected success after pointer manipulation");
+}

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

@@ -0,0 +1,11 @@
+CORE
+pointer_subtraction_unsigned.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected success after pointer manipulation: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The test is similar to the one in `pointer_subtraction.desc`, but with different
+types in the subtraction operands.