diff --git a/share/libc/signal.h b/share/libc/signal.h index 126a96f1f5eb0c79b8be42f718c9cdd4057f7cf1..be91ea934aea93f3d1079594e817409cc5ce8aee 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 0d4b2f34d58af18ed677c59a1c28d3a5f8ed644c..05ad831e993f78d522fb2364835c6cf6ba29fc60 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 3a32f6fad473cf57727a6c7c31076473dff807cb..6e2583960b04677a372487d32c5380d563212db5 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 f538eb0df63193ae59d0f766306178203e1249b1..c4f99b0821b5281f600ec4be89651e0810e67ecd 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 8ccb3952e2c95094d578b8036768c3d6e397c08c..aba988b5624c444e51a8f6e2d187a93babef1602 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 39f935901bc56f8d9e6ccaa002a4376144ecbaf1..ed89198e37771120c40703bd0103f95063805dcf 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 ba58f4d8eace71b8fff6f7879e2f3ad271e58d36..716351aa934c625fad9a6d2e52fc9473affe719a 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 244a3c3874dea50d65c592e3b154f7901f153b5b..b0678bffa4d59c069764a6355bde2241656faa34 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 33be991a565ebb04c0640683a93e1909a47ad1b2..552f484c93f588d4f9202cdf1d700da128a2f3e9 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 154475ce0fabb9bec55040ab20a0ee9b7de26a59..c17d66ce2148ab2d8c5933c9ca40cfa1763ca8ce 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 dcb294278cf8f21ae6868081c48cb5015f74b6e7..36a7dce5daeb5e1c13b87e3de1ce4e700cf56d4d 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 add95aab7340597a593a83b23fa9e751c4ce0bef..fe5a481f89fb554eea9228405d85cdd9ff147723 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 0000000000000000000000000000000000000000..f06be916baf72551844b51a0d288f651ee828c42 --- /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 c1c2f636c7d08fc6bc0fb8cf196a1fa366cf2565..1fe63aec1c200c161eb0fb34b92e73e31b2985ad 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 722c99194bcec6aa6de3f764e0b24319b4908f40..b23472c9d17826c522e3a5c510285270c235abe0 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 9c9f4c62f9525603755a69050617acf9f9ec4fc2..847cdaab5133bd18e709e413b941e9a609ed7486 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 99d86dd1467e4257a574ce130b122a8f24423d07..1953e4e58234d924b513504d3e613d121bc6bc65 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 d779f218d20ea925e1a58d99a37c9ea3f8e8b99d..56aca3d413092dd6d3b12d3462674d86f3802e79 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 48f3d97acbce62b9f220e8736f6f497774d21743..b2788e8fca0a40fc6695d163989292b9530ca954 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";