Add regression tests for plus_exprt conversion

Author: NlightNFotis

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

@@ -0,0 +1,13 @@
+#include <stdint.h>
+
+#define NULL (void *)0
+
+int main()
+{
+  int32_t *a;
+  __CPROVER_assume(a != NULL);
+  int32_t *z = a + 2 * sizeof(int32_t);
+
+  __CPROVER_assert(a != z, "expected successful because of pointer arithmetic");
+  __CPROVER_assert(a == z, "expected failure because of pointer arithmetic");
+}

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

@@ -0,0 +1,13 @@
+CORE
+addition_compound_expr.c
+--trace
+\[main\.assertion\.1\] line \d+ expected successful because of pointer arithmetic: SUCCESS
+\[main\.assertion\.2\] line \d+ expected failure because of pointer arithmetic: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing the same thing as the test in addition_simple.desc, with the
+difference being that the addition expression here is compound, containing a
+more elaborate operand in the form of a multiplication containing a sizeof
+operator.

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

@@ -0,0 +1,12 @@
+#define NULL (void *)0
+
+int main()
+{
+  int *x;
+  int *y = x + 1;
+  __CPROVER_assume(x != NULL);
+  __CPROVER_assume(y != NULL);
+
+  __CPROVER_assert(y == x, "expected false after pointer manipulation");
+  __CPROVER_assert(y != x, "expected true");
+}

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

@@ -0,0 +1,12 @@
+CORE
+addition_simple.c
+--trace
+\[main\.assertion\.1\] line \d+ expected false after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected true: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing basic pointer arithmetic by adding by incrementing a pointer's
+address and assigning that value to another pointer, then asserting that they
+don't point to the same thing.