From da849fce18a713950c61dcd80d509f00a4eb4a17 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 18 Jul 2019 18:55:16 +0200
Subject: [PATCH] [Libc] add ftw.h header
---
headers/header_spec.txt | 1 +
share/libc/ftw.h | 80 ++++++++++++++++++++++++++
tests/libc/fc_libc.c | 1 +
tests/libc/oracle/fc_libc.0.res.oracle | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 48 ++++++++--------
tests/libc/oracle/fc_libc.2.res.oracle | 1 +
6 files changed, 108 insertions(+), 25 deletions(-)
create mode 100644 share/libc/ftw.h
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3122754828c..08eb5d8ee17 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -222,6 +222,7 @@ share/libc/fenv.h: CEA_LGPL
share/libc/fenv.c: CEA_LGPL
share/libc/float.h: CEA_LGPL
share/libc/fnmatch.h: CEA_LGPL
+share/libc/ftw.h: CEA_LGPL
share/libc/getopt.c: CEA_LGPL
share/libc/getopt.h: CEA_LGPL
share/libc/glob.c: CEA_LGPL
diff --git a/share/libc/ftw.h b/share/libc/ftw.h
new file mode 100644
index 00000000000..f1e1645f860
--- /dev/null
+++ b/share/libc/ftw.h
@@ -0,0 +1,80 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2019 */
+/* 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_FTW
+#define __FC_FTW
+#include "features.h"
+__PUSH_FC_STDLIB
+
+__BEGIN_DECLS
+
+struct FTW
+{
+ int base;
+ int level;
+};
+
+enum __fc_ftw
+{
+ FTW_F,
+#define FTW_F FTW_F
+ FTW_D,
+#define FTW_D FTW_D
+ FTW_DNR,
+#define FTW_DNR FTW_DNR
+ FTW_DP,
+#define FTW_DP FTW_DP
+ FTW_NS,
+#define FTW_NS FTW_NS
+ FTW_SL,
+#define FTW_SL FTW_SL
+ FTW_SLN,
+#define FTW_SLN FTW_SLN
+};
+
+enum __fc_nftw
+{
+ NFTW_PHYS,
+#define NFTW_PHYS NFTW_PHYS
+ NFTW_MOUNT,
+#define NFTW_MOUNT NFTW_MOUNT
+ NFTW_DEPTH,
+#define NFTW_DEPTH NFTW_DEPTH
+ NFTW_CHDIR,
+#define NFTW_CHDIR NFTW_CHDIR
+};
+
+// From POSIX 1.2008: "Inclusion of the <ftw.h> header may also make visible
+// all symbols from <sys/stat.h>".
+#include "sys/stat.h"
+
+int ftw(const char *path,
+ int (*fn)(const char *, const struct stat *ptr, int flag), int ndirs);
+
+int nftw(const char *path,
+ int (*fn)(const char *, const struct stat *, int, struct FTW *),
+ int fd_limit, int flags);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 7f19d6c406a..3baf405b459 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -77,6 +77,7 @@
#include "fenv.h"
#include "float.h"
#include "fnmatch.h"
+#include "ftw.h"
#include "getopt.h"
#include "glob.h"
#include "grp.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 9077994133d..37633dcd6d3 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:148: assertion got status valid.
[eva] tests/libc/fc_libc.c:149: assertion got status valid.
[eva] tests/libc/fc_libc.c:150: assertion got status valid.
[eva] tests/libc/fc_libc.c:151: assertion got status valid.
+[eva] tests/libc/fc_libc.c:152: 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.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8d9222bf040..97573852495 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6867,6 +6867,30 @@ extern int setitimer(int which,
extern int select(int nfds, fd_set *readfds, fd_set *writefds,
fd_set *errorfds, struct timeval *timeout);
+/*@ requires valid_string_path: valid_read_string(path);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: mode);
+ */
+extern int mkdir(char const *path, mode_t mode);
+
+/*@ requires valid_pathname: valid_read_string(pathname);
+ requires valid_buf: \valid(buf);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ ensures
+ init_on_success: initialization: buf:
+ \result ≡ 0 ⇒ \initialized(\old(buf));
+ assigns \result, *buf;
+ assigns \result \from *(pathname + (0 ..));
+ assigns *buf \from *(pathname + (0 ..));
+ */
+extern int stat(char const *pathname, struct stat *buf);
+
+/*@ assigns \result;
+ assigns \result \from (indirect: cmask); */
+extern mode_t umask(mode_t cmask);
+
/*@ assigns *(*(outbuf + (0 .. *outbytesleft - 1))), __fc_errno;
assigns *(*(outbuf + (0 .. *outbytesleft - 1)))
\from *(*(inbuf + (0 .. *inbytesleft - 1)));
@@ -7198,30 +7222,6 @@ extern int getrusage(int r, struct rusage *ru);
assigns \result \from r, rl->rlim_cur, rl->rlim_max; */
extern int setrlimit(int r, struct rlimit const *rl);
-/*@ requires valid_string_path: valid_read_string(path);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result
- \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: mode);
- */
-extern int mkdir(char const *path, mode_t mode);
-
-/*@ requires valid_pathname: valid_read_string(pathname);
- requires valid_buf: \valid(buf);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- ensures
- init_on_success: initialization: buf:
- \result ≡ 0 ⇒ \initialized(\old(buf));
- assigns \result, *buf;
- assigns \result \from *(pathname + (0 ..));
- assigns *buf \from *(pathname + (0 ..));
- */
-extern int stat(char const *pathname, struct stat *buf);
-
-/*@ assigns \result;
- assigns \result \from (indirect: cmask); */
-extern mode_t umask(mode_t cmask);
-
/*@ requires valid_buffer: \valid(buffer);
assigns \result, *buffer;
assigns \result \from __fc_time;
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 6650a34b1f8..fc16d42e535 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -55,6 +55,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/fenv.h (with preprocessing)
[kernel] Parsing share/libc/float.h (with preprocessing)
[kernel] Parsing share/libc/fnmatch.h (with preprocessing)
+[kernel] Parsing share/libc/ftw.h (with preprocessing)
[kernel] Parsing share/libc/getopt.h (with preprocessing)
[kernel] Parsing share/libc/glob.h (with preprocessing)
[kernel] Parsing share/libc/grp.h (with preprocessing)
--
GitLab