diff --git a/.gitattributes b/.gitattributes index 4b3153a8a04f91e9342f547f8b71a712f818da47..b56c468b60c519126c53eeb8773852ea2f107044 100644 --- a/.gitattributes +++ b/.gitattributes @@ -266,6 +266,7 @@ README* header_spec=.ignore /share/win32_installer.iss header_spec=.ignore /share/win32_manual_installation_step.txt header_spec=.ignore /share/compliance/*.json header_spec=.ignore +/share/machdeps/machdep-schema.json header_spec=.ignore /tests/**/* header_spec=.ignore diff --git a/make_machdep/alignof_aligned.c b/make_machdep/alignof_aligned.c index 4e3406707b8041a6593e009adfcbe272f3bbce7c..1ab18626f94e160edc7abcdfe45a365d56b587cf 100644 --- a/make_machdep/alignof_aligned.c +++ b/make_machdep/alignof_aligned.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" char array[1] __attribute__((aligned)); diff --git a/make_machdep/alignof_double.c b/make_machdep/alignof_double.c index 638d4749eda51d26b49dda6fae317cbccf1619b0..3ad3c9526be103cbb5f4ce11a6ae5d7b83174d13 100644 --- a/make_machdep/alignof_double.c +++ b/make_machdep/alignof_double.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(double) != 1, "alignof_double is 1"); diff --git a/make_machdep/alignof_float.c b/make_machdep/alignof_float.c index 93a87cbec67a60947f65b2e6ded13d9f5fd7e70e..2bbb0bf8967db1baa1a3889a27041d123d5f4e7f 100644 --- a/make_machdep/alignof_float.c +++ b/make_machdep/alignof_float.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(float) != 1, "alignof_float is 1"); diff --git a/make_machdep/alignof_fun.c b/make_machdep/alignof_fun.c index 6d3ba20a8a62a52bd73ad6cf9e997a2ce53f7c8c..26028f6b5a3b4e604b7dee757f85cfe3ec55b3b7 100644 --- a/make_machdep/alignof_fun.c +++ b/make_machdep/alignof_fun.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(void ()) != 1, "alignof_fun is 1"); diff --git a/make_machdep/alignof_int.c b/make_machdep/alignof_int.c index db2098074713c5a423e49cd1b9e473a53fd54cdb..a83f429cd061be487e130f0fc69330cdb8e563a5 100644 --- a/make_machdep/alignof_int.c +++ b/make_machdep/alignof_int.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(int) != 1, "alignof_int is 1"); _Static_assert(ALIGNOF(int) != 2, "alignof_int is 2"); diff --git a/make_machdep/alignof_long.c b/make_machdep/alignof_long.c index 2939718ac29b6e771c91f5c44ff59ff933c096b6..f34ec3ca89f349404fbe181edf9c90adc78fb85f 100644 --- a/make_machdep/alignof_long.c +++ b/make_machdep/alignof_long.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(long) != 1, "alignof_long is 1"); _Static_assert(ALIGNOF(long) != 2, "alignof_long is 2"); diff --git a/make_machdep/alignof_longdouble.c b/make_machdep/alignof_longdouble.c index 3bec841257b133e15b5b161846207f240a262e12..0cd52668fe54cad32a0b0d26429259927365b5e7 100644 --- a/make_machdep/alignof_longdouble.c +++ b/make_machdep/alignof_longdouble.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(long double) != 1, "alignof_longdouble is 1"); diff --git a/make_machdep/alignof_longlong.c b/make_machdep/alignof_longlong.c index cb808ff6e687694fea5c8c62f0687c6ebf3fc68f..222eba81362a4089b7af59a5ff0891817be497be 100644 --- a/make_machdep/alignof_longlong.c +++ b/make_machdep/alignof_longlong.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(long long) != 1, "alignof_longlong is 1"); _Static_assert(ALIGNOF(long long) != 2, "alignof_longlong is 2"); diff --git a/make_machdep/alignof_ptr.c b/make_machdep/alignof_ptr.c index 92b094544da4e0cd232cffa4b236739e008502bd..babe1cd560d7277132648ee2a6396bd2910768a9 100644 --- a/make_machdep/alignof_ptr.c +++ b/make_machdep/alignof_ptr.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(void *) != 1, "alignof_ptr is 1"); diff --git a/make_machdep/alignof_short.c b/make_machdep/alignof_short.c index bbad8d49c13b14d7568dd39235fa916dd7b769bf..7e1c66cfa417d6a94081d640443911add7c316fa 100644 --- a/make_machdep/alignof_short.c +++ b/make_machdep/alignof_short.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF(short) != 1, "alignof_short is 1"); _Static_assert(ALIGNOF(short) != 2, "alignof_short is 2"); diff --git a/make_machdep/alignof_str.c b/make_machdep/alignof_str.c index 86d50e598ca1c9658168598de844a9aa74bbb301..51ba68521cd21c26e24fcd5f362f4e4c1cb2cb5b 100644 --- a/make_machdep/alignof_str.c +++ b/make_machdep/alignof_str.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" _Static_assert(ALIGNOF("test string") != 1, "alignof_str is 1"); diff --git a/make_machdep/char_is_unsigned.c b/make_machdep/char_is_unsigned.c index aca0a8054061692e2109ef2447ea778bd96c81f4..46ad63d750231360d7f276aa2d62e04f31e5cfd5 100644 --- a/make_machdep/char_is_unsigned.c +++ b/make_machdep/char_is_unsigned.c @@ -1,2 +1,24 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert((char)-1 >= 0 ? 1 : 0, "char_is_unsigned is False"); _Static_assert((char)-1 >= 0 ? 0 : 1, "char_is_unsigned is True"); diff --git a/make_machdep/const_string_literals.c b/make_machdep/const_string_literals.c index 2e51bff8891ef06ae3fb27ed92f426221723364b..35fb4e651ec1e4c5ba3f07033d19e1085bb37137 100644 --- a/make_machdep/const_string_literals.c +++ b/make_machdep/const_string_literals.c @@ -1 +1,23 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + char *const_string_literals = "%$#!"; diff --git a/make_machdep/has__builtin_va_list.c b/make_machdep/has__builtin_va_list.c index 77d2b17a4075ca43bf2f513ca9bf36c6aec992e4..4f2420598eca140e508b6f6259185edadea87388 100644 --- a/make_machdep/has__builtin_va_list.c +++ b/make_machdep/has__builtin_va_list.c @@ -1,2 +1,24 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + /* If this compiles, we assume the compiler has __builtin_va_list. */ __builtin_va_list l = {0}; diff --git a/make_machdep/little_endian.c b/make_machdep/little_endian.c index 2632a464e029ce1f6ca826b5e8a985c2f6b7f9a2..eeb191ac1232f6eb1391f5f1dfa8e06889e28e8c 100644 --- a/make_machdep/little_endian.c +++ b/make_machdep/little_endian.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + #if defined(__BYTE_ORDER__) # if __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__ __attribute__((section(".data"))) diff --git a/make_machdep/make_machdep.py b/make_machdep/make_machdep.py index 8b9d6519d0a0ef012433a907f883b31f6d676015..25df600d93d061346fb5cc4ae2424fe1672d1400 100755 --- a/make_machdep/make_machdep.py +++ b/make_machdep/make_machdep.py @@ -1,4 +1,25 @@ #!/usr/bin/env python +########################################################################## +# # +# 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). # +# # +########################################################################## """ Produces a machdep.ml file for a given architecture. diff --git a/make_machdep/make_machdep_common.h b/make_machdep/make_machdep_common.h index 46e98a4d20c3b5b63310763b215b3932decc4761..82feab58fac0cd300eef939780660a7e62433a63 100644 --- a/make_machdep/make_machdep_common.h +++ b/make_machdep/make_machdep_common.h @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + #if __STDC_VERSION__ < 201112L && !defined(__COMPCERT__) /* Try using a compiler builtin */ #define ALIGNOF alignof diff --git a/make_machdep/ptrdiff_t.c b/make_machdep/ptrdiff_t.c index e19be36f09fdc4af927a36bb6928c36d4acecce5..29c9d38d42b5ca332b0111761b323ff69d60b1fc 100644 --- a/make_machdep/ptrdiff_t.c +++ b/make_machdep/ptrdiff_t.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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 <stddef.h> #define TEST_TYPE ptrdiff_t diff --git a/make_machdep/size_t.c b/make_machdep/size_t.c index c853b2705090b1ecc8d7f4a709ed307dc99bbf79..65bed06a2e6b281832c6727443eb9c2a7a1c3286 100644 --- a/make_machdep/size_t.c +++ b/make_machdep/size_t.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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 <stddef.h> #include "make_machdep_common.h" diff --git a/make_machdep/sizeof_alignof_standard.c b/make_machdep/sizeof_alignof_standard.c index 8aaa2d8041826b7423f64e6b2640a82a5d43001e..ffd82d33796aaa74ecc8847e170c3a0b5ea2f1dc 100644 --- a/make_machdep/sizeof_alignof_standard.c +++ b/make_machdep/sizeof_alignof_standard.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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" /* We want to obtain values produced by the compiler. diff --git a/make_machdep/sizeof_double.c b/make_machdep/sizeof_double.c index e03d044bedc26e82dd2ec9729bbfe49e98a4971e..c87c337250d403c4bce05eac6cf3f5197098132b 100644 --- a/make_machdep/sizeof_double.c +++ b/make_machdep/sizeof_double.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(double) != 1, "sizeof_double is 1"); _Static_assert(sizeof(double) != 2, "sizeof_double is 2"); _Static_assert(sizeof(double) != 3, "sizeof_double is 3"); diff --git a/make_machdep/sizeof_float.c b/make_machdep/sizeof_float.c index e3c22a3f78f4c9edc8f81154722947632bcd294a..6de246c1bde90eb86caec97394c703a2b6974c32 100644 --- a/make_machdep/sizeof_float.c +++ b/make_machdep/sizeof_float.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(float) != 1, "sizeof_float is 1"); _Static_assert(sizeof(float) != 2, "sizeof_float is 2"); _Static_assert(sizeof(float) != 3, "sizeof_float is 3"); diff --git a/make_machdep/sizeof_fun.c b/make_machdep/sizeof_fun.c index 9b893dbab6913ee5dbec41e5deeea526da7f194a..0a8af7f1e69ba5b1db06d0f218b8d71431d4d316 100644 --- a/make_machdep/sizeof_fun.c +++ b/make_machdep/sizeof_fun.c @@ -1 +1,23 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(void ()) != 1, "sizeof_fun is 1"); diff --git a/make_machdep/sizeof_int.c b/make_machdep/sizeof_int.c index 758a8da7b26c4e92507ddddeec88c0fe17cdb0c6..914fa6af09af11e6d7565b50c24b75ec6e7f5fe2 100644 --- a/make_machdep/sizeof_int.c +++ b/make_machdep/sizeof_int.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(int) != 1, "sizeof_int is 1"); _Static_assert(sizeof(int) != 2, "sizeof_int is 2"); _Static_assert(sizeof(int) != 3, "sizeof_int is 3"); diff --git a/make_machdep/sizeof_long.c b/make_machdep/sizeof_long.c index 029c6a771b624580476002f478a7965ac0ae7502..a545896ddfcb6d6b26dccddd33268cfebeb87fda 100644 --- a/make_machdep/sizeof_long.c +++ b/make_machdep/sizeof_long.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(long) != 1, "sizeof_long is 1"); _Static_assert(sizeof(long) != 2, "sizeof_long is 2"); _Static_assert(sizeof(long) != 3, "sizeof_long is 3"); diff --git a/make_machdep/sizeof_longdouble.c b/make_machdep/sizeof_longdouble.c index d76733dce3cc0a8c0b2ec0f1c68902b660c35545..78922473994cf9d2305f426ab067079b4ba5fe04 100644 --- a/make_machdep/sizeof_longdouble.c +++ b/make_machdep/sizeof_longdouble.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(long double) != 1, "sizeof_longdouble is 1"); _Static_assert(sizeof(long double) != 2, "sizeof_longdouble is 2"); _Static_assert(sizeof(long double) != 3, "sizeof_longdouble is 3"); diff --git a/make_machdep/sizeof_longlong.c b/make_machdep/sizeof_longlong.c index ce3b1c7e738ee3c280473a9e4209d4c653b90e88..246b21d6fdafe51191d9905439cf5db08b29a5d2 100644 --- a/make_machdep/sizeof_longlong.c +++ b/make_machdep/sizeof_longlong.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(long long) != 1, "sizeof_longlong is 1"); _Static_assert(sizeof(long long) != 2, "sizeof_longlong is 2"); _Static_assert(sizeof(long long) != 3, "sizeof_longlong is 3"); diff --git a/make_machdep/sizeof_ptr.c b/make_machdep/sizeof_ptr.c index 359e2f962a9c1cb5dcc33e40c76bc4916a9d3a0d..d99d94fbcdde01a34d5d5c5db6d855c079c465ba 100644 --- a/make_machdep/sizeof_ptr.c +++ b/make_machdep/sizeof_ptr.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(void *) != 1, "sizeof_ptr is 1"); _Static_assert(sizeof(void *) != 2, "sizeof_ptr is 2"); _Static_assert(sizeof(void *) != 3, "sizeof_ptr is 3"); diff --git a/make_machdep/sizeof_short.c b/make_machdep/sizeof_short.c index 299d215175573cf1efb0946ace6bb89b86419e83..5287ec206760c0bb43d3e5fd6d06ec016dd819dc 100644 --- a/make_machdep/sizeof_short.c +++ b/make_machdep/sizeof_short.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(short) != 1, "sizeof_short is 1"); _Static_assert(sizeof(short) != 2, "sizeof_short is 2"); _Static_assert(sizeof(short) != 3, "sizeof_short is 3"); diff --git a/make_machdep/sizeof_void.c b/make_machdep/sizeof_void.c index c5f0e53a77bdb82e8078ae31db54ee2f49553928..bac4d738ffd58543d42c3b6b346897b393ff5cfc 100644 --- a/make_machdep/sizeof_void.c +++ b/make_machdep/sizeof_void.c @@ -1 +1,23 @@ +/**************************************************************************/ +/* */ +/* 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). */ +/* */ +/**************************************************************************/ + _Static_assert(sizeof(void)!=1,"sizeof_void is 1"); diff --git a/make_machdep/wchar_t.c b/make_machdep/wchar_t.c index 564963d211e1b4d6e600205b003eda1f34c8705d..ce5b3ae2a74ab4fb8f83f6a227f5aaf174cb9b70 100644 --- a/make_machdep/wchar_t.c +++ b/make_machdep/wchar_t.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* 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 <stddef.h> #define TEST_TYPE wchar_t