diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index b6e8f0b54628de43c8fe181b61ec43f8e1837c44..a5ba5bf7da343d2590a12be9a56d68c547ecd89e 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -38,6 +38,13 @@ __PUSH_FC_STDLIB
#include "__fc_define_intptr_t.h"
#include "__fc_define_fds.h"
#include "limits.h"
+
+#ifndef __FC_POSIX_VERSION
+#error "unistd.h should only be included with a POSIX machdep"
+#endif
+
+#define _POSIX_VERSION __FC_POSIX_VERSION
+
__BEGIN_DECLS
extern volatile int Frama_C_entropy_source;
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index a48241896c2dfe48f15b7f8fa332b8ea96372879..3b0ea4d4f2b435c4be0c693f914b75b60bfea767 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -107,6 +107,11 @@ little_endian:
type: boolean
+posix_version:
+ description: |
+ value of the macro '_POSIX_VERSION'
+ leave empty for non-POSIX systems
+
ptrdiff_t:
description: definition of 'ptrdiff_t'
@@ -214,3 +219,9 @@ wint_t:
description: definition of 'wint_t'
type: string
+
+wordsize:
+
+ description: value of "__WORDSIZE" macro
+
+ type: string
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index be755d979fb9ee3c1efc3d444c26e36ca5af0ad5..6f2e4bec15efadc003195b32be626e952b338816 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -18,6 +18,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: true
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 4
@@ -36,3 +37,4 @@ version: clang version 15.0.7
wchar_t: int
weof: (0xffffffffu)
wint_t: int
+wordsize: '32'
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index f15c429e025d97de6fdb70e45b899a113ee8009b..007ce9e7d3f756b07184a196220d0a427e5624e6 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -34,3 +34,5 @@ version: none
wchar_t: int
weof: (0xffffffffUL)
wint_t: unsigned long
+wordsize: '16'
+posix_version: '200809L'
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index c2b6c927b7b4dc00b32e42a40dec1435496a5713..ed625f542ebebc90635088f0c61efc979de956cf 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: true
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: long
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '32'
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index be370464cd6bdfc476ba6fe64d791ea46c6dfecd..b3b1c4b03b30fd7688e5f2259cf6e2bc11e95ae6 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: long
little_endian: true
+posix_version: 200809L
ptrdiff_t: long
size_t: unsigned long
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: int
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '64'
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index b530584b9900646ac8d427e4bd2d2fb9354b0ece..c0d9ec1d73af5cf6deb15c1bd953aa7f318ae446 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -34,3 +34,5 @@ version: MSVC - X86-64bits mode
wchar_t: unsigned short
weof: (0xffffU)
wint_t: unsigned short
+wordsize: '64'
+posix_version: ''
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 7f0e1a922d1f076f1dba66842620654de2114b36..4f309f9155cd95048d7bd796cad81f696314b2cd 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -18,6 +18,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: false
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 8
@@ -36,3 +37,4 @@ version: clang version 15.0.7
wchar_t: int
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '32'
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index 0ef5ad977a00c290a405a2148bcd361b4bbe195f..8d417a3b9e11e8a1762318b7fc3179ec5fa81b76 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -34,3 +34,5 @@ version: none
wchar_t: int
weof: (0xffffffffUL)
wint_t: unsigned long
+wordsize: '16'
+posix_version: '200809L'
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index cf02c8f3bfcce6035924a40be41c4f77d8aac7f6..ed6a4c8423e8a8bb6103b3559c5fe574308816e5 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: true
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: long
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '32'
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index 8d9a2386e8f835f029c2238601e8d2aecd1baa38..5e322f71b455002d6341a5b6491a82f52b383aad 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: long
little_endian: true
+posix_version: 200809L
ptrdiff_t: long
size_t: unsigned long
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: int
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '64'
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index e8766ab6ceebd649985b7f309ac9311594c26bbd..b1bbccd739aafe9fd12802d3a9d0638af8c7520d 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -170,6 +170,8 @@ source_files = [
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
("weof.c", "macro"),
+ ("wordsize.c", "macro"),
+ ("posix_version.c", "macro"),
]
@@ -227,7 +229,9 @@ def find_macro_value(name,output):
else:
warnings.warn(f"unexpected symbol '{name}', ignoring")
else:
- warnings.warn(f"cannot find value of field '{name}', skipping")
+ warnings.warn(f"cannot find value of field '{name}', treating as empty")
+ if name in machdep:
+ machdep[name] = ''
if args.verbose:
print(f"compiler output is:{output}")
@@ -244,9 +248,12 @@ for (f, typ) in source_files:
Path(f).with_suffix(".o").unlink(missing_ok=True)
if typ == "macro":
if proc.returncode != 0:
- warnings.warn(f"error in determining value of '{p,stem}', skipping")
+ warnings.warn(f"error in determining value of '{p,stem}', treating as empty")
if args.verbose:
print(f"compiler output is:{proc.stderr.decode()}")
+ name = p.stem
+ if name in machdep:
+ machdep[name] = ''
continue
find_macro_value(p.stem,cleanup_cpp(proc.stdout.decode()))
continue
diff --git a/share/machdeps/make_machdep/posix_version.c b/share/machdeps/make_machdep/posix_version.c
new file mode 100644
index 0000000000000000000000000000000000000000..ded2e9b3de33fedd088a1c663337e47aa2f1d616
--- /dev/null
+++ b/share/machdeps/make_machdep/posix_version.c
@@ -0,0 +1,3 @@
+#include <unistd.h>
+
+long posix_version_is = _POSIX_VERSION;
diff --git a/share/machdeps/make_machdep/wordsize.c b/share/machdeps/make_machdep/wordsize.c
new file mode 100644
index 0000000000000000000000000000000000000000..ff430111be06b6b834f66994a65e9e5da622690e
--- /dev/null
+++ b/share/machdeps/make_machdep/wordsize.c
@@ -0,0 +1,2 @@
+#include <features.h>
+const int wordsize_is = __WORDSIZE;
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 1caae68014cec49b2135dd7ac67a8aedc80c359b..3df712561bddd53536ea9b297fabdabe0be67b3f 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -11,6 +11,10 @@ let gen_define_string fmt macro def =
let gen_define_literal_string fmt macro def =
gen_define fmt macro Format.pp_print_string ("\"" ^ def ^ "\"")
+let gen_define_macro fmt macro def =
+ if def = "" then gen_undef fmt macro
+ else gen_define_string fmt macro def
+
let gen_define_int fmt macro def = gen_define fmt macro Format.pp_print_int def
let gen_byte_order fmt mach =
@@ -201,13 +205,13 @@ let gen_all_defines fmt mach =
gen_intlike_max fmt "__FC_PTRDIFF" mach.ptrdiff_t mach;
gen_intlike_min fmt "__FC_WINT" mach.wint_t mach;
gen_intlike_max fmt "__FC_WINT" mach.wint_t mach;
- gen_define_string fmt "__FC_WEOF" mach.weof;
+ gen_define_macro fmt "__FC_WEOF" mach.weof;
(* NB: Frama-C's inttypes.h is assuming that intptr_t and uintptr_t have the
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);
-
- (* TODO: __FC_POSIX_VERSION *)
+ gen_define_macro fmt "__FC_WORDSIZE" mach.wordsize;
+ gen_define_macro fmt "__FC_POSIX_VERSION" mach.posix_version;
(* TODO: __FC_HOST_NAME_MAX *)
(* TODO: __FC_TTY_NAME_MAX *)
(* TODO: __FC_SIG_ATOMIC_MIN *)
@@ -224,7 +228,6 @@ let gen_all_defines fmt mach =
(* TODO: __FC_TIME_T *)
(* TODO: __FC_NSIG *)
(* TODO: __FC__NSIG *)
- (* TODO: __WORDSIZE *)
(* TODO: gcc builtins *)
Format.fprintf fmt "#endif // __FC_MACHDEP@\n"
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 1b77b2e58561cc57a9363a03a15464530a211785..b9361bc473e758109906106461dcd91bd17d24e8 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1901,7 +1901,9 @@ type mach = {
cpp_arch_flags: string list; (* Architecture-specific flags to be given to
the preprocessor (if supported) *)
version: string; (* Information on this machdep *)
- weof: string; (* expansion of WEOF macro *)
+ weof: string; (* expansion of WEOF macro, empty if undefined *)
+ wordsize: string; (* expansion of __WORDSIZE macro, empty if undefined *)
+ posix_version: string; (* expansion of _POSIX_VERSION macro, empty if undefined *)
}
(*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 8819cba4a61430f8b2497245f1725dd9301c705c..b6efe80bca28f1978596213da545ab9f9831d332 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2663,7 +2663,9 @@ let dummy_machdep =
compiler = "none";
cpp_arch_flags = [];
version = "N/A";
- weof = "(-1)"
+ weof = "(-1)";
+ wordsize = "64";
+ posix_version = "";
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index fc497312b0954cb876499b7b7a298db8dd9d47c6..e00cd79dc58aed4ef1ca40801daf23fc85b694c4 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -37,6 +37,8 @@ let mach =
little_endian = true;
has__builtin_va_list = true;
weof = "(-1)";
+ wordsize = "24";
+ posix_version = "200809L";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 11e6ed0cab15d267049281edbd055056be3bfc7c..7b1dbeb487f94f7613c921948c0634ddb1fc5da0 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -33,3 +33,5 @@ ssize_t: long
version: foo
wchar_t: int
weof: (-1)
+wordsize: '24'
+posix_version: '200809L'
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 51b9b7655e24e412e81e73b8045e4d083b9d514f..c35154121ae9fb3f351b9cb37e3adca0c98a4382 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -35,7 +35,9 @@ let md = {
ptrdiff_t = "int";
wint_t = "long";
has__builtin_va_list = true;
- weof = "(-1L)"
+ weof = "(-1L)";
+ wordsize = "16";
+ posix_version = "";
}
let () =