From 6f27a7d0c52cf751c4677a832e17557cdc840957 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 3 Mar 2023 14:59:53 +0100
Subject: [PATCH] [machdep] support for sig_atomic_t in new machdep
---
share/libc/signal.h | 3 +-
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 | 2 ++
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/sig_atomic_t.c | 33 +++++++++++++++++++
src/kernel_internals/runtime/machdep.ml | 5 +--
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 +
19 files changed, 59 insertions(+), 4 deletions(-)
create mode 100644 share/machdeps/make_machdep/sig_atomic_t.c
diff --git a/share/libc/signal.h b/share/libc/signal.h
index 126a96f1f5e..be91ea934ae 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -35,9 +35,8 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-/* TODO: put sig_atomic_t in machdep */
#ifndef __sig_atomic_t_defined
-typedef volatile int sig_atomic_t;
+typedef volatile __FC_SIG_ATOMIC_T sig_atomic_t;
#define __sig_atomic_t_defined
#endif
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index 0d4b2f34d58..05ad831e993 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -160,6 +160,12 @@ rand_max:
type: string
+sig_atomic_t:
+
+ description: representation of 'sig_atomic_t' (defined in signal.h)
+
+ type: string
+
size_t:
description: type of 'sizeof e'
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index 3a32f6fad47..6e2583960b0 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -27,6 +27,7 @@ mb_cur_max: ((size_t)16)
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
+sig_atomic_t: int
size_t: unsigned int
sizeof_double: 4
sizeof_float: 4
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index f538eb0df63..c4f99b0821b 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -17,6 +17,7 @@ has__builtin_va_list: true
intptr_t: long
little_endian: true
ptrdiff_t: int
+sig_atomic_t: int
size_t: unsigned int
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index 8ccb3952e2c..aba988b5624 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -25,6 +25,7 @@ mb_cur_max: ((size_t) 16 )
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
+sig_atomic_t: int
size_t: unsigned int
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index 39f935901bc..ed89198e377 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -25,6 +25,7 @@ mb_cur_max: ((size_t) 16 )
posix_version: 200809L
ptrdiff_t: long
rand_max: '2147483647'
+sig_atomic_t: int
size_t: unsigned long
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index ba58f4d8eac..716351aa934 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -17,6 +17,8 @@ has__builtin_va_list: false
intptr_t: signed long long
little_endian: true
ptrdiff_t: long long
+# NB: wasn't defined at all in old __fc_machdep.h
+sig_atomic_t: int
size_t: unsigned long long
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 244a3c3874d..b0678bffa4d 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -27,6 +27,7 @@ mb_cur_max: ((size_t)16)
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
+sig_atomic_t: int
size_t: unsigned int
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index 33be991a565..552f484c93f 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -17,6 +17,7 @@ has__builtin_va_list: true
intptr_t: long
little_endian: true
ptrdiff_t: int
+sig_atomic_t: int
size_t: unsigned int
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index 154475ce0fa..c17d66ce214 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -25,6 +25,7 @@ mb_cur_max: ((size_t) 16 )
posix_version: 200809L
ptrdiff_t: int
rand_max: '2147483647'
+sig_atomic_t: int
size_t: unsigned int
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index dcb294278cf..36a7dce5dae 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -25,6 +25,7 @@ mb_cur_max: ((size_t) 16 )
posix_version: 200809L
ptrdiff_t: long
rand_max: '2147483647'
+sig_atomic_t: int
size_t: unsigned long
sizeof_double: 8
sizeof_float: 4
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index add95aab734..fe5a481f89f 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -172,6 +172,7 @@ source_files = [
("intptr_t.c", "type"),
("uintptr_t.c", "type"),
("wint_t.c", "type"),
+ ("sig_atomic_t.c", "type"),
("char_is_unsigned.c", "bool"),
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
diff --git a/share/machdeps/make_machdep/sig_atomic_t.c b/share/machdeps/make_machdep/sig_atomic_t.c
new file mode 100644
index 00000000000..f06be916baf
--- /dev/null
+++ b/share/machdeps/make_machdep/sig_atomic_t.c
@@ -0,0 +1,33 @@
+/**************************************************************************/
+/* */
+/* 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 "make_machdep_common.h"
+#include <signal.h>
+
+#define TEST_TYPE sig_atomic_t
+
+TEST_TYPE_IS(unsigned int)
+TEST_TYPE_IS(int)
+TEST_TYPE_IS(unsigned long)
+TEST_TYPE_IS(long)
+TEST_TYPE_IS(unsigned long long)
+TEST_TYPE_IS(long long)
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index c1c2f636c7d..1fe63aec1c2 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -234,8 +234,9 @@ let gen_all_defines fmt mach =
(List.assoc (no_signedness mach.intptr_t) pp_of_kind);
gen_define_macro fmt "__FC_WORDSIZE" mach.wordsize;
gen_define_macro fmt "__FC_POSIX_VERSION" mach.posix_version;
- (* TODO: __FC_SIG_ATOMIC_MIN *)
- (* TODO: __FC_SIG_ATOMIC_MAX *)
+ gen_define_string fmt "__FC_SIG_ATOMIC_T" mach.sig_atomic_t;
+ gen_intlike_min fmt "__FC_SIG_ATOMIC_MIN" mach.sig_atomic_t mach;
+ gen_intlike_max fmt "__FC_SIG_ATOMIC_MAX" mach.sig_atomic_t mach;
gen_define_macro fmt "__FC_BUFSIZ" mach.bufsiz;
gen_define_macro fmt "__FC_EOF" mach.eof;
gen_define_macro fmt "__FC_FOPEN_MAX" mach.fopen_max;
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 722c99194bc..b23472c9d17 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1882,6 +1882,7 @@ type mach = {
intptr_t: string; (* Type of "intptr_t" *)
uintptr_t: string; (* Type of "uintptr_t" *)
wint_t: string; (* Type of "wint_t" *)
+ sig_atomic_t: string; (* Type of "sig_atomic_t" *)
alignof_short: int; (* Alignment of "short" *)
alignof_int: int; (* Alignment of "int" *)
alignof_long: int; (* Alignment of "long" *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 9c9f4c62f95..847cdaab513 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2646,6 +2646,7 @@ let dummy_machdep =
intptr_t = "long"; (* Type of "intptr_t" *)
uintptr_t = "unsigned long"; (* Type of "uintptr_t" *)
wint_t = "int";
+ sig_atomic_t = "int";
alignof_short = 2;
alignof_int = 4;
alignof_long = 8;
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index 99d86dd1467..1953e4e5823 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -22,6 +22,7 @@ let mach =
wint_t = "int";
wchar_t = "int";
ptrdiff_t = "int";
+ sig_atomic_t = "int";
alignof_short = 2;
alignof_int = 3;
alignof_long = 4;
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index d779f218d20..56aca3d4130 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -43,3 +43,4 @@ l_tmpnam: '255'
tmp_max: '255'
rand_max: '0xFFFFFE'
mb_cur_max: 16
+sig_atomic_t: int
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 48f3d97acbc..b2788e8fca0 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -34,6 +34,7 @@ let md = {
uintptr_t = "unsigned int";
ptrdiff_t = "int";
wint_t = "long";
+ sig_atomic_t = "int";
has__builtin_va_list = true;
weof = "(-1L)";
wordsize = "16";
--
GitLab