Merge pull request #6923 from NlightNFotis/pointer_casting_tests

Pointer casting regression tests for new SMT backend

Author: NlightNFotis

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

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint32_t input;
+  uint32_t original = input;
+  uint8_t *ptr = (uint8_t *)(&input);
+  assert(*ptr == 0); // falsifiable
+  *ptr = ~(*ptr);
+  assert(input != original); // valid
+}

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

@@ -0,0 +1,10 @@
+KNOWNBUG
+byte_extract_issue.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_extract_little_endian
+--
+This test is here to document our lack of support for byte_extract_little_endian
+in the pointers support for the new SMT backend.

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

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint32_t x = 0;
+  uint8_t *ptr = (uint8_t *)(&x);
+  int offset;
+  __CPROVER_assume(offset >= 0 && offset < 4);
+  *(ptr + offset) = 1;
+  assert(x != 256);
+}

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

@@ -0,0 +1,10 @@
+KNOWNBUG
+byte_update_issue.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_update_little_endian
+--
+This test is here to document our lack of support for byte_update_little_endian
+in the pointers support for the new SMT backend.

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

@@ -0,0 +1,13 @@
+int main()
+{
+  int *p = (int *)4;
+  __CPROVER_allocated_memory(4, sizeof(int));
+
+  __CPROVER_assert(p == 4, "p == 4: expected success");
+  __CPROVER_assert(p != 0, "p != 0: expected success");
+
+  p = (int *)0x1020304;
+  __CPROVER_assert(p == 0x1020304, "p == 0x1020304: expected success");
+  __CPROVER_assert(p != 0, "p != 0: expected success");
+  __CPROVER_assert(p == 0, "p != 0: expected failure");
+}

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

@@ -0,0 +1,16 @@
+CORE
+pointer_from_int.c
+--trace
+\[main\.assertion\.1\] line \d+ p == 4: expected success: SUCCESS
+\[main\.assertion\.2\] line \d+ p != 0: expected success: SUCCESS
+\[main\.assertion\.3\] line \d+ p == 0x1020304: expected success: SUCCESS
+\[main\.assertion\.4\] line \d+ p != 0: expected success: SUCCESS
+\[main\.assertion\.5\] line \d+ p != 0: expected failure: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is covering basic conversion of pointer values to integers.
+It contains two such conversions, one of an integer in decimal form,
+and one of an integer in a hexadecimal form.

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

@@ -0,0 +1,13 @@
+int f(int x)
+{
+  void *p = (void *)x;
+  int r = (int)p;
+  return r;
+}
+
+int main()
+{
+  int a = f(5);
+  __CPROVER_assert(a == 5, "a == 5: expected success");
+  __CPROVER_assert(a != 5, "a != 5: expected failure");
+}

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

@@ -0,0 +1,11 @@
+CORE
+pointer_round_trip.c
+--trace
+\[main\.assertion\.1\] line \d+ a == 5: expected success: SUCCESS
+\[main\.assertion\.2\] line \d+ a != 5: expected failure: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is testing an integer value round trip (int -> pointer -> int) test.

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.