[libc] Add futimes, futimens and utimensat

share/libc/__fc_define_at.h

+/**************************************************************************/
+/*                                                                        */
+/*  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).            */
+/*                                                                        */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_AT
+#define __FC_DEFINE_AT
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+
+#define AT_FDCWD -100
+#define AT_EACCESS 0x200
+#define AT_SYMLINK_NOFOLLOW 0x100
+#define AT_SYMLINK_FOLLOW 0x400
+#define AT_REMOVEDIR 0x200
+
+// Non-POSIX (GNU extensions)
+#define AT_EMPTY_PATH 0x1000
+#define AT_RECURSIVE 0x8000
+#define AT_STATX_DONT_SYNC 0x4000
+#define AT_STATX_FORCE_SYNC 0x2000
+#define AT_STATX_SYNC_AS_STAT 0x0000
+#define AT_STATX_SYNC_TYPE 0x6000
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif // __FC_DEFINE_AT

share/libc/__fc_define_fds.h

@@ -26,10 +26,7 @@
 __PUSH_FC_STDLIB
 __BEGIN_DECLS
 
-// arbitrary number
-#ifndef __FC_MAX_OPEN_FILES
-#define __FC_MAX_OPEN_FILES 1024
-#endif
+#include "__fc_define_max_open_files.h"
 
 // __fc_fds represents the state of open file descriptors.
 extern volatile int __fc_fds[__FC_MAX_OPEN_FILES];

share/libc/fcntl.h

@@ -25,6 +25,7 @@
 #include "features.h"
 __PUSH_FC_STDLIB
 
+#include "__fc_define_at.h"
 #include "__fc_define_off_t.h"
 #include "__fc_define_pid_t.h"
 #include "__fc_define_mode_t.h"
@@ -83,20 +84,6 @@ __PUSH_FC_STDLIB
 //#define O_SEARCH
 #define O_WRONLY 1
 
-#define AT_FDCWD -100
-#define AT_EACCESS 0x200
-#define AT_SYMLINK_NOFOLLOW 0x100
-#define AT_SYMLINK_FOLLOW 0x400
-#define AT_REMOVEDIR 0x200
-
-// Non-POSIX (GNU extensions)
-#define AT_EMPTY_PATH 0x1000
-#define AT_RECURSIVE 0x8000
-#define AT_STATX_DONT_SYNC 0x4000
-#define AT_STATX_FORCE_SYNC 0x2000
-#define AT_STATX_SYNC_AS_STAT 0x0000
-#define AT_STATX_SYNC_TYPE 0x6000
-
 #define POSIX_FADV_DONTNEED 4
 #define POSIX_FADV_NOREUSE 5
 #define POSIX_FADV_NORMAL 0
@@ -159,7 +146,7 @@ extern int __va_fcntl_int(int fd, int cmd, int arg);
 
 /*@ requires cmd_as_flock_arg: cmd == F_GETLK || cmd == F_SETLK ||
                         cmd == F_SETLKW ;
-    requires valid_arg: \valid(arg) ; 
+    requires valid_arg: \valid(arg) ;
     assigns \result, *arg \from fd, cmd, *arg ; */
 extern int __va_fcntl_flock(int fd, int cmd, struct flock *arg);
 

share/libc/sys/stat.h

@@ -26,8 +26,11 @@
 __PUSH_FC_STDLIB
 __BEGIN_DECLS
 
+#include "../__fc_define_at.h"
 #include "../__fc_define_stat.h"
 #include "../__fc_string_axiomatic.h"
+#include "../__fc_define_fds.h"
+#include "../__fc_define_timespec.h"
 #include "../errno.h"
 
 /*@
@@ -159,6 +162,40 @@ extern int    stat(const char *pathname, struct stat *buf);
 */
 extern mode_t umask(mode_t cmask);
 
+/*@ //missing: assigns 'filesystem' \from ...
+  requires valid_fd: dirfd == AT_FDCWD || 0 <= dirfd < __FC_MAX_OPEN_FILES;
+  requires valid_string_path: valid_read_string(path);
+  requires valid_flags: (flags & ~(AT_EMPTY_PATH | AT_SYMLINK_NOFOLLOW)) == 0 ||
+                        flags == 0;
+  requires valid_times_or_null:
+    \valid_read(times+(0 .. 1)) || times == \null;
+  requires initialized_times_or_null:initialization:
+    \initialized(times+(0 .. 1)) || times == \null;
+  assigns \result \from indirect:dirfd, indirect:path, indirect:path[0..],
+                        indirect:times, indirect:times[0..], indirect:flags;
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EACCES, EBADF, EFAULT, EINVAL, ELOOP,
+                                     ENAMETOOLONG, ENOENT, ENOTDIR, EPERM,
+                                     EROFS, ESRCH};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int utimensat(int dirfd, const char *path,
+                     const struct timespec times[2], int flags);
+
+/*@ //missing: assigns 'filesystem' \from ...
+  requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+  requires valid_times_or_null:
+    \valid_read(times+(0 .. 1)) || times == \null;
+  requires initialized_times_or_null:initialization:
+    \initialized(times+(0 .. 1)) || times == \null;
+  assigns \result \from indirect:fd, indirect:times, indirect:times[0..];
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EACCES, EBADF, EFAULT, EINVAL, EPERM,
+                                     EROFS};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int futimens(int fd, const struct timespec times[2]);
+
 #define S_TYPEISMQ(buf) ((buf)->st_mode - (buf)->st_mode)
 #define S_TYPEISSEM(buf) ((buf)->st_mode - (buf)->st_mode)
 #define S_TYPEISSHM(buf) ((buf)->st_mode - (buf)->st_mode)

share/libc/sys/time.h

@@ -25,6 +25,7 @@
 #include "../features.h"
 __PUSH_FC_STDLIB
 #include "../__fc_define_fd_set_t.h"
+#include "../__fc_define_max_open_files.h"
 #include "../__fc_define_suseconds_t.h"
 #include "../__fc_define_time_t.h"
 #include "../__fc_define_timeval.h"
@@ -43,11 +44,23 @@ struct timezone {
 /*@
   requires valid_path: valid_read_string(path);
   requires valid_times_or_null: \valid_read(times+(0..1)) || times == \null;
+  requires intialized_times_or_null:initialization:
+    \initialized(times+(0..1)) || times == \null;
   assigns \result \from indirect:path[0..strlen(path)],
     indirect:times, indirect:times[0..1];
 */
 extern int utimes(const char *path, const struct timeval times[2]);
 
+/*@ //missing: assigns 'filesystem' \from ...
+    //missing: errno
+  requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+  requires valid_times_or_null: \valid_read(times+(0..1)) || times == \null;
+  requires intialized_times_or_null:initialization:
+    \initialized(times+(0..1)) || times == \null;
+  assigns \result \from indirect:fd, indirect:times, indirect:times[0..1];
+*/
+extern int futimes(int fd, const struct timeval times[2]);
+
 /*@ assigns tv->tv_sec, tv->tv_usec \from __fc_time;
   @ assigns *(struct timezone *)tz \from __fc_tz;
   @ assigns \result \from indirect:tv, indirect:tz, *tv, *(struct timezone *)tz, __fc_tz;

tests/libc/fc_libc.c

@@ -48,6 +48,7 @@
 #include "error.h"
 #include "__fc_alloc_axiomatic.h"
 #include "__fc_builtin.h"
+#include "__fc_define_at.h"
 #include "__fc_define_blkcnt_t.h"
 #include "__fc_define_blksize_t.h"
 #include "__fc_define_clockid_t.h"