Add a test based on the conversion of casting of pointer values

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.c

@@ -0,0 +1,19 @@
+int cmp(const void *p1, const void *p2)
+{
+  int x = *(int *)p1;
+  int y = *(int *)p2;
+
+  return (x < y) ? -1 : ((x == y) ? 0 : 1);
+}
+
+int main()
+{
+  int a = 5;
+  int b = 6;
+  int c = 7;
+
+  __CPROVER_assert(cmp(&a, &b) == -1, "expected result == -1: success");
+  __CPROVER_assert(cmp(&c, &b) == 1, "expected result == 1: success");
+  __CPROVER_assert(cmp(&c, &c) == 0, "expected result == 0: success");
+  __CPROVER_assert(cmp(&c, &c) == 1, "expected result == 1: failure");
+}

regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc

@@ -0,0 +1,16 @@
+CORE
+pointer_to_int.c
+--trace
+\[main\.assertion\.1\] line \d+ expected result == -1: success: SUCCESS
+\[main\.assertion\.2\] line \d+ expected result == 1: success: SUCCESS
+\[main\.assertion\.3\] line \d+ expected result == 0: success: SUCCESS
+\[main\.assertion\.4\] line \d+ expected result == 1: failure: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is covering basic conversion of casting of different pointer values,
+which are then dereferenced and used in the function. We are asserting against
+the result of the function, which cannot be right, unless the conversions
+work as they should.