Add two tests (marked KNOWNBUG for now) as documentation for lack of support for byte operations on pointers.

In particular the tests regard `byte_extract_little_endian` and `byte_update_little_endian`
expressions.

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.