From 3cc70b1d1e2ba6011a0490228fb36650dca3a301 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 29 Dec 2020 21:12:46 +0000
Subject: [PATCH] Union regression test of unspecified behaviour

The C standard leaves the values of bytes not belonging to the object
representation of the member last stored unspecified, but GCC, Clang,
and Visual Studio all seem to behave just as CBMC currently does. Ensure
we maintain this behaviour via a regression test.
---
 regression/cbmc/union15/main.c    | 62 +++++++++++++++++++++++++++++++
 regression/cbmc/union15/test.desc |  8 ++++
 2 files changed, 70 insertions(+)
 create mode 100644 regression/cbmc/union15/main.c
 create mode 100644 regression/cbmc/union15/test.desc

diff --git a/regression/cbmc/union15/main.c b/regression/cbmc/union15/main.c
new file mode 100644
index 00000000000..5e3f498bc6d
--- /dev/null
+++ b/regression/cbmc/union15/main.c
@@ -0,0 +1,62 @@
+#include <assert.h>
+
+struct S
+{
+  union U {
+    int x;
+    int y;
+  } u;
+  int z;
+} s = {1, 2};
+
+union B {
+  unsigned char b : 1;
+  unsigned char c;
+};
+
+union C {
+  char c;
+  int i;
+};
+
+union A {
+  struct
+  {
+    char c;
+    char p[3];
+  };
+  int i;
+} x = {1};
+
+int main()
+{
+  // Make sure elements of initializer lists are assigned to the right members
+  // (in particular, `2` is not to be assigned to the second component of the
+  // union, but has to be assigned to the second member of the struct).
+  assert(s.u.x == 1);
+  assert(s.z == 2);
+  assert(x.p[0] == 0);
+
+  // The C standard (6.2.6.1 (7)) states: "When a value is stored in a member of
+  // an object of union type, the bytes of the object representation that do not
+  // correspond to that member but do correspond to other members take
+  // unspecified values." Appendix J.1 Unspecified behavior refers back to this:
+  // "When a value is stored in a member of an object of union type, the bytes
+  // of the object representation that do not correspond to that member but do
+  // correspond to other members take unspecified values."
+  //
+  // GCC, Clang, Visual Studio (and possibly others) choose to maintain the
+  // values of any bits not being assigned to. This includes bit fields, as the
+  // following examples demonstrate.
+  union B ub = {.c = 0xFF};
+  ub.b = 0;
+  assert(ub.c == 0xFE);
+
+  union C uc = {.i = 0xFFFFFFFF};
+  uc.c = 0;
+  assert(uc.i == 0xFFFFFF00);
+
+  union A ua = {.i = 0xFFFFFFFF};
+  ua.c = 0;
+  assert(ua.i == 0xFFFFFF00);
+}
diff --git a/regression/cbmc/union15/test.desc b/regression/cbmc/union15/test.desc
new file mode 100644
index 00000000000..39d9265e8a7
--- /dev/null
+++ b/regression/cbmc/union15/test.desc
@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring