From b7b3b03b75421bf4e3dd2139fa42bd0bd79c7923 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 15 Feb 2023 15:44:15 +0100
Subject: [PATCH] [machdep] create headers for new files
---
.gitattributes | 1 +
make_machdep/alignof_aligned.c | 22 ++++++++++++++++++++++
make_machdep/alignof_double.c | 22 ++++++++++++++++++++++
make_machdep/alignof_float.c | 22 ++++++++++++++++++++++
make_machdep/alignof_fun.c | 22 ++++++++++++++++++++++
make_machdep/alignof_int.c | 22 ++++++++++++++++++++++
make_machdep/alignof_long.c | 22 ++++++++++++++++++++++
make_machdep/alignof_longdouble.c | 22 ++++++++++++++++++++++
make_machdep/alignof_longlong.c | 22 ++++++++++++++++++++++
make_machdep/alignof_ptr.c | 22 ++++++++++++++++++++++
make_machdep/alignof_short.c | 22 ++++++++++++++++++++++
make_machdep/alignof_str.c | 22 ++++++++++++++++++++++
make_machdep/char_is_unsigned.c | 22 ++++++++++++++++++++++
make_machdep/const_string_literals.c | 22 ++++++++++++++++++++++
make_machdep/has__builtin_va_list.c | 22 ++++++++++++++++++++++
make_machdep/little_endian.c | 22 ++++++++++++++++++++++
make_machdep/make_machdep.py | 21 +++++++++++++++++++++
make_machdep/make_machdep_common.h | 22 ++++++++++++++++++++++
make_machdep/ptrdiff_t.c | 22 ++++++++++++++++++++++
make_machdep/size_t.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_alignof_standard.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_double.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_float.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_fun.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_int.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_long.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_longdouble.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_longlong.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_ptr.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_short.c | 22 ++++++++++++++++++++++
make_machdep/sizeof_void.c | 22 ++++++++++++++++++++++
make_machdep/wchar_t.c | 22 ++++++++++++++++++++++
32 files changed, 682 insertions(+)
diff --git a/.gitattributes b/.gitattributes
index 4b3153a8a04..b56c468b60c 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 4e3406707b8..1ab18626f94 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 638d4749eda..3ad3c9526be 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 93a87cbec67..2bbb0bf8967 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 6d3ba20a8a6..26028f6b5a3 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 db209807471..a83f429cd06 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 2939718ac29..f34ec3ca89f 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 3bec841257b..0cd52668fe5 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 cb808ff6e68..222eba81362 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 92b094544da..babe1cd560d 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 bbad8d49c13..7e1c66cfa41 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 86d50e598ca..51ba68521cd 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 aca0a805406..46ad63d7502 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 2e51bff8891..35fb4e651ec 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 77d2b17a407..4f2420598ec 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 2632a464e02..eeb191ac123 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 8b9d6519d0a..25df600d93d 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 46e98a4d20c..82feab58fac 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 e19be36f09f..29c9d38d42b 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 c853b270509..65bed06a2e6 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 8aaa2d80418..ffd82d33796 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 e03d044bedc..c87c337250d 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 e3c22a3f78f..6de246c1bde 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 9b893dbab69..0a8af7f1e69 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 758a8da7b26..914fa6af09a 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 029c6a771b6..a545896ddfc 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 d76733dce3c..78922473994 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 ce3b1c7e738..246b21d6fda 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 359e2f962a9..d99d94fbcdd 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 299d2151755..5287ec20676 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 c5f0e53a77b..bac4d738ffd 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 564963d211e..ce5b3ae2a74 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
--
GitLab