Field sensitivity for unions

Field-sensitive tracking of unions permits propagating constants even
when those do not affect the full width of the union (implying that some
bits remain non-constant).

Author: tautschnig

regression/cbmc/union18/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+union u_type
+{
+  int i;
+  char ch;
+};
+
+int main()
+{
+  union u_type u;
+
+  u.ch = 2;
+  assert(u.ch == 2);
+}

regression/cbmc/union18/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This should be fully solved by constant propagation when union field-sensitivity
+is in place.