From 51d664eaa25fe03fe171dc1cbb43a52e1b863630 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 26 Jul 2024 13:36:02 +0200
Subject: [PATCH] [libc] add non-POSIX, glibc-specific sys/sysmacros.h

---
 share/dune                             |  1 +
 share/libc/__fc_libc.h                 |  1 +
 share/libc/sys/sysmacros.h             | 33 ++++++++++++++++++++++++++
 share/libc/sys/types.h                 |  8 +++----
 tests/libc/fc_libc.c                   |  1 +
 tests/libc/oracle/fc_libc.0.res.oracle |  2 +-
 tests/libc/oracle/fc_libc.2.res.oracle |  1 +
 7 files changed, 41 insertions(+), 6 deletions(-)
 create mode 100644 share/libc/sys/sysmacros.h

diff --git a/share/dune b/share/dune
index 2ae614fc0c6..e7ab88d2f41 100644
--- a/share/dune
+++ b/share/dune
@@ -237,6 +237,7 @@
 (libc/sys/socket.h as libc/sys/socket.h)
 (libc/sys/stat.h as libc/sys/stat.h)
 (libc/sys/statvfs.h as libc/sys/statvfs.h)
+(libc/sys/sysmacros.h as libc/sys/sysmacros.h)
 (libc/sys/time.h as libc/sys/time.h)
 (libc/sys/times.h as libc/sys/times.h)
 (libc/sys/timex.h as libc/sys/timex.h)
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index e03a746b5fd..8157b6347b9 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -111,6 +111,7 @@
 #include "sys/socket.h"
 #include "sys/stat.h"
 #include "sys/statvfs.h"
+#include "sys/sysmacros.h"
 #include "sys/time.h"
 #include "sys/times.h"
 #include "sys/timex.h"
diff --git a/share/libc/sys/sysmacros.h b/share/libc/sys/sysmacros.h
new file mode 100644
index 00000000000..8f590fd9aa6
--- /dev/null
+++ b/share/libc/sys/sysmacros.h
@@ -0,0 +1,33 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2024                                               */
+/*    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).            */
+/*                                                                        */
+/**************************************************************************/
+
+// glibc-specific, Non-POSIX
+
+#ifndef __FC_SYS_SYSMACROS_H__
+#define __FC_SYS_SYSMACROS_H__
+
+// The macros below are useful for coreutils.
+#define major(dev)  (((dev) >> 8) & 0xff)
+#define minor(dev)  ((dev) & 0xff)
+#define makedev(maj, min)  (((maj) << 8) | (min))
+
+#endif
diff --git a/share/libc/sys/types.h b/share/libc/sys/types.h
index 53de26f443e..83a1eaa7967 100644
--- a/share/libc/sys/types.h
+++ b/share/libc/sys/types.h
@@ -50,11 +50,9 @@ typedef unsigned int u_int;
 typedef unsigned short u_short;
 typedef unsigned char u_char;
 
-// The macros below are non-POSIX; the definitions below should allow
-// parsing coreutils.
-# define major(dev)  (((dev) >> 8) & 0xff)
-# define minor(dev)  ((dev) & 0xff)
-# define makedev(maj, min)  (((maj) << 8) | (min))
+// Some glibc versions include major/minor/makedev here, but recently
+// they are in 'sysmacros.h'
+#include "sysmacros.h"
 
 #define __u_char_defined
 #endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 60b769f7041..be77d71504e 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -164,6 +164,7 @@
 #include "sys/socket.h"
 #include "sys/stat.h"
 #include "sys/statvfs.h"
+#include "sys/sysmacros.h"
 #include "sys/time.h"
 #include "sys/times.h"
 #include "sys/timex.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 1c30bf3978c..9753e12ffeb 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/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:205: assertion got status valid.
 [eva] fc_libc.c:206: assertion got status valid.
 [eva] fc_libc.c:207: assertion got status valid.
 [eva] fc_libc.c:208: assertion got status valid.
+[eva] fc_libc.c:209: 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 b8e07f4d510..f4b1572e418 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -129,6 +129,7 @@ skipping FRAMAC_SHARE/libc/complex.h
 [kernel] Parsing FRAMAC_SHARE/libc/sys/socket.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/sys/stat.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/sys/statvfs.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/sys/sysmacros.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/sys/time.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/sys/times.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/libc/sys/timex.h (with preprocessing)
-- 
GitLab