Add regression for non-symbol lhs SMT2 trace node

Author: Enrico Steffinlongo

…ointers-conversions/byte_extract_issue.c …smt2/pointers-conversions/byte_extract.cregression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c renamed to regression/cbmc-incr-smt2/pointers-conversions/byte_extract.c regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c renamed to regression/cbmc-incr-smt2/pointers-conversions/byte_extract.c

@@ -6,7 +6,7 @@ int main()
   uint32_t input;
   uint32_t original = input;
   uint8_t *ptr = (uint8_t *)(&input);
-  assert(*ptr == 0); // falsifiable
+  assert(*ptr != 42); // falsifiable
   *ptr = ~(*ptr);
   assert(input != original); // valid
 }

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

@@ -0,0 +1,19 @@
+CORE
+byte_extract.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion \*ptr != 42: FAILURE
+\[main\.assertion\.\d+\] line \d+ assertion input != original: SUCCESS
+  input=42ul? \(00000000 00000000 00000000 00101010\)
+  original=42ul? \(00000000 00000000 00000000 00101010\)
+Violated property:
+  file byte_extract.c function main line \d+ thread \d+
+  assertion \*ptr != 42
+^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_extract_issue.desc

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

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

@@ -0,0 +1,23 @@
+CORE
+byte_update.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion x != 256u: FAILURE
+State \d+ file byte_update\.c function main line \d+ thread \d
+  offset=1ul? \(00000000 00000000 00000000 00000001\)
+Assumption:
+  file byte_update\.c line \d+ function main
+  offset >= 0u && offset < 4u
+State \d+ file byte_update\.c function main line \d+ thread \d+
+  byte_extract_little_endian\(x, \(signed long( long)? int\)offset, uint8_t\)=1 \(00000001\)
+Violated property:
+  file byte_update.c function main line \d+ thread \d+
+  assertion x != 256u
+^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.