From f7a0c3d36c36cc4d066a3aeea92ef6d91ab04534 Mon Sep 17 00:00:00 2001
From: kroening <kroening@6afb6bc1-c8e4-404c-8f48-9ae832c5b171>
Date: Sat, 3 Nov 2012 15:39:05 +0000
Subject: [PATCH] C++ tests for cbmc

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1881 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
---
 regression/cbmc-cpp/Makefile         | 14 ++++++++++++++
 regression/cbmc-cpp/union2/main.cpp  | 16 ++++++++++++++++
 regression/cbmc-cpp/union2/test.desc |  8 ++++++++
 3 files changed, 38 insertions(+)
 create mode 100644 regression/cbmc-cpp/Makefile
 create mode 100644 regression/cbmc-cpp/union2/main.cpp
 create mode 100644 regression/cbmc-cpp/union2/test.desc

diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
new file mode 100644
index 0000000000..e7e6b2c03e
--- /dev/null
+++ b/regression/cbmc-cpp/Makefile
@@ -0,0 +1,14 @@
+default: tests.log
+
+test:
+	@../test.pl -c cbmc
+
+tests.log: ../test.pl
+	@../test.pl -c cbmc
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
diff --git a/regression/cbmc-cpp/union2/main.cpp b/regression/cbmc-cpp/union2/main.cpp
new file mode 100644
index 0000000000..3981fff6d4
--- /dev/null
+++ b/regression/cbmc-cpp/union2/main.cpp
@@ -0,0 +1,16 @@
+struct A
+{
+  union
+  {
+    int a;
+    char b;
+  };
+};
+
+int main()
+{
+  A obj;
+  obj.a = 'z';
+  assert(obj.b=='z'); // little endian assumption
+  assert(sizeof(A) == sizeof(int));
+}
diff --git a/regression/cbmc-cpp/union2/test.desc b/regression/cbmc-cpp/union2/test.desc
new file mode 100644
index 0000000000..5249662e6a
--- /dev/null
+++ b/regression/cbmc-cpp/union2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+--little-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring