[Libc] use stronger assigns clause for readv

share/libc/sys/uio.h

@@ -33,20 +33,20 @@ __PUSH_FC_STDLIB
 
 __BEGIN_DECLS
 
-// 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 initialization:initialized_inputs:
      \forall integer i; 0 <= i < iovcnt ==>
     \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
   requires valid_iov: \forall integer i; 0 <= i < iovcnt ==>
-    \valid( ((char*)&iov[i].iov_base)+(0..iov[i].iov_len-1));
+    \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..],
+  assigns { ((char*)iov[i].iov_base)[j] |
+            integer i, j; 0 <= i < iovcnt && 0 <= j < iov[i].iov_len }
+    \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);
@@ -58,15 +58,15 @@ extern ssize_t readv(int fd, const struct iovec *iov, int iovcnt);
   requires initialization:initialized_inputs:
     \forall integer i; 0 <= i < iovcnt ==>
     \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
-  requires valid_read_iov: \valid_read(&iov[0..iovcnt-1]);
+  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..],
+     \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;
+  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);
+          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);
 

tests/libc/oracle/fc_libc.1.res.oracle

@@ -4538,8 +4538,12 @@ extern int killpg(pid_t pgrp, int sig);
         \result ≡ -1 ∨
         (0 ≤ \result ≤
          \sum(0, \old(iovcnt) - 1, \lambda ℤ k; (\old(iov) + k)->iov_len));
-    assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..)), \result;
-    assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..))
+    assigns {*((char *)(iov + i)->iov_base + j) |
+             ℤ i, ℤ j; 0 ≤ i < iovcnt ∧ 0 ≤ j < (iov + i)->iov_len},
+            \result;
+    assigns
+    {*((char *)(iov + i)->iov_base + j) |
+     ℤ i, ℤ j; 0 ≤ i < iovcnt ∧ 0 ≤ j < (iov + i)->iov_len}
       \from (indirect: fd), (indirect: iovcnt), (indirect: __fc_fds[fd]);
     assigns \result
       \from (indirect: fd), (indirect: __fc_fds[fd]),