add three tests for unions in structs

These tests pass with the built-in solver but fail with three different
errors when using SMT.

Author: kroening

regression/cbmc/union/union_initialization.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+struct s {
+    union U {
+      char c;
+      char b[2];
+    } u;
+} X;
+
+int main() {
+  // expected to fail
+  __CPROVER_assert(X.u.b[1] == 2, "should fail");
+}

regression/cbmc/union/union_initialization.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+union_initialization.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This fails when using the SMT backend.

regression/cbmc/union/union_member.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+struct s {
+    union U {
+      char b[2];
+    };
+};
+
+int main() {
+  struct s X;
+  __CPROVER_assert(X.b[1] == 2, "should fail");
+}

regression/cbmc/union/union_member.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+union_member.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This fails when using the SMT backend.

regression/cbmc/union/union_update.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+struct s {
+    char a;
+    union U {
+      char c;
+      char b[2];
+    } u;
+} X = { 1, 2 };
+
+int main() {
+  __CPROVER_assert(X.u.b[1] == 123, "should fail");
+}

regression/cbmc/union/union_update.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+union_update.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This fails when using the SMT backend.