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