diff --git a/tests/misc/dune b/tests/misc/dune index 93eae8d4100a7dca3874f32ae2879a7bee91c003..1ac66020dfef15db60a3f578e47e78b01f746433 100644 --- a/tests/misc/dune +++ b/tests/misc/dune @@ -2,3 +2,9 @@ (applies_to user_directories.unix.t) (enabled_if (and (= %{os_type} unix) (<> %{system} macos))) ) + +(cram + (applies_to pragma-pack-gcc) + (enabled_if %{bin-available:gcc}) + (deps pragma-pack.c pragma-pack-utils.h) +) diff --git a/tests/misc/pragma-pack-gcc.t b/tests/misc/pragma-pack-gcc.t new file mode 100644 index 0000000000000000000000000000000000000000..c68a6edf7ef6087b89bbeacd1f68f5382d3fb6d9 --- /dev/null +++ b/tests/misc/pragma-pack-gcc.t @@ -0,0 +1,11 @@ +Testing that the output produced by Eva and the execution of the binary +compiled by GCC are identical, both on a 32-bit machdep and on a 64-bit one + +# Note: we cannot currently test this in Nix due to issues with multiStdenv +# $ frama-c pragma-pack.c -machdep gcc_x86_32 -eva -eva-msg-key=-summary | grep -A999 "eva:final-states" | grep -v "\[eva:final-states\]" | grep -v __retres > eva.res +# $ gcc -m32 pragma-pack.c -Wno-pragmas && ./a.out > gcc.res +# $ diff -B eva.res gcc.res # should be identical + + $ frama-c pragma-pack.c -machdep gcc_x86_64 -eva -eva-msg-key=-summary | grep -A999 "eva:final-states" | grep -v "\[eva:final-states\]" | grep -v __retres > eva.res + $ gcc pragma-pack.c -Wno-pragmas && ./a.out > gcc.res + $ diff -B eva.res gcc.res # should be identical