aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2023-01-20 16:08:21 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2023-02-01 15:09:02 +0100
commit14dde0a20c52d7bb35bbdab2bd017be9cdd75522 (patch)
treea7a10438f1f4ef4496ede86a8c5f2824afff5c77
parentc678903054da11c0b34d9ceb35664d264f840361 (diff)
downloadcompcert-14dde0a20c52d7bb35bbdab2bd017be9cdd75522.tar.gz
compcert-14dde0a20c52d7bb35bbdab2bd017be9cdd75522.zip
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.
-rw-r--r--driver/Frontend.ml9
-rw-r--r--runtime/include/stddef.h8
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