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

@@ -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;

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));
+}

regression/cbmc-cpp/union2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+--little-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring