From 4e7e9b311bdfd954037fa858276a73bc5b53e784 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 27 Apr 2020 10:04:10 +0200
Subject: [PATCH] [Libc] add stub for non-POSIX sys/param.h

---
 headers/header_spec.txt                |  1 +
 share/libc/sys/param.h                 | 36 ++++++++++++++++++++++++++
 tests/libc/fc_libc.c                   |  1 +
 tests/libc/oracle/fc_libc.0.res.oracle |  2 +-
 tests/libc/oracle/fc_libc.2.res.oracle |  1 +
 5 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 share/libc/sys/param.h

diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 593ff2ec4ba..90def1eb367 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -279,6 +279,7 @@ share/libc/sys/file.h: CEA_LGPL
 share/libc/sys/ioctl.h: CEA_LGPL
 share/libc/sys/ipc.h: CEA_LGPL
 share/libc/sys/mman.h: CEA_LGPL
+share/libc/sys/param.h: CEA_LGPL
 share/libc/sys/random.h: CEA_LGPL
 share/libc/sys/resource.h: CEA_LGPL
 share/libc/sys/select.h: CEA_LGPL
diff --git a/share/libc/sys/param.h b/share/libc/sys/param.h
new file mode 100644
index 00000000000..a8206b81cd6
--- /dev/null
+++ b/share/libc/sys/param.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2020                                               */
+/*    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).            */
+/*                                                                        */
+/**************************************************************************/
+
+#ifndef __FC_SYS_PARAM_H__
+#define __FC_SYS_PARAM_H__
+#include "../features.h"
+__PUSH_FC_STDLIB
+
+// Note: sys/param.h is not a POSIX file. This is provided as a best-effort
+// basis to support projects using constants such as PATH_MAX, which should
+// be defined in "limits.h" according to POSIX. For instance, in Linux,
+// PATH_MAX is defined in the non-POSIX file linux/limits.h.
+
+#include "../limits.h"
+
+__POP_FC_STDLIB
+#endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index fc52ca5ff0a..db68bcf3adf 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -123,6 +123,7 @@
 #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"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index fefd9fce133..eb8a94e6c73 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/libc/fc_libc.c:153: assertion got status valid.
 [eva] tests/libc/fc_libc.c:154: assertion got status valid.
 [eva] tests/libc/fc_libc.c:155: assertion got status valid.
 [eva] tests/libc/fc_libc.c:156: assertion got status valid.
+[eva] tests/libc/fc_libc.c:157: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index e85ef1cf9e1..4b7f321bdae 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -97,6 +97,7 @@ skipping share/libc/complex.h
 [kernel] Parsing share/libc/sys/ioctl.h (with preprocessing)
 [kernel] Parsing share/libc/sys/ipc.h (with preprocessing)
 [kernel] Parsing share/libc/sys/mman.h (with preprocessing)
+[kernel] Parsing share/libc/sys/param.h (with preprocessing)
 [kernel] Parsing share/libc/sys/random.h (with preprocessing)
 [kernel] Parsing share/libc/sys/resource.h (with preprocessing)
 [kernel] Parsing share/libc/sys/select.h (with preprocessing)
-- 
GitLab