Merge pull request #397 from smowton/fix_byte_update

Fix byte update flattening

Author: Daniel Kroening

regression/cbmc/byte_update1/main.c

@@ -0,0 +1,24 @@
+#include <stdio.h>
+#include <assert.h>
+
+struct A {
+  int x;
+};
+
+int main(int argc, char** argv) {
+
+  struct A a;
+  int i;
+  struct A* a_addr=&a;
+
+  if(argc != 2)
+    return;
+
+  void** ptrs[argc];
+  for(i = 0; i < 2; ++i)
+    ptrs[i] = (void*)0;
+
+  ((struct A**)ptrs)[1]=&a;
+  assert(ptrs[1] == (void*)&a);
+
+}

regression/cbmc/byte_update1/test.desc

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

regression/cbmc/byte_update2/main.c

@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 2)
+    return 0;
+
+  unsigned long x[argc];
+  x[0]=0x0102030405060708;
+  x[1]=0x1112131415161718;
+
+  unsigned char* alias=(unsigned short*)(((char*)x)+5);
+  *alias=0xed;
+
+  unsigned char* alias2=(unsigned char*)x;
+  /*
+  for(int i = 0; i < 16; ++i)
+    printf("%02hhx\n",alias2[i]);
+  */
+
+  assert(alias2[0]==0x08);
+  assert(alias2[1]==0x07);
+  assert(alias2[2]==0x06);
+  assert(alias2[3]==0x05);
+  assert(alias2[4]==0x04);
+  assert(alias2[5]==0xed);
+  assert(alias2[6]==0x02);
+  assert(alias2[7]==0x01);
+  assert(alias2[8]==0x18);
+  assert(alias2[9]==0x17);
+  assert(alias2[10]==0x16);
+  assert(alias2[11]==0x15);
+  assert(alias2[12]==0x14);
+  assert(alias2[13]==0x13);
+  assert(alias2[14]==0x12);
+  assert(alias2[15]==0x11);
+
+}

regression/cbmc/byte_update2/test.desc

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

regression/cbmc/byte_update3/main.c

@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 5)
+    return 0;
+
+  short x[argc];
+  x[0]=0x0102;
+  x[1]=0x0304;
+  x[2]=0x0506;
+  x[3]=0x0708;
+  x[4]=0x090a;
+
+  unsigned long* alias=(unsigned long*)(((char*)x)+0);
+  *alias=0xf1f2f3f4f5f6f7f8;
+
+  unsigned char* alias2=(unsigned char*)x;
+  assert(alias2[0]==0xf8);
+  assert(alias2[1]==0xf7);
+  assert(alias2[2]==0xf6);
+  assert(alias2[3]==0xf5);
+  assert(alias2[4]==0xf4);
+  assert(alias2[5]==0xf3);
+  assert(alias2[6]==0xf2);
+  assert(alias2[7]==0xf1);
+  assert(alias2[8]==0x0a);
+  assert(alias2[9]==0x09);
+
+}

regression/cbmc/byte_update3/test.desc

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

regression/cbmc/byte_update4/main.c

@@ -0,0 +1,36 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 10)
+    return 0;
+
+  unsigned char x[argc];
+  x[0]=0x01;
+  x[1]=0x02;
+  x[2]=0x03;
+  x[3]=0x04;
+  x[4]=0x05;
+  x[5]=0x06;
+  x[6]=0x07;
+  x[7]=0x08;
+  x[8]=0x09;
+  x[9]=0x0a;
+
+  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  *alias=0xf1f2f3f4f5f6f7f8;
+
+  unsigned char* alias2=(unsigned char*)x;
+  assert(alias2[0]==0x01);
+  assert(alias2[1]==0xf8);
+  assert(alias2[2]==0xf7);
+  assert(alias2[3]==0xf6);
+  assert(alias2[4]==0xf5);
+  assert(alias2[5]==0xf4);
+  assert(alias2[6]==0xf3);
+  assert(alias2[7]==0xf2);
+  assert(alias2[8]==0xf1);
+  assert(alias2[9]==0x0a);
+
+}

regression/cbmc/byte_update4/test.desc

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

regression/cbmc/byte_update5/main.c

@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 5)
+    return 0;
+
+  short x[argc];
+  x[0]=0x0102;
+  x[1]=0x0304;
+  x[2]=0x0506;
+  x[3]=0x0708;
+  x[4]=0x090a;
+
+  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  *alias=0xf1f2f3f4f5f6f7f8;
+
+  unsigned char* alias2=(unsigned char*)x;
+  assert(alias2[0]==0x02);
+  assert(alias2[1]==0xf8);
+  assert(alias2[2]==0xf7);
+  assert(alias2[3]==0xf6);
+  assert(alias2[4]==0xf5);
+  assert(alias2[5]==0xf4);
+  assert(alias2[6]==0xf3);
+  assert(alias2[7]==0xf2);
+  assert(alias2[8]==0xf1);
+  assert(alias2[9]==0x09);
+
+}

regression/cbmc/byte_update5/test.desc

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

regression/cbmc/byte_update6/main.c

@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 2)
+    return 0;
+
+  unsigned long x[argc];
+  x[0]=0x0102030405060708;
+  x[1]=0x1112131415161718;
+
+  unsigned short* alias=(unsigned short*)(((char*)x)+8);
+  *alias=0xedcb;
+
+  unsigned char* alias2=(unsigned char*)x;
+  /*
+  for(int i = 0; i < 16; ++i)
+    printf("%02hhx\n",alias2[i]);
+  */
+
+  assert(alias2[0]==0x08);
+  assert(alias2[1]==0x07);
+  assert(alias2[2]==0x06);
+  assert(alias2[3]==0x05);
+  assert(alias2[4]==0x04);
+  assert(alias2[5]==0x03);
+  assert(alias2[6]==0x02);
+  assert(alias2[7]==0x01);
+  assert(alias2[8]==0xcb);
+  assert(alias2[9]==0xed);
+  assert(alias2[10]==0x16);
+  assert(alias2[11]==0x15);
+  assert(alias2[12]==0x14);
+  assert(alias2[13]==0x13);
+  assert(alias2[14]==0x12);
+  assert(alias2[15]==0x11);
+
+}

regression/cbmc/byte_update6/test.desc

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

regression/cbmc/byte_update7/main.c

@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 2)
+    return 0;
+
+  unsigned long x[argc];
+  x[0]=0x0102030405060708;
+  x[1]=0x1112131415161718;
+
+  unsigned short* alias=(unsigned short*)(((char*)x)+7);
+  *alias=0xedcb;
+
+  unsigned char* alias2=(unsigned char*)x;
+  /*
+  for(int i = 0; i < 16; ++i)
+    printf("%02hhx\n",alias2[i]);
+  */
+
+  assert(alias2[0]==0x08);
+  assert(alias2[1]==0x07);
+  assert(alias2[2]==0x06);
+  assert(alias2[3]==0x05);
+  assert(alias2[4]==0x04);
+  assert(alias2[5]==0x03);
+  assert(alias2[6]==0x02);
+  assert(alias2[7]==0xcb);
+  assert(alias2[8]==0xed);
+  assert(alias2[9]==0x17);
+  assert(alias2[10]==0x16);
+  assert(alias2[11]==0x15);
+  assert(alias2[12]==0x14);
+  assert(alias2[13]==0x13);
+  assert(alias2[14]==0x12);
+  assert(alias2[15]==0x11);
+
+}

regression/cbmc/byte_update7/test.desc

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