[Libc] add specs and defines for uio.h

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

share/libc/__fc_define_fds.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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

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

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)

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"