Additional very basic regression tests for byte_update

All other tests appear to be using arrays, these new ones don't.

regression/cbmc/byte_update8/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x=0x01020304;
+  short *p=((short*)&x)+1;
+  *p=0xABCD;
+  assert(x==0xABCD0304);
+  p=(short*)(((char*)&x)+1);
+  *p=0xABCD;
+  assert(x==0xABABCD04);
+}

regression/cbmc/byte_update8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/byte_update9/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x=0x01020304;
+  short *p=((short*)&x)+1;
+  *p=0xABCD;
+  assert(x==0x0102ABCD);
+  p=(short*)(((char*)&x)+1);
+  *p=0xABCD;
+  assert(x==0x01ABCDCD);
+}

regression/cbmc/byte_update9/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--big-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring