diff --git a/share/libc/sys/stat.h b/share/libc/sys/stat.h
index b2deabaa9cae10a03be9003e0c3fb8aff4c61f48..cefb3fa30037e4b1674ee5a59d2f5e752f3b31de 100644
--- a/share/libc/sys/stat.h
+++ b/share/libc/sys/stat.h
@@ -28,13 +28,72 @@ __BEGIN_DECLS
#include "../__fc_define_stat.h"
#include "../__fc_string_axiomatic.h"
+#include "../errno.h"
-extern int chmod(const char *, mode_t);
-extern int fchmodat(int fd, const char *path, mode_t mode, int flag);
-extern int fchmod(int, mode_t);
-extern int fstat(int, struct stat *);
-extern int fstatat(int fd, const char *restrict path,
- struct stat *restrict buf, int flag);
+/*@
+ // missing: assigns 'filesystem' \frompath, path[0..], mode;
+ requires valid_path: valid_read_string(path);
+ assigns \result, __fc_errno
+ \from indirect:path, indirect:path[0 .. strlen(path)],
+ indirect:mode; //missing: \from 'filesystem'
+ ensures errno_set: __fc_errno == \old(__fc_errno) ||
+ __fc_errno \in {EACCES, ELOOP, ENAMETOOLONG, ENOENT,
+ ENOTDIR, EPERM, EROFS};
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int chmod(const char *path, mode_t mode);
+
+/*@
+ // missing: assigns 'filesystem' \from fd, path, path[0..], mode, flag;
+ requires valid_path: valid_read_string(path);
+ assigns \result, __fc_errno
+ \from indirect:fd, indirect:path, indirect:path[0 .. strlen(path)],
+ indirect:mode, indirect:flag; //missing: \from 'filesystem'
+ ensures errno_set: __fc_errno == \old(__fc_errno) ||
+ __fc_errno \in {EACCES, EBADF, EINTR, EINVAL, ELOOP,
+ ENAMETOOLONG, ENOENT, EOPNOTSUPP, ENOTDIR,
+ EPERM, EROFS};
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fchmodat(int fd, const char *path, mode_t mode, int flag);
+
+/*@
+ // missing: assigns 'filesystem' \from fildes, mode;
+ assigns \result, __fc_errno
+ \from indirect:fildes, indirect:mode; //missing: \from 'filesystem'
+ ensures errno_set: __fc_errno == \old(__fc_errno) ||
+ __fc_errno \in {EBADF, EINTR, EINVAL, EPERM, EROFS};
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fchmod(int fildes, mode_t mode);
+
+/*@
+ //TODO: define proper initialization postcondition; it involves only a few
+ // specific fields, and only a few bits within those fields.
+ requires valid_buf: \valid(buf);
+ assigns \result, *buf, __fc_errno
+ \from indirect:fildes; //missing: \from 'filesystem'
+ ensures errno_set: __fc_errno == \old(__fc_errno) ||
+ __fc_errno \in {EBADF, EIO, EOVERFLOW};
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fstat(int fildes, struct stat *buf);
+
+/*@
+ // missing: assigns 'filesystem' \from fd, path, path[0..], flag;
+ requires valid_path: valid_read_string(path);
+ requires valid_buf: \valid(buf);
+ assigns \result, *buf, __fc_errno
+ \from indirect:fd, indirect:path, indirect:path[0 .. strlen(path)],
+ indirect:flag; //missing: \from 'filesystem'
+ ensures errno_set: __fc_errno == \old(__fc_errno) ||
+ __fc_errno \in {EACCES, EBADF, EINVAL, ELOOP,
+ ENAMETOOLONG, ENOENT, ENOMEM, ENOTDIR,
+ EOVERFLOW};
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fstatat(int fd, const char *restrict path,
+ struct stat *restrict buf, int flag);
/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG,
// ENOENT, ENOMEM, ENOTDIR, EOVERFLOW,
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index d01d8094eec109f870f833fb1f9140852bfffcfd..3fb04d0fb90cbc7e4aa584185168bf39a6da368d 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8979,6 +8979,83 @@ extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
extern int select(int nfds, fd_set *readfds, fd_set *writefds,
fd_set *errorfds, struct timeval *timeout);
+/*@ requires valid_path: valid_read_string(path);
+ ensures
+ errno_set:
+ __fc_errno ≡ \old(__fc_errno) ∨
+ __fc_errno ∈ {13, 40, 36, 2, 20, 1, 30};
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, __fc_errno;
+ assigns \result
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: mode);
+ assigns __fc_errno
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: mode);
+ */
+extern int chmod(char const *path, mode_t mode);
+
+/*@ requires valid_path: valid_read_string(path);
+ ensures
+ errno_set:
+ __fc_errno ≡ \old(__fc_errno) ∨
+ __fc_errno ∈ {13, 9, 4, 22, 40, 36, 2, 95, 20, 1, 30};
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, __fc_errno;
+ assigns \result
+ \from (indirect: fd), (indirect: path),
+ (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: mode),
+ (indirect: flag);
+ assigns __fc_errno
+ \from (indirect: fd), (indirect: path),
+ (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: mode),
+ (indirect: flag);
+ */
+extern int fchmodat(int fd, char const *path, mode_t mode, int flag);
+
+/*@ ensures
+ errno_set:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ∈ {9, 4, 22, 1, 30};
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: fildes), (indirect: mode);
+ assigns __fc_errno \from (indirect: fildes), (indirect: mode);
+ */
+extern int fchmod(int fildes, mode_t mode);
+
+/*@ requires valid_buf: \valid(buf);
+ ensures
+ errno_set:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ∈ {9, 5, 75};
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, *buf, __fc_errno;
+ assigns \result \from (indirect: fildes);
+ assigns *buf \from (indirect: fildes);
+ assigns __fc_errno \from (indirect: fildes);
+ */
+extern int fstat(int fildes, struct stat *buf);
+
+/*@ requires valid_path: valid_read_string(path);
+ requires valid_buf: \valid(buf);
+ ensures
+ errno_set:
+ __fc_errno ≡ \old(__fc_errno) ∨
+ __fc_errno ∈ {13, 9, 22, 40, 36, 2, 12, 20, 75};
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, *buf, __fc_errno;
+ assigns \result
+ \from (indirect: fd), (indirect: path),
+ (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: flag);
+ assigns *buf
+ \from (indirect: fd), (indirect: path),
+ (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: flag);
+ assigns __fc_errno
+ \from (indirect: fd), (indirect: path),
+ (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: flag);
+ */
+extern int fstatat(int fd, char const * restrict path,
+ struct stat * restrict buf, int flag);
+
/*@ requires valid_path: valid_read_string(path);
requires valid_buf: \valid(buf);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
diff --git a/tests/libc/oracle/sys_stat_h.res.oracle b/tests/libc/oracle/sys_stat_h.res.oracle
index fe5efe7073c7422ba45150f3b323bc271c4c6e76..edb2f90be28452d72fa2645a8b131995f355ded9 100644
--- a/tests/libc/oracle/sys_stat_h.res.oracle
+++ b/tests/libc/oracle/sys_stat_h.res.oracle
@@ -69,10 +69,47 @@
[eva] computing for function mknod <- main.
Called from sys_stat_h.c:25.
[eva] Done for function mknod
+[eva] computing for function chmod <- main.
+ Called from sys_stat_h.c:27.
+[eva] using specification for function chmod
+[eva] sys_stat_h.c:27:
+ function chmod: precondition 'valid_path' got status valid.
+[eva] Done for function chmod
+[eva] computing for function fchmod <- main.
+ Called from sys_stat_h.c:29.
+[eva] using specification for function fchmod
+[eva] Done for function fchmod
+[eva] computing for function fchmod <- main.
+ Called from sys_stat_h.c:29.
+[eva] Done for function fchmod
+[eva] computing for function fchmodat <- main.
+ Called from sys_stat_h.c:31.
+[eva] using specification for function fchmodat
+[eva] sys_stat_h.c:31:
+ function fchmodat: precondition 'valid_path' got status valid.
+[eva] Done for function fchmodat
+[eva] computing for function fstat <- main.
+ Called from sys_stat_h.c:35.
+[eva] using specification for function fstat
+[eva] sys_stat_h.c:35:
+ function fstat: precondition 'valid_buf' got status valid.
+[eva] Done for function fstat
+[eva] computing for function fstat <- main.
+ Called from sys_stat_h.c:35.
+[eva] Done for function fstat
+[eva] computing for function fstatat <- main.
+ Called from sys_stat_h.c:37.
+[eva] using specification for function fstatat
+[eva] sys_stat_h.c:37:
+ function fstatat: precondition 'valid_path' got status valid.
+[eva] sys_stat_h.c:37:
+ function fstatat: precondition 'valid_buf' got status valid.
+[eva] Done for function fstatat
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
__fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
st ∈ [--..--] or UNINITIALIZED
@@ -82,4 +119,10 @@
r2 ∈ {-1; 0}
r3 ∈ {-1; 0}
r4 ∈ {-1; 0}
+ r5 ∈ {-1; 0}
+ r6 ∈ {-1; 0}
+ r7 ∈ {-1; 0}
+ buf ∈ [--..--] or UNINITIALIZED
+ r8 ∈ {-1; 0}
+ r9 ∈ {-1; 0}
__retres ∈ {-1; 0; 1; 2; 3}
diff --git a/tests/libc/sys_stat_h.c b/tests/libc/sys_stat_h.c
index 24a4b3335118005af0fc3e28cfd303f9d32a1b7e..deefde5a31fcb34f71f2ac0dfc20d33f7c0d5c53 100644
--- a/tests/libc/sys_stat_h.c
+++ b/tests/libc/sys_stat_h.c
@@ -23,5 +23,18 @@ int main() {
int r2 = lstat("/tmp/bla", &st);
int r3 = mkfifo("/tmp/fifo", 0644);
int r4 = mknod("/tmp/fifo2", 0644, 42);
+
+ int r5 = chmod("/tmp/bla", 0700);
+
+ int r6 = fchmod(fd, 0700);
+
+ int r7 = fchmodat(AT_FDCWD, "bla", 0700, AT_SYMLINK_NOFOLLOW);
+
+ struct stat buf;
+
+ int r8 = fstat(fd, &buf);
+
+ int r9 = fstatat(AT_FDCWD, "bla", &buf, AT_SYMLINK_NOFOLLOW);
+
return 0;
}