Add regression tests for byte extraction/update

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x[3];
+  x[0] = 0;
+  x[1] = 0;
+  x[2] = 0;
+  uint8_t *c = x;
+  c[1] = 1;
+  assert(x[0] == 256);
+  assert(x[0] == 0);
+  assert(x[1] == 0);
+  assert(x[2] == 0);
+  uint16_t between = c[1];
+  assert(between == 1);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc

@@ -0,0 +1,12 @@
+CORE
+array-misalign-between.c
+--slice-formula
+\[main\.assertion\.1\] line \d+ assertion x\[0\] == 256: SUCCESS
+\[main\.assertion\.2\] line \d+ assertion x\[0\] == 0: FAILURE
+\[main\.assertion\.3\] line \d+ assertion x\[1\] == 0: SUCCESS
+\[main\.assertion\.4\] line \d+ assertion x\[2\] == 0: SUCCESS
+\[main\.assertion\.5\] line \d+ assertion between == 1: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x[3];
+  x[0] = 0;
+  x[1] = 0;
+  x[2] = 0;
+  uint8_t *c = x;
+  c[1] = 1;
+  assert(x[0] == 256ul);
+  assert(x[0] == 0ul);
+  assert(x[1] == 0ul);
+  assert(x[2] == 0ul);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc

@@ -0,0 +1,11 @@
+CORE
+array-misalign.c
+--slice-formula
+\[main.assertion\.1\] line \d+ assertion x\[0\] == 256ul: SUCCESS
+\[main.assertion\.2\] line \d+ assertion x\[0\] == 0ul: FAILURE
+\[main.assertion\.3\] line \d+ assertion x\[1\] == 0ul: SUCCESS
+\[main.assertion\.4\] line \d+ assertion x\[2\] == 0ul: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint8_t x[2];
+  x[0] = 1u;
+  x[1] = 1u;
+  uint16_t *y = x;
+  uint16_t z = *y;
+  assert(z == 257);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc

@@ -0,0 +1,8 @@
+CORE
+byte-extract-small.c
+--slice-formula
+\[main.assertion\.1\] line \d+ assertion z == 257: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x;
+  uint8_t *y = &x;
+  assert(y[0] == 0);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc

@@ -0,0 +1,8 @@
+CORE
+byte-extract.c
+--slice-formula
+\[main.assertion\.1\] line \d+ assertion y\[0\] == 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint8_t x[2];
+  x[0] = 0;
+  x[1] = 0;
+  uint16_t *y = x;
+  *y = 258;
+  assert(x[0] == 2);
+  assert(x[1] == 1);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc

@@ -0,0 +1,9 @@
+CORE
+byte-update-small.c
+--slice-formula
+\[main\.assertion\.1\] line \d+ assertion x\[0\] == 2: SUCCESS
+\[main\.assertion\.2\] line \d+ assertion x\[1\] == 1: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x = 0;
+  uint8_t *y = &x;
+  y[1] = 1;
+  assert(x == 256);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc

@@ -0,0 +1,8 @@
+CORE
+byte-update.c
+--slice-formula
+\[main\.assertion\.1\] line \d+ assertion x == 256: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--