diff --git a/share/dune b/share/dune index 2ae614fc0c6e23b920743c499ff5d3336e61178f..e7ab88d2f418b70fb4584b78a7bd9c3847aa6271 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 e03a746b5fd93c7b7517d16d025179d308bf1694..8157b6347b9d8499ae41e55132d1363b6b7b480f 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 0000000000000000000000000000000000000000..8f590fd9aa6fab278f9aba5bbf058ca60b2baa6f --- /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 53de26f443e307634d9a4085ad6c3f52263bbe8c..83a1eaa7967024f96252d333e42adfd15d07fe33 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 60b769f70410851d5fa574a39919776fef2f28e1..be77d71504e012469455a694b74938066c4de302 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 1c30bf3978c0942907017a876cba68216a01456d..9753e12ffebb6769813519d2da15a91fd2e5520c 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 b8e07f4d5104574e045c2d0751cfc89acda935f0..f4b1572e418b5308dc78d9bdcfb09af9413e108a 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)