From e2ee2d60ab3e44007cee6d2328ef4a6d9acb4acb Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 27 Oct 2022 16:05:25 +0100
Subject: [PATCH] add three tests for unions in structs

These tests pass with the built-in solver but fail with three different
errors when using SMT.
---
 regression/cbmc/union/union_initialization.c    | 16 ++++++++++++++++
 regression/cbmc/union/union_initialization.desc | 13 +++++++++++++
 regression/cbmc/union/union_member.c            | 15 +++++++++++++++
 regression/cbmc/union/union_member.desc         | 13 +++++++++++++
 regression/cbmc/union/union_update.c            | 16 ++++++++++++++++
 regression/cbmc/union/union_update.desc         | 13 +++++++++++++
 6 files changed, 86 insertions(+)
 create mode 100644 regression/cbmc/union/union_initialization.c
 create mode 100644 regression/cbmc/union/union_initialization.desc
 create mode 100644 regression/cbmc/union/union_member.c
 create mode 100644 regression/cbmc/union/union_member.desc
 create mode 100644 regression/cbmc/union/union_update.c
 create mode 100644 regression/cbmc/union/union_update.desc

diff --git a/regression/cbmc/union/union_initialization.c b/regression/cbmc/union/union_initialization.c
new file mode 100644
index 00000000000..e0ea55d1fa2
--- /dev/null
+++ b/regression/cbmc/union/union_initialization.c
@@ -0,0 +1,16 @@
+#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");
+}
diff --git a/regression/cbmc/union/union_initialization.desc b/regression/cbmc/union/union_initialization.desc
new file mode 100644
index 00000000000..68b3c6b2c2f
--- /dev/null
+++ b/regression/cbmc/union/union_initialization.desc
@@ -0,0 +1,13 @@
+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 with Z3 with the error message
+"invalid function/constant definition, sort mismatch".
diff --git a/regression/cbmc/union/union_member.c b/regression/cbmc/union/union_member.c
new file mode 100644
index 00000000000..1989f28c695
--- /dev/null
+++ b/regression/cbmc/union/union_member.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+struct s
+{
+  union U
+  {
+    char b[2];
+  };
+};
+
+int main()
+{
+  struct s X;
+  __CPROVER_assert(X.b[1] == 2, "should fail");
+}
diff --git a/regression/cbmc/union/union_member.desc b/regression/cbmc/union/union_member.desc
new file mode 100644
index 00000000000..a2b273bfe0f
--- /dev/null
+++ b/regression/cbmc/union/union_member.desc
@@ -0,0 +1,13 @@
+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 with Z3 with the error message
+"select requires 1 arguments, but was provided with 2 arguments"
diff --git a/regression/cbmc/union/union_update.c b/regression/cbmc/union/union_update.c
new file mode 100644
index 00000000000..e06161aedb0
--- /dev/null
+++ b/regression/cbmc/union/union_update.c
@@ -0,0 +1,16 @@
+#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");
+}
diff --git a/regression/cbmc/union/union_update.desc b/regression/cbmc/union/union_update.desc
new file mode 100644
index 00000000000..8f8f7b852b0
--- /dev/null
+++ b/regression/cbmc/union/union_update.desc
@@ -0,0 +1,13 @@
+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 with Z3 with the error message
+"store expects the first argument sort to be an array".