From 3302fb1d7b55b7999a86d588298cc456fc22131b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 31 Mar 2021 15:21:24 +0200
Subject: [PATCH] [Libc] add header sys/statvfs.h
---
headers/header_spec.txt | 3 ++
share/libc/__fc_define_fs_cnt.h | 38 ++++++++++++++++++
share/libc/sys/statvfs.h | 55 ++++++++++++++++++++++++++
share/libc/sys/vfs.h | 25 ++++++++++++
tests/libc/fc_libc.c | 3 ++
tests/libc/oracle/fc_libc.0.res.oracle | 6 +--
tests/libc/oracle/fc_libc.2.res.oracle | 3 ++
7 files changed, 130 insertions(+), 3 deletions(-)
create mode 100644 share/libc/__fc_define_fs_cnt.h
create mode 100644 share/libc/sys/statvfs.h
create mode 100644 share/libc/sys/vfs.h
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 0a01c138627..7a5d5138ee1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -174,6 +174,7 @@ share/libc/__fc_define_eof.h: CEA_LGPL
share/libc/__fc_define_fd_set_t.h: CEA_LGPL
share/libc/__fc_define_file.h: CEA_LGPL
share/libc/__fc_define_fpos_t.h: CEA_LGPL
+share/libc/__fc_define_fs_cnt.h: CEA_LGPL
share/libc/__fc_define_id_t.h: CEA_LGPL
share/libc/__fc_define_ino_t.h: CEA_LGPL
share/libc/__fc_define_intptr_t.h: CEA_LGPL
@@ -289,6 +290,7 @@ share/libc/sys/shm.h: CEA_LGPL
share/libc/sys/signal.h: CEA_LGPL
share/libc/sys/socket.h: CEA_LGPL
share/libc/sys/stat.h: CEA_LGPL
+share/libc/sys/statvfs.h: CEA_LGPL
share/libc/sys/time.h: CEA_LGPL
share/libc/sys/times.h: CEA_LGPL
share/libc/sys/timex.h: CEA_LGPL
@@ -296,6 +298,7 @@ share/libc/sys/types.h: CEA_LGPL
share/libc/sys/uio.h: CEA_LGPL
share/libc/sys/un.h: CEA_LGPL
share/libc/sys/utsname.h: CEA_LGPL
+share/libc/sys/vfs.h: CEA_LGPL
share/libc/sys/wait.h: CEA_LGPL
share/libc/syslog.h: CEA_LGPL
share/libc/termios.h: CEA_LGPL
diff --git a/share/libc/__fc_define_fs_cnt.h b/share/libc/__fc_define_fs_cnt.h
new file mode 100644
index 00000000000..0ea2e5ebc5e
--- /dev/null
+++ b/share/libc/__fc_define_fs_cnt.h
@@ -0,0 +1,38 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_FS_CNT
+#define __FC_DEFINE_FS_CNT
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+#ifndef __fsblkcnt_t_defined
+typedef unsigned long fsblkcnt_t;
+#define __fsblkcnt_t_defined
+#endif
+#ifndef __fsfilcnt_t_defined
+typedef unsigned long fsfilcnt_t;
+#define __fsfilcnt_t_defined
+#endif
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/sys/statvfs.h b/share/libc/sys/statvfs.h
new file mode 100644
index 00000000000..7a796e4db34
--- /dev/null
+++ b/share/libc/sys/statvfs.h
@@ -0,0 +1,55 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_SYS_STATVFS_H__
+#define __FC_SYS_STATVFS_H__
+
+#include "../features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+
+#include "../__fc_define_fs_cnt.h"
+
+struct statvfs {
+ unsigned long f_bsize; // File system block size.
+ unsigned long f_frsize; // Fundamental file system block size.
+ fsblkcnt_t f_blocks; // Total number of blocks on file system in units of
+ // f_frsize.
+ fsblkcnt_t f_bfree; // Total number of free blocks.
+ fsblkcnt_t f_bavail; // Number of free blocks available to
+ // non-privileged process.
+ fsfilcnt_t f_files; // Total number of file serial numbers.
+ fsfilcnt_t f_ffree; // Total number of free file serial numbers.
+ fsfilcnt_t f_favail; // Number of file serial numbers available to
+ // non-privileged process.
+ unsigned long f_fsid; // File system ID.
+ unsigned long f_flag; // Bit mask of f_flag values.
+ unsigned long f_namemax; // Maximum filename length.
+};
+
+extern int fstatvfs(int fildes, struct statvfs *buf);
+
+extern int statvfs(const char *restrict path, struct statvfs *restrict buf);
+
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/sys/vfs.h b/share/libc/sys/vfs.h
new file mode 100644
index 00000000000..e3620887098
--- /dev/null
+++ b/share/libc/sys/vfs.h
@@ -0,0 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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 is neither in the C standard nor in POSIX;
+// it exists for compatibility purposes
+#include "statvfs.h"
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index a1a67ca9bf4..8563ea2a4ed 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -44,6 +44,7 @@
#include "__fc_define_fd_set_t.h"
#include "__fc_define_file.h"
#include "__fc_define_fpos_t.h"
+#include "__fc_define_fs_cnt.h"
#include "__fc_define_id_t.h"
#include "__fc_define_ino_t.h"
#include "__fc_define_intptr_t.h"
@@ -132,6 +133,7 @@
#include "sys/signal.h"
#include "sys/socket.h"
#include "sys/stat.h"
+#include "sys/statvfs.h"
#include "sys/time.h"
#include "sys/times.h"
#include "sys/timex.h"
@@ -139,6 +141,7 @@
#include "sys/uio.h"
#include "sys/un.h"
#include "sys/utsname.h"
+#include "sys/vfs.h"
#include "sys/wait.h"
#include "termios.h"
#include "tgmath.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 78e6ae2ca53..4bd29442f2a 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -7,10 +7,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[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] tests/libc/fc_libc.c:158: assertion got status valid.
+[eva] tests/libc/fc_libc.c:159: assertion got status valid.
+[eva] tests/libc/fc_libc.c:160: assertion got status valid.
+[eva] tests/libc/fc_libc.c:161: 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 b1e1247a436..06372c7bffc 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -8,6 +8,7 @@
[kernel] Parsing share/libc/__fc_define_fd_set_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_file.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fpos_t.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_define_fs_cnt.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_id_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_ino_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_intptr_t.h (with preprocessing)
@@ -106,6 +107,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/sys/signal.h (with preprocessing)
[kernel] Parsing share/libc/sys/socket.h (with preprocessing)
[kernel] Parsing share/libc/sys/stat.h (with preprocessing)
+[kernel] Parsing share/libc/sys/statvfs.h (with preprocessing)
[kernel] Parsing share/libc/sys/time.h (with preprocessing)
[kernel] Parsing share/libc/sys/times.h (with preprocessing)
[kernel] Parsing share/libc/sys/timex.h (with preprocessing)
@@ -113,6 +115,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/sys/uio.h (with preprocessing)
[kernel] Parsing share/libc/sys/un.h (with preprocessing)
[kernel] Parsing share/libc/sys/utsname.h (with preprocessing)
+[kernel] Parsing share/libc/sys/vfs.h (with preprocessing)
[kernel] Parsing share/libc/sys/wait.h (with preprocessing)
[kernel] Parsing share/libc/syslog.h (with preprocessing)
[kernel] Parsing share/libc/termios.h (with preprocessing)
--
GitLab