From 4439682b936dee2f9089079b36f37bcf986a2fd9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 3 Mar 2023 18:33:34 +0100
Subject: [PATCH] [machdep] support for NSIG in new machdep
---
share/libc/__fc_define_sigset_t.h | 1 -
share/libc/signal.h | 11 +++++--
share/machdeps/machdep-schema.yaml | 6 ++++
share/machdeps/machdep_avr_16.yaml | 1 +
share/machdeps/machdep_gcc_x86_16.yaml | 1 +
share/machdeps/machdep_gcc_x86_32.yaml | 1 +
share/machdeps/machdep_gcc_x86_64.yaml | 1 +
share/machdeps/machdep_msvc_x86_64.yaml | 1 +
share/machdeps/machdep_ppc_32.yaml | 1 +
share/machdeps/machdep_x86_16.yaml | 1 +
share/machdeps/machdep_x86_32.yaml | 1 +
share/machdeps/machdep_x86_64.yaml | 1 +
share/machdeps/make_machdep/make_machdep.py | 1 +
share/machdeps/make_machdep/nsig.c | 29 +++++++++++++++++++
src/kernel_internals/runtime/machdep.ml | 3 +-
src/kernel_services/ast_data/cil_types.ml | 1 +
.../ast_queries/cil_datatype.ml | 1 +
tests/misc/custom_machdep.ml | 1 +
tests/misc/custom_machdep.yaml | 1 +
tests/syntax/machdep_char_unsigned.ml | 1 +
20 files changed, 60 insertions(+), 5 deletions(-)
create mode 100644 share/machdeps/make_machdep/nsig.c
diff --git a/share/libc/__fc_define_sigset_t.h b/share/libc/__fc_define_sigset_t.h
index b5718423a3c..30f99f6f804 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 be91ea934ae..30851947103 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 795492d92db..82beb3530ac 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 f4c03215a7d..76ce8188aee 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 e8b8136039b..7d36c6f2c24 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 bfe54a7b612..5992ccb7121 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 2406b67761c..2092ac09fb1 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 95d157a05b1..a71a5365fa0 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 a3ad08e801e..fda90435289 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 d0128407f6e..aa873f36dd6 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 af0bed28d86..41c794f2371 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 e77034fed4a..96d69bf96f1 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 0978cbe1838..55c62051b6e 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 00000000000..5fa6451f020
--- /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 c216353b5c7..c67516d799a 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 37f7ef14d09..41556c96c9a 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 f513e304f57..b3342275ccf 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 b3593e3c11b..f0efefcba8d 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 ae66369154d..3517a4968c8 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 7edc20afd16..df21c1e192b 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 () =
--
GitLab