From 4d3f6c2e9b4bd847cf5c6bd41e17d63722726eca Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 23 Oct 2020 14:23:59 +0200
Subject: [PATCH] [Libc] add list of compatible headers from the Frama-C libc

---
 headers/header_spec.txt                |   1 +
 share/libc/__fc_libc.h                 | 109 +++++++++++++++++++++++++
 tests/libc/oracle/fc_libc.2.res.oracle |   1 +
 tests/libc/oracle/fc_libc.5.res.oracle |   1 +
 4 files changed, 112 insertions(+)
 create mode 100644 share/libc/__fc_libc.h

diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4c33aba539b..fefab89f71c 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -204,6 +204,7 @@ share/libc/__fc_define_wint_t.h: CEA_LGPL
 share/libc/__fc_gcc_builtins.h: CEA_LGPL
 share/libc/__fc_inet.h: CEA_LGPL
 share/libc/__fc_integer.h: CEA_LGPL
+share/libc/__fc_libc.h: CEA_LGPL
 share/libc/__fc_machdep.h: CEA_LGPL
 share/libc/__fc_machdep_linux_shared.h: CEA_LGPL
 share/libc/__fc_runtime.c: CEA_LGPL
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
new file mode 100644
index 00000000000..f9677ee2920
--- /dev/null
+++ b/share/libc/__fc_libc.h
@@ -0,0 +1,109 @@
+/**************************************************************************/
+/*                                                                        */
+/*  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).            */
+/*                                                                        */
+/**************************************************************************/
+
+// This file includes all compatible libc/POSIX/BSD headers known by the
+// Frama-C standard library. It is used by some Frama-C scripts.
+
+#define _XOPEN_SOURCE 600
+#define _POSIX_C_SOURCE 200112L
+#define _GNU_SOURCE 1
+
+#include "alloca.h"
+#include "arpa/inet.h"
+#include "assert.h"
+#include "byteswap.h"
+#include "ctype.h"
+#include "dirent.h"
+#include "dlfcn.h"
+#include "endian.h"
+#include "errno.h"
+#include "fcntl.h"
+#include "features.h"
+#include "fenv.h"
+#include "float.h"
+#include "fnmatch.h"
+#include "ftw.h"
+#include "getopt.h"
+#include "glob.h"
+#include "grp.h"
+#include "iconv.h"
+#include "ifaddrs.h"
+#include "inttypes.h"
+#include "iso646.h"
+#include "libgen.h"
+#include "limits.h"
+#include "locale.h"
+#include "malloc.h"
+#include "math.h"
+#include "memory.h"
+#include "netdb.h"
+#include "net/if.h"
+#include "netinet/in.h"
+#include "netinet/ip.h"
+#include "netinet/tcp.h"
+#include "nl_types.h"
+#include "poll.h"
+#include "pthread.h"
+#include "pwd.h"
+#include "regex.h"
+#include "resolv.h"
+#include "sched.h"
+#include "semaphore.h"
+#include "setjmp.h"
+#include "signal.h"
+#include "stdarg.h"
+#include "stdbool.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+#include "stropts.h"
+#include "sys/file.h"
+#include "sys/ioctl.h"
+#include "sys/ipc.h"
+#include "syslog.h"
+#include "sys/mman.h"
+#include "sys/param.h"
+#include "sys/random.h"
+#include "sys/resource.h"
+#include "sys/select.h"
+#include "sys/shm.h"
+#include "sys/signal.h"
+#include "sys/socket.h"
+#include "sys/stat.h"
+#include "sys/time.h"
+#include "sys/times.h"
+#include "sys/timex.h"
+#include "sys/types.h"
+#include "sys/uio.h"
+#include "sys/un.h"
+#include "sys/utsname.h"
+#include "sys/wait.h"
+#include "termios.h"
+#include "time.h"
+#include "unistd.h"
+#include "utime.h"
+#include "utmpx.h"
+#include "wchar.h"
+#include "wctype.h"
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 06372c7bffc..3061c00a626 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -38,6 +38,7 @@
 [kernel] Parsing share/libc/__fc_gcc_builtins.h (with preprocessing)
 [kernel] Parsing share/libc/__fc_inet.h (with preprocessing)
 [kernel] Parsing share/libc/__fc_integer.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_libc.h (with preprocessing)
 [kernel] Parsing share/libc/__fc_machdep.h (with preprocessing)
 skipping share/libc/__fc_machdep_linux_shared.h
 [kernel] Parsing share/libc/__fc_select.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index 73dac90425a..ee4ef42c999 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -1 +1,2 @@
 #include "__fc_integer.h"
+#include "__fc_libc.h"
-- 
GitLab