From 14dde0a20c52d7bb35bbdab2bd017be9cdd75522 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 20 Jan 2023 16:08:21 +0100 Subject: Use define for wchar_t type Since the wchar_t type depends on the architecture and the system we are compiling for we replace the typedef to a fixed type by a typedef to a define which is predefined by the compiler itself. --- driver/Frontend.ml | 9 +++++++++ runtime/include/stddef.h | 8 ++------ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/driver/Frontend.ml b/driver/Frontend.ml index c8131662..0e2c392f 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -51,6 +51,14 @@ let predefined_macros = (* From C to preprocessed C *) +(* We define the type wchar_t since it is dependent on the system and + we want to avoid more ifdefs in the stddef header file. *) +let abi_macros () = + let wchar_typ = Cprint.name_of_ikind (Cutil.wchar_ikind()) in + [ + sprintf "-D__COMPCERT_WCHAR_TYPE__=%s" wchar_typ + ] + let preprocess ifile ofile = Diagnostics.raise_on_errors (); let output = @@ -61,6 +69,7 @@ let preprocess ifile ofile = then ["-std=" ^ !option_std] else []); predefined_macros; + abi_macros (); (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] else []); diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 5a66215a..5a84f8bb 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -86,7 +86,7 @@ typedef signed long ptrdiff_t; #ifdef _TYPE_wchar_t _TYPE_wchar_t; #else -typedef unsigned short wchar_t; +typedef __COMPCERT_WCHAR_TYPE__ wchar_t; #endif #endif #undef __need_wchar_t @@ -95,11 +95,7 @@ typedef unsigned short wchar_t; #if defined(_STDDEF_H) || defined(__need_wchar_t) #ifndef _WCHAR_T #define _WCHAR_T -#ifdef _WIN32 -typedef unsigned short wchar_t; -#else -typedef signed int wchar_t; -#endif +typedef __COMPCERT_WCHAR_TYPE__ wchar_t; #endif #undef __need_wchar_t #endif -- cgit