From e36c92b46237e1fc33f41db58f59d510aa5c2b42 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 3 Sep 2024 17:34:10 +0200
Subject: [PATCH] [tests] add test for #pragma pack with gcc
---
tests/misc/dune | 6 ++++++
tests/misc/pragma-pack-gcc.t | 11 +++++++++++
2 files changed, 17 insertions(+)
create mode 100644 tests/misc/pragma-pack-gcc.t
diff --git a/tests/misc/dune b/tests/misc/dune
index 93eae8d410..1ac66020df 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 0000000000..c68a6edf7e
--- /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
--
GitLab