Merge branch 'fix/libc/stat-missing-errno-codes' into 'master'

[Libc] add a few missing errno codes in stat.h

See merge request frama-c/frama-c!3709

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;

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