[kernel] Add max_align_t to machdeps

share/libc/stddef.h

@@ -30,6 +30,14 @@ __BEGIN_DECLS
 typedef __PTRDIFF_T ptrdiff_t;
 #define __ptrdiff_t_defined
 #endif
+
+// max_align_t is not defined in every machdeps
+#ifdef __MAX_ALIGN_T
+#ifndef __max_align_t_defined
+typedef __MAX_ALIGN_T max_align_t;
+#define __max_align_t_defined
+#endif
+#endif
 __END_DECLS
 #include "__fc_define_size_t.h"
 #include "__fc_define_ssize_t.h"

share/machdeps/machdep-schema.yaml

@@ -66,6 +66,12 @@ alignof_str:
 
   type: integer
 
+max_align_t:
+
+  description: definition of 'max_align_t' (in stddef.h)
+
+  type: string
+
 bufsiz:
 
   description: value of 'BUFSIZ' macro

share/machdeps/machdep_avr_16.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 1
 alignof_ptr: 1
 alignof_short: 2
 alignof_str: 1
+max_align_t: struct {int __max_align; } __attribute__ ((aligned (8)))
 bufsiz: '1024'
 char_is_unsigned: false
 compiler: clang

share/machdeps/machdep_avr_8.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 1
 alignof_ptr: 1
 alignof_short: 2
 alignof_str: 1
+max_align_t: struct {int __max_align; } __attribute__ ((aligned (8)))
 bufsiz: '1024'
 char_is_unsigned: false
 compiler: clang

share/machdeps/machdep_gcc_x86_16.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+max_align_t: struct {int __max_align; } __attribute__ ((aligned (16)))
 char_is_unsigned: false
 compiler: gcc
 cpp_arch_flags:

share/machdeps/machdep_gcc_x86_32.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+max_align_t: struct {int __max_align; } __attribute__ ((aligned (16)))
 bufsiz: '8192'
 char_is_unsigned: false
 compiler: gcc

share/machdeps/machdep_gcc_x86_64.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 8
 alignof_ptr: 8
 alignof_short: 2
 alignof_str: 1
+max_align_t: long double
 bufsiz: '8192'
 char_is_unsigned: false
 compiler: gcc

share/machdeps/machdep_msvc_x86_64.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 8
 alignof_ptr: 8
 alignof_short: 2
 alignof_str: 1
+max_align_t: ''
 char_is_unsigned: false
 compiler: msvc
 cpp_arch_flags:
@@ -50,7 +51,7 @@ wordsize: '64'
 posix_version: ''
 
 # NB: except for l_tmpnam, the following macros are not defined in the old
-# __fc_machdep.h in the MSVC_X86_64 section. The values below have thus been 
+# __fc_machdep.h in the MSVC_X86_64 section. The values below have thus been
 # taken from gnu
 bufsiz: '8192'
 eof: '(-1)'

share/machdeps/machdep_ppc_32.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 8
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+max_align_t: long double
 bufsiz: '8192'
 char_is_unsigned: true
 compiler: clang

share/machdeps/machdep_x86_16.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+max_align_t: struct {int __max_align; } __attribute__ ((aligned (16)))
 char_is_unsigned: false
 compiler: generic
 cpp_arch_flags:

share/machdeps/machdep_x86_32.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+max_align_t: struct {int __max_align; } __attribute__ ((aligned (16)))
 bufsiz: '8192'
 char_is_unsigned: false
 compiler: generic

share/machdeps/machdep_x86_64.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 8
 alignof_ptr: 8
 alignof_short: 2
 alignof_str: 1
+max_align_t: long double
 bufsiz: '8192'
 char_is_unsigned: false
 compiler: generic

share/machdeps/make_machdep/make_machdep.py

@@ -217,6 +217,7 @@ source_files = [
     ("ssize_t.c", "type"),
     ("wchar_t.c", "type"),
     ("ptrdiff_t.c", "type"),
+    ("max_align_t.c", "type"),
     ("intptr_t.c", "type"),
     ("uintptr_t.c", "type"),
     ("int_fast8_t.c", "type"),

share/machdeps/make_machdep/max_align_t.c

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2024                                               */
+/*    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 <stddef.h>
+
+#define TEST_MAX_ALIGN_T_IS(type) \
+    _Static_assert(ALIGNOF(max_align_t) != ALIGNOF(type), \
+                   "max_align_t is `"#type"`");
+
+TEST_MAX_ALIGN_T_IS(char)
+TEST_MAX_ALIGN_T_IS(short)
+TEST_MAX_ALIGN_T_IS(int)
+TEST_MAX_ALIGN_T_IS(long)
+TEST_MAX_ALIGN_T_IS(long long)
+TEST_MAX_ALIGN_T_IS(double)
+TEST_MAX_ALIGN_T_IS(long double)
+TEST_MAX_ALIGN_T_IS(struct {int __max_align; } __attribute__ ((aligned (8))))
+TEST_MAX_ALIGN_T_IS(struct {int __max_align; } __attribute__ ((aligned (16))))

src/kernel_internals/runtime/machdep.ml

@@ -62,6 +62,7 @@ type mach = {
   wint_t: string;
   sig_atomic_t: string;
   time_t: string;
+  max_align_t: string;
   alignof_short: int;
   alignof_int: int;
   alignof_long: int;
@@ -127,6 +128,7 @@ let dummy = {
   wint_t = "int";
   sig_atomic_t = "int";
   time_t = "long";
+  max_align_t = "long";
   alignof_short = 2;
   alignof_int = 4;
   alignof_long = 8;
@@ -187,17 +189,17 @@ module Machdep = struct
     fprintf fmt
       "{sizeof_short=%d;sizeof_int=%d;sizeof_long=%d;sizeof_longlong=%d;\
        sizeof_ptr=%d;sizeof_float=%d;sizeof_double=%d;sizeof_longdouble=%d;\
-       sizeof_void=%d;sizeof_fun=%d;size_t=%s;ssize_t=%s;wchar_t=%s;
+       sizeof_void=%d;sizeof_fun=%d;size_t=%s;ssize_t=%s;wchar_t=%s;\
        ptrdiff_t=%s;intptr_t=%s;uintptr_t=%s;\
        int_fast8_t=%s;int_fast16_t=%s;int_fast32_t=%s;int_fast64_t=%s;\
        uint_fast8_t=%s;uint_fast16_t=%s;uint_fast32_t=%s;uint_fast64_t=%s;\
-       wint_t=%s;sig_atomic_t=%s;time_t=%s;\
+       wint_t=%s;sig_atomic_t=%s;time_t=%s;max_align_t=%s;\
        alignof_short=%d;alignof_int=%d;alignof_long=%d;alignof_longlong=%d;\
        alignof_ptr=%d;alignof_float=%d;alignof_double=%d;alignof_longdouble=%d;\
        alignof_str=%d;alignof_fun=%d;alignof_aligned=%d;\
-       char_is_unsigned=%b;little_endian=%b;has__builtin_va_list=%b;
-       compiler=%s;cpp_arch_flags=%a;version=%s;weof=%s;wordsize=%s;
-       posix_version=%s;bufsiz=%s;eof=%s;fopen_max=%s;filename_max=%s;
+       char_is_unsigned=%b;little_endian=%b;has__builtin_va_list=%b;\
+       compiler=%s;cpp_arch_flags=%a;version=%s;weof=%s;wordsize=%s;\
+       posix_version=%s;bufsiz=%s;eof=%s;fopen_max=%s;filename_max=%s;\
        path_max=%s;tty_name_max=%s;host_name_max=%s;l_tmpnam=%s;tmp_max=%s;\
        rand_max=%s;mb_cur_max=%s;nsig=%s;errno=%a;machdep_name=%s;custom_defs=%a}"
       mach.sizeof_short
@@ -227,6 +229,7 @@ module Machdep = struct
       mach.wint_t
       mach.sig_atomic_t
       mach.time_t
+      mach.max_align_t
       mach.alignof_short
       mach.alignof_int
       mach.alignof_long
@@ -558,7 +561,6 @@ let gen_all_defines fmt ?(censored_macros=Datatype.String.Set.empty) mach =
   gen_sizeof_std fmt mach;
   gen_char_bit fmt mach;
   gen_precise_size_type fmt mach;
-  gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
   gen_define_string fmt "__SIZE_T" mach.size_t;
   gen_define_string fmt "__WCHAR_T" mach.wchar_t;
   gen_define_string fmt "__INTPTR_T" mach.intptr_t;
@@ -566,6 +568,8 @@ let gen_all_defines fmt ?(censored_macros=Datatype.String.Set.empty) mach =
   gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
   gen_define_string fmt "__WINT_T" mach.wint_t;
   gen_define_string fmt "__SSIZE_T" mach.ssize_t;
+  if String.length mach.max_align_t > 0 then
+    gen_define_string fmt "__MAX_ALIGN_T" mach.max_align_t;
   gen_intlike_max fmt "__FC_SIZE" mach.size_t mach;
   gen_intlike_min fmt "__FC_INTPTR" mach.intptr_t mach;
   gen_intlike_max fmt "__FC_INTPTR" mach.intptr_t mach;

src/kernel_internals/runtime/machdep.mli

@@ -56,6 +56,7 @@ type mach = {
   wint_t: string;         (** Type of "wint_t" *)
   sig_atomic_t: string;   (** Type of "sig_atomic_t" *)
   time_t: string;         (** Type of "time_t" *)
+  max_align_t: string;    (** Type of "max_align_t" *)
   alignof_short: int;     (** [_AlignOf(short)] *)
   alignof_int: int;       (** [_AlignOf(int)] *)
   alignof_long: int;      (** [_AlignOf(long)] *)

tests/misc/custom_machdep.yaml

@@ -9,6 +9,7 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+max_align_t: long double
 char_is_unsigned: false
 compiler: bar
 cpp_arch_flags: []

tests/syntax/machdep_char_unsigned.yaml

@@ -23,6 +23,7 @@ alignof_double: 2
 alignof_longdouble: 2
 alignof_str: 0
 alignof_fun: 0
+max_align_t: long long
 char_is_unsigned: true
 little_endian: true
 size_t: 'unsigned int'