Merge pull request #7388 from peterschrammel/union-field-sensitivity-bug

Test for union field sensitivity bug

Author: kroening

regression/cbmc/union-unequal-element-size1/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+union UNIONNAME
+{
+  int x1;
+  char x3[3];
+};
+
+int main()
+{
+  union UNIONNAME u;
+  u.x1 = 0x01010101;
+
+  assert(u.x3[0]);
+  assert(u.x3[1]);
+  assert(u.x3[2]);
+
+  assert(*((char *)&u.x1));
+  assert(*(((char *)&u.x1) + 1));
+  assert(*(((char *)&u.x1) + 2));
+  char s = *(((char *)&u.x1) + 3);
+  assert(s);
+  return 0;
+}

regression/cbmc/union-unequal-element-size1/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+assert(s) fails with field sensitivity, but passes without