Add two regression tests for pointer relational support

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c

@@ -0,0 +1,19 @@
+#define NULL (void *)0
+
+int main()
+{
+  int i = 12;
+  int *x = &i;
+  int *y = x + 1;
+  int *z = x - 1;
+
+  // Assertions on y's relation to x
+  __CPROVER_assert(y != x, "y != x: expected successful");
+  __CPROVER_assert(y > x, "y > x: expected successful");
+  __CPROVER_assert(y < x, "y < x: expected failure");
+
+  // Assertions on z's relation to x
+  __CPROVER_assert(z != x, "z != x: expected successful");
+  __CPROVER_assert(z > x, "z > x: expected failure");
+  __CPROVER_assert(z < x, "z < x: expected success");
+}

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.desc

@@ -0,0 +1,15 @@
+CORE
+pointers_stack_lessthan.c
+--trace
+\[main\.assertion\.1] line \d+ y != x: expected successful: SUCCESS
+\[main\.assertion\.2] line \d+ y > x: expected successful: SUCCESS
+\[main\.assertion\.3] line \d+ y < x: expected failure: FAILURE
+\[main\.assertion\.4] line \d+ z != x: expected successful: SUCCESS
+\[main\.assertion\.5] line \d+ z > x: expected failure: FAILURE
+\[main\.assertion\.6] line \d+ z < x: expected success: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing basic pointer relational operator support for three objects
+defined in the function's stack frame.

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *a = malloc(sizeof(int) * 5);
+
+  for(int i = 0; i < 5; i++)
+    *(a + i) = i;
+
+  for(int i = 0; i < 5; i++)
+  {
+    __CPROVER_assert(*(a + i) >= i, "*(a + i) >= i: expected successful");
+    __CPROVER_assert(*(a + i) <= i, "*(a + i) <= i: expected successful");
+    __CPROVER_assert(*(a + i) == i, "*(a + i) <= i: expected successful");
+    __CPROVER_assert(*(a + i) != i, "*(a + i) <= i: expected failure");
+  }
+}

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.desc

@@ -0,0 +1,13 @@
+CORE
+pointers_stack_malloc.c
+--trace
+\[main\.assertion\.1\] line \d+ \*\(a \+ i\) >= i: expected successful: SUCCESS
+\[main\.assertion\.2\] line \d+ \*\(a \+ i\) <= i: expected successful: SUCCESS
+\[main\.assertion\.3\] line \d+ \*\(a \+ i\) <= i: expected successful: SUCCESS
+\[main\.assertion\.4\] line \d+ \*\(a \+ i\) <= i: expected failure: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing the support for relational operators as applied to pointer objects
+backed by a malloc and initialised to some values.