From 2e49f1a7b5e900f802e8363e859c5a661b440aec Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 9 May 2023 18:34:52 +0200
Subject: [PATCH] [machdep] provide definition for __WORDSIZE in __fc_machdep.h

---
 src/kernel_internals/runtime/machdep.ml   | 2 +-
 tests/libc/fc_builtin_c.c                 | 7 +++++++
 tests/libc/oracle/fc_builtin_c.res.oracle | 2 ++
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index f7742080fd4..b1dcd202c82 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -264,7 +264,7 @@ let gen_all_defines fmt mach =
      same rank when it comes to define PRI.?PTR macros. *)
   gen_define_literal_string fmt "__PRIPTR_PREFIX"
     (List.assoc (no_signedness mach.intptr_t) pp_of_kind);
-  gen_define_macro fmt "__FC_WORDSIZE" mach.wordsize;
+  gen_define_macro fmt "__WORDSIZE" mach.wordsize;
   gen_define_macro fmt "__FC_POSIX_VERSION" mach.posix_version;
   gen_define_string fmt "__FC_SIG_ATOMIC_T" mach.sig_atomic_t;
   gen_intlike_min fmt "__FC_SIG_ATOMIC_MIN" mach.sig_atomic_t mach;
diff --git a/tests/libc/fc_builtin_c.c b/tests/libc/fc_builtin_c.c
index ea336b1e04e..abd1f7ce3de 100644
--- a/tests/libc/fc_builtin_c.c
+++ b/tests/libc/fc_builtin_c.c
@@ -34,4 +34,11 @@ int main() {
     Frama_C_unsigned_long_interval(LONG_MAX - 1UL, LONG_MAX + 1UL);
   //@ assert bounds: LONG_MAX - 1 <= ul <= LONG_MAX + 1;
   //@ assert sampling:unknown: ul == LONG_MAX;
+
+#ifdef __WORDSIZE
+  int w = __WORDSIZE;
+#else
+  int w = -1;
+#endif
+  //@ assert __WORDSIZE_is_defined: w > 0;
 }
diff --git a/tests/libc/oracle/fc_builtin_c.res.oracle b/tests/libc/oracle/fc_builtin_c.res.oracle
index d922ab4e1ef..6ca7e87a24c 100644
--- a/tests/libc/oracle/fc_builtin_c.res.oracle
+++ b/tests/libc/oracle/fc_builtin_c.res.oracle
@@ -73,6 +73,7 @@
 [eva] fc_builtin_c.c:35: assertion 'bounds' got status valid.
 [eva:alarm] fc_builtin_c.c:36: Warning: 
   assertion 'sampling,unknown' got status unknown.
+[eva] fc_builtin_c.c:43: assertion '__WORDSIZE_is_defined' got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -111,4 +112,5 @@
   d ∈ [12345678901.2 .. 12345678901.2]
   l ∈ {-3}
   ul ∈ {2147483647}
+  w ∈ {32}
   __retres ∈ {0}
-- 
GitLab