Test for union field sensitivity bug

The assignment to s becomes

{-22} main::1::s!0@1#2 = main::1::u!0@1#0..x3[[3]]

The field sensitivity variable on the rhs does not even exist
as it is outside the array bounds of u.x3
(however still pointing to valid memory of the union).
I have seen --pointer-check violations in other situations
for similar reasons.

Author: peterschrammel

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