diff --git a/share/libc/__fc_define_sigset_t.h b/share/libc/__fc_define_sigset_t.h
index b5718423a3cebd450cc8c989b7b60b679697e789..30f99f6f804ea9d320d2aa3e1378608b79fa35c9 100644
--- a/share/libc/__fc_define_sigset_t.h
+++ b/share/libc/__fc_define_sigset_t.h
@@ -32,4 +32,3 @@ typedef unsigned long sigset_t;
__END_DECLS
__POP_FC_STDLIB
#endif
-
diff --git a/share/libc/signal.h b/share/libc/signal.h
index be91ea934aea93f3d1079594e817409cc5ce8aee..30851947103312e43d4a0adf40dfc50484c68c82 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -102,9 +102,16 @@ extern void __fc_sig_err(int);
#define SIGRTMIN 32
#define SIGRTMAX 64
+/* Non-standard macros (depending on the OS, the name has an underscore or not)
+ supposed to be the number of distinct signals that may be raised.
+ Upcoming POSIX standard seems to allow for a NSIG_MAX macro in limits.h that
+ would have roughly the same usage as NSIG (NSIG_MAX would be the maximal value
+ that a signal can have, i.e. NSIG-1 if we start at 0 and don't leave holes. If
+ this ever becomes supported, we might use this macro instead
+*/
+#ifdef __FC_NSIG
#define NSIG __FC_NSIG
-#ifdef __FC__NSIG
-#define _NSIG __FC__NSIG
+#define _NSIG __FC_NSIG
#endif
#define SA_NOCLDSTOP 0x00000001
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index 795492d92dbea6930c734a7b5cf0da3a43d418e8..82beb3530ac7c4553ba260952756d753d6fd7894 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -143,6 +143,12 @@ mb_cur_max:
type: string
+nsig:
+
+ description: number of possible signals (non standard macro, empty if undefined)
+
+ type: string
+
posix_version:
description: |
value of the macro '_POSIX_VERSION'
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index f4c03215a7dbcff781ff9330a8c8c2a4c8034a3a..76ce8188aeee8ccce1acd1ed5a85f16658272653 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -24,6 +24,7 @@ intptr_t: int
l_tmpnam: '20'
little_endian: true
mb_cur_max: ((size_t)16)
+nsig: (64 + 1)
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index e8b8136039b06c238217bb30a59e2f1c21af276b..7d36c6f2c2436a07e7df70b70938195d33d855a0 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: long
little_endian: true
+nsig: 65
ptrdiff_t: int
sig_atomic_t: int
size_t: unsigned int
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index bfe54a7b612238e305aa75a893341048a868223e..5992ccb712121282be7acb3626c9c8b4664ca241 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -22,6 +22,7 @@ intptr_t: int
l_tmpnam: '20'
little_endian: true
mb_cur_max: ((size_t) 16 )
+nsig: (64 + 1)
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index 2406b67761cf64c11b82d7b5450ae5c50cb24fe1..2092ac09fb19e6901dce740ada25f0a729c35003 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -22,6 +22,7 @@ intptr_t: long
l_tmpnam: '20'
little_endian: true
mb_cur_max: ((size_t) 16 )
+nsig: (64 + 1)
posix_version: 200809L
ptrdiff_t: long
rand_max: '2147483647'
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index 95d157a05b155530248c9ef864ebcfe3a679d7ea..a71a5365fa01d3fee8aa68502be35ec050cdbe18 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: false
intptr_t: signed long long
little_endian: true
+nsig: 23
ptrdiff_t: long long
# NB: wasn't defined at all in old __fc_machdep.h
sig_atomic_t: int
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index a3ad08e801edfa9efc8a2ed4466e1fef0efc751e..fda90435289e8d7bb838481c032f7afa5c5cfb12 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -24,6 +24,7 @@ intptr_t: int
l_tmpnam: '20'
little_endian: false
mb_cur_max: ((size_t)16)
+nsig: (64 + 1)
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index d0128407f6e554c78adea8a93c841b9535dcd666..aa873f36dd60688ac2c2e1edaa2b9e5308407e09 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: long
little_endian: true
+nsig: 65
ptrdiff_t: int
sig_atomic_t: int
size_t: unsigned int
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index af0bed28d860c3280f65545278dbd1454e29cb38..41c794f237174ffdfec6f22193089f934d3a85c2 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -22,6 +22,7 @@ intptr_t: int
l_tmpnam: '20'
little_endian: true
mb_cur_max: ((size_t) 16 )
+nsig: (64 + 1)
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index e77034fed4ac5ee3b01b69bfb34622fc5a50c0a5..96d69bf96f1fabb5e11b30b9cee87087c3de3ed0 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -22,6 +22,7 @@ intptr_t: long
l_tmpnam: '20'
little_endian: true
mb_cur_max: ((size_t) 16 )
+nsig: (64 + 1)
posix_version: 200809L
ptrdiff_t: long
rand_max: '2147483647'
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index 0978cbe183847a99044dd63415c41d9a8a8b48e1..55c62051b6e52745e0f5f67688e48f0814eee057 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -182,6 +182,7 @@ source_files = [
("posix_version.c", "macro"),
("stdio_macros.c", "macro"),
("stdlib_macros.c", "macro"),
+ ("nsig.c", "macro"),
]
diff --git a/share/machdeps/make_machdep/nsig.c b/share/machdeps/make_machdep/nsig.c
new file mode 100644
index 0000000000000000000000000000000000000000..5fa6451f020dc696755688ae93edadd105f453ab
--- /dev/null
+++ b/share/machdeps/make_machdep/nsig.c
@@ -0,0 +1,29 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include <signal.h>
+
+#if defined(NSIG)
+int nsig_is = NSIG;
+#elif defined(_NSIG);
+int nsig_is = _NSIG;
+#endif
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index c216353b5c7e2dd81b407042bd2a1257cf36c48a..c67516d799a069fffcf94cf5136201c7f8748792 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -247,8 +247,7 @@ let gen_all_defines fmt mach =
gen_define_macro fmt "__FC_MB_CUR_MAX" mach.mb_cur_max;
(* TODO: __FC_E*, errno enumeration *)
gen_define_macro fmt "__FC_TIME_T" mach.time_t;
- (* TODO: __FC_NSIG *)
- (* TODO: __FC__NSIG *)
+ gen_define_macro fmt "__FC_NSIG" mach.nsig;
(* 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 37f7ef14d09c8d67512fea58839224a28ca23633..41556c96c9aba3d600cbeb2a8018a5c8e24a1db8 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1914,6 +1914,7 @@ type mach = {
tmp_max: string; (* expansion of TMP_MAX macro *)
rand_max: string; (* expansion of RAND_MAX macro *)
mb_cur_max: string; (* expansion of MB_CUR_MAX macro *)
+ nsig: string; (* expansion of non-standard NSIG 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 f513e304f575f15437b3e7cc8b10fa08cf851d64..b3342275ccfbe05f82c298f0ec07ca4e4b8152bd 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2676,6 +2676,7 @@ let dummy_machdep =
tmp_max = "1024";
rand_max = "0xFFFFFFFE";
mb_cur_max = "16";
+ nsig = "";
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index b3593e3c11ba678a663097bc23395fa667a7753f..f0efefcba8d498f262a6eec0afa47b03b2547c78 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -49,6 +49,7 @@ let mach =
tmp_max = "4095";
rand_max = "0xFFFFFFFE";
mb_cur_max = "16";
+ nsig = "";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index ae66369154d0ad9d1375562e50535b55b23b7ae6..3517a4968c88a2592b8c92551650347d07a7cada 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -45,3 +45,4 @@ rand_max: '0xFFFFFE'
mb_cur_max: 16
sig_atomic_t: int
time_t: long
+nsig: ''
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 7edc20afd1655dd94219053eecafffdd3c9ef263..df21c1e192b710f9418826bca447b574ad9c149c 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -48,6 +48,7 @@ let md = {
tmp_max = "0xFFFFFFFF";
rand_max = "0xFFFFFFFE";
mb_cur_max = "16";
+ nsig = 64;
}
let () =