diff --git a/share/libc/sys/stat.h b/share/libc/sys/stat.h index 150e072d7569961cb731c7f1ac429f1af282ab2a..3368dd41ccc125d3fe24d36d7ed58c0f5d35ff82 100644 --- a/share/libc/sys/stat.h +++ b/share/libc/sys/stat.h @@ -37,8 +37,9 @@ __BEGIN_DECLS \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}; + __fc_errno \in {EACCES, EINTR, EINVAL, ELOOP, + ENAMETOOLONG, ENOENT, ENOTDIR, EPERM, + EROFS}; ensures result_ok_or_error: \result == 0 || \result == -1; */ extern int chmod(const char *path, mode_t mode); @@ -51,7 +52,7 @@ extern int chmod(const char *path, mode_t mode); 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, + ENAMETOOLONG, ENOENT, ENOTDIR, EOPNOTSUPP, EPERM, EROFS}; ensures result_ok_or_error: \result == 0 || \result == -1; */ @@ -87,7 +88,7 @@ extern int fstat(int fildes, struct stat *buf); \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, + __fc_errno \in {EACCES, EBADF, EINVAL, EIO, ELOOP, ENAMETOOLONG, ENOENT, ENOMEM, ENOTDIR, EOVERFLOW}; ensures result_ok_or_error: \result == 0 || \result == -1; diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index 0da6c52851bceaa477e699fcb919ec7aa5c389ea..b12618051d597aabd339dd8b8be1b42905ffa0fb 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -9370,7 +9370,7 @@ extern int select(int nfds, fd_set *readfds, fd_set *writefds, ensures errno_set: __fc_errno ≡ \old(__fc_errno) ∨ - __fc_errno ∈ {13, 40, 36, 2, 20, 1, 30}; + __fc_errno ∈ {13, 4, 22, 40, 36, 2, 20, 1, 30}; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_errno; assigns \result @@ -9386,7 +9386,7 @@ extern int chmod(char const *path, mode_t mode); ensures errno_set: __fc_errno ≡ \old(__fc_errno) ∨ - __fc_errno ∈ {13, 9, 4, 22, 40, 36, 2, 95, 20, 1, 30}; + __fc_errno ∈ {13, 9, 4, 22, 40, 36, 2, 20, 95, 1, 30}; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_errno; assigns \result @@ -9427,7 +9427,7 @@ extern int fstat(int fildes, struct stat *buf); ensures errno_set: __fc_errno ≡ \old(__fc_errno) ∨ - __fc_errno ∈ {13, 9, 22, 40, 36, 2, 12, 20, 75}; + __fc_errno ∈ {13, 9, 22, 5, 40, 36, 2, 12, 20, 75}; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, *buf, __fc_errno; assigns \result