Merge branch 'feature/andre/libc-stdalign' into 'master'

[Libc] add stdalign.h

See merge request frama-c/frama-c!3585

headers/header_spec.txt

@@ -284,6 +284,7 @@ share/libc/semaphore.h: CEA_LGPL
 share/libc/setjmp.h: CEA_LGPL
 share/libc/signal.c: CEA_LGPL
 share/libc/signal.h: CEA_LGPL
+share/libc/stdalign.h: CEA_LGPL
 share/libc/stdarg.h: CEA_LGPL
 share/libc/stdatomic.c: CEA_LGPL
 share/libc/stdatomic.h: CEA_LGPL

share/libc/__fc_libc.h

@@ -73,6 +73,7 @@
 #include "semaphore.h"
 #include "setjmp.h"
 #include "signal.h"
+#include "stdalign.h"
 #include "stdarg.h"
 #include "stdatomic.h"
 #include "stdbool.h"

share/libc/stdalign.h

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2021                                               */
+/*    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).            */
+/*                                                                        */
+/**************************************************************************/
+
+// Non-ISO, Non-POSIX; header provided only for improved compatibility with
+// non-portable code.
+
+#ifndef __FC_STDALIGN
+#define __FC_STDALIGN
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+
+#define alignas _Alignas
+#define alignof _Alignof
+
+__END_DECLS
+__POP_FC_STDLIB
+#endif

tests/libc/fc_libc.c

@@ -122,6 +122,7 @@
 #include "semaphore.h"
 #include "setjmp.h"
 #include "signal.h"
+#include "stdalign.h"
 #include "stdarg.h"
 #include "stdatomic.h"
 #include "stdbool.h"

tests/libc/oracle/fc_libc.0.res.oracle

@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] fc_libc.c:172: assertion got status valid.
 [eva] fc_libc.c:173: assertion got status valid.
 [eva] fc_libc.c:174: assertion got status valid.
 [eva] fc_libc.c:175: assertion got status valid.
+[eva] fc_libc.c:176: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

tests/libc/oracle/fc_libc.2.res.oracle

@@ -93,6 +93,7 @@ skipping FRAMAC_SHARE/libc/complex.h
 [kernel] Parsing FRAMAC_SHARE/libc/semaphore.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/setjmp.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/signal.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/stdalign.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/stdarg.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/stdatomic.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/stdbool.h (with preprocessing)