diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 81ea66623889de33690c7d2cfd92aa261053deb6..d5a4550ba8159849c07a08e303f297b9fe1a6c20 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -180,6 +180,7 @@ share/libc/__fc_define_clockid_t.h: CEA_LGPL
share/libc/__fc_define_dev_t.h: CEA_LGPL
share/libc/__fc_define_eof.h: CEA_LGPL
share/libc/__fc_define_fd_set_t.h: CEA_LGPL
+share/libc/__fc_define_fds.h: CEA_LGPL
share/libc/__fc_define_file.h: CEA_LGPL
share/libc/__fc_define_fpos_t.h: CEA_LGPL
share/libc/__fc_define_fs_cnt.h: CEA_LGPL
diff --git a/share/libc/__fc_define_fds.h b/share/libc/__fc_define_fds.h
new file mode 100644
index 0000000000000000000000000000000000000000..6905aad49acb612be5e77082bcd23d64356053a9
--- /dev/null
+++ b/share/libc/__fc_define_fds.h
@@ -0,0 +1,40 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* 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_FDS
+#define __FC_DEFINE_FDS
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+
+// arbitrary number
+#ifndef __FC_MAX_OPEN_FILES
+#define __FC_MAX_OPEN_FILES 1024
+#endif
+
+// __fc_fds represents the state of open file descriptors.
+extern volatile int __fc_fds[__FC_MAX_OPEN_FILES];
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/limits.h b/share/libc/limits.h
index be32d497acd2883f59ef9096978290932287fc37..7c19508f17883e2954384f61b9d79f6ca228440a 100644
--- a/share/libc/limits.h
+++ b/share/libc/limits.h
@@ -95,4 +95,9 @@
*/
#define ARG_MAX 4096
+// POSIX; used by <sys/uio.h>.
+// Must be >= _XOPEN_IOV_MAX, which is 16.
+// 1024 is the value used by some Linux implementations.
+#define IOV_MAX 1024
+
#endif
diff --git a/share/libc/sys/uio.h b/share/libc/sys/uio.h
index 7ef6ce26a73b7c58c36a3413b228658349faa9ff..93f33eeded29c84d9d6aa548a8980efeca066171 100644
--- a/share/libc/sys/uio.h
+++ b/share/libc/sys/uio.h
@@ -28,15 +28,40 @@ __PUSH_FC_STDLIB
#include "../__fc_define_ssize_t.h"
#include "../__fc_define_size_t.h"
#include "../__fc_define_iovec.h"
+#include "../__fc_define_fds.h"
+#include "../limits.h"
__BEGIN_DECLS
-/*@ requires valid_read_iov: \valid_read( &iov[0..iovcnt-1] );
-// Value cannot yet interpret the precise assigns clause; we use the weaker one as a fallback.
-//@ assigns { ((char *) iov[i].iov_base)[0..iov[i].iov_len - 1] | integer i; 0 <= i < iovcnt };
- @ assigns ((char *) iov[0..iovcnt -1].iov_base)[0..];
+// Frama-C cannot yet interpret the precise assigns clause;
+// we use the weaker one as a fallback.
+// assigns { ((char *) iov[i].iov_base)[0..iov[i].iov_len - 1] | integer i; 0 <= i < iovcnt };
+/*@
+ requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+ requires valid_iov: \forall integer i; 0 <= i < iovcnt ==>
+ \valid( ((char*)&iov[i].iov_base)+(0..iov[i].iov_len-1));
+ requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
+ assigns ((char *)iov[0..iovcnt-1].iov_base)[0..] \from indirect:fd,
+ indirect:iovcnt, indirect:__fc_fds[fd];
+ assigns \result \from indirect:fd, indirect:__fc_fds[fd], indirect:iov[0..],
+ indirect:iovcnt;
+ ensures result_error_or_read_bytes: \result == -1 ||
+ 0 <= \result <= \sum(0,iovcnt-1, \lambda integer k; iov[k].iov_len);
*/
extern ssize_t readv(int fd, const struct iovec *iov, int iovcnt);
+
+/*@
+ requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+ requires valid_read_iov: \valid_read(&iov[0..iovcnt-1]);
+ requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
+ requires bounded_lengths:
+ \sum(0,iovcnt-1, \lambda integer k; iov[k].iov_len) <= SSIZE_MAX;
+ assigns \result \from indirect:fd, indirect:__fc_fds[fd], indirect:iov[0..],
+ indirect:iovcnt;
+ assigns __fc_fds[fd] \from indirect:iov[0..], indirect:iovcnt;
+ ensures result_error_or_written_bytes: \result == -1 ||
+ 0 <= \result <= \sum(0,iovcnt-1, \lambda integer k; iov[k].iov_len);
+ */
extern ssize_t writev(int fd, const struct iovec *iov, int iovcnt);
__END_DECLS
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index a8c71c4da66bfde812e77250d56ab9b6192509b8..916d67d1a3a8bd10fbebc9ecfa91aca92b56c834 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -35,7 +35,8 @@ __PUSH_FC_STDLIB
#include "__fc_define_pid_t.h"
#include "__fc_define_useconds_t.h"
#include "__fc_define_intptr_t.h"
-
+#include "__fc_define_fds.h"
+#include "__fc_select.h"
#include "limits.h"
@@ -722,16 +723,6 @@ enum __fc_confstr_name
#define _CS_V7_ENV _CS_V7_ENV
};
-
-// arbitrary number
-#define __FC_MAX_OPEN_FILES 1024
-
-// __fc_fds represents the state of open file descriptors.
-//@ ghost int __fc_fds[__FC_MAX_OPEN_FILES];
-// TODO: Model the state of some functions more precisely.
-// TODO: define __fc_fds as volatile.
-
-
/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG, ENOENT,
// ENOTDIR, EROFS, ETXTBSY
// (EINVAL prevented by precondition)
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 1345145e950c37a80e559c9426ab5a2ce0dc968e..bc77198c9b7df50e50eca7e5a477ae2e1c0bac45 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -44,6 +44,7 @@
#include "__fc_define_dev_t.h"
#include "__fc_define_eof.h"
#include "__fc_define_fd_set_t.h"
+#include "__fc_define_fds.h"
#include "__fc_define_file.h"
#include "__fc_define_fpos_t.h"
#include "__fc_define_fs_cnt.h"