[Libc] add ftw.h header

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

share/libc/ftw.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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"

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 ======

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;

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)