Add regression tests for the subtraction of two pointer values

Author: NlightNFotis

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

@@ -0,0 +1,15 @@
+#define NULL (void *)0
+
+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");
+}

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

@@ -0,0 +1,12 @@
+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
+^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_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.