diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 81ea66623889de33690c7d2cfd92aa261053deb6..23e24fa4d73ef6939753a9a7177bc6a8b73f3708 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
@@ -206,6 +207,7 @@ share/libc/__fc_define_suseconds_t.h: CEA_LGPL
share/libc/__fc_define_time_t.h: CEA_LGPL
share/libc/__fc_define_timer_t.h: CEA_LGPL
share/libc/__fc_define_timespec.h: CEA_LGPL
+share/libc/__fc_define_timeval.h: CEA_LGPL
share/libc/__fc_define_uid_and_gid.h: CEA_LGPL
share/libc/__fc_define_useconds_t.h: CEA_LGPL
share/libc/__fc_define_wchar_t.h: CEA_LGPL
diff --git a/share/libc/__fc_define_fd_set_t.h b/share/libc/__fc_define_fd_set_t.h
index 5f9b7c721b2124a2158961a07c7db38eda5506e3..5e6bbe0272593c03712707a3966a0cd086f32250 100644
--- a/share/libc/__fc_define_fd_set_t.h
+++ b/share/libc/__fc_define_fd_set_t.h
@@ -29,40 +29,6 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
typedef struct __fc_fd_set { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
-/*@
- requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_CLR(int fd, fd_set *fdset);
-#define FD_CLR FD_CLR
-
-// Note: the 2nd argument in FD_ISSET is not const in some implementations
-// due to historical and compatibility reasons.
-/*@
- requires valid_fdset: \valid_read(fdset);
- requires initialization: \initialized(fdset);
- assigns \result \from indirect:*fdset, indirect:fd;
-*/
-extern int FD_ISSET(int fd, const fd_set *fdset);
-#define FD_ISSET FD_ISSET
-
-/*@
- requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_SET(int fd, fd_set *fdset);
-#define FD_SET FD_SET
-
-/*@
- requires valid_fdset: \valid(fdset);
- assigns *fdset \from \nothing;
- ensures initialization: \initialized(fdset);
-*/
-extern void FD_ZERO(fd_set *fdset);
-#define FD_ZERO FD_ZERO
-
__END_DECLS
__POP_FC_STDLIB
#endif
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/__fc_define_timeval.h b/share/libc/__fc_define_timeval.h
new file mode 100644
index 0000000000000000000000000000000000000000..34db8894a582b2e7a28779182505194efadaed79
--- /dev/null
+++ b/share/libc/__fc_define_timeval.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* 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_TIMEVAL
+#define __FC_DEFINE_TIMEVAL
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+#include "__fc_define_suseconds_t.h"
+#include "__fc_define_time_t.h"
+struct timeval {
+ time_t tv_sec;
+ suseconds_t tv_usec;
+};
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/__fc_select.h b/share/libc/__fc_select.h
index 4fc0f3b0aa6e161a24d6daefa686adb5e5223392..1fad5956e876ce077f8db6bfccda7db5ddd8c7d4 100644
--- a/share/libc/__fc_select.h
+++ b/share/libc/__fc_select.h
@@ -24,13 +24,11 @@
#define __FC_SELECT__
#include "features.h"
__PUSH_FC_STDLIB
-#include "__fc_define_time_t.h"
-#include "__fc_define_suseconds_t.h"
#include "__fc_define_fd_set_t.h"
#include "__fc_define_sigset_t.h"
-
-#include "sys/time.h"
-
+#include "__fc_define_suseconds_t.h"
+#include "__fc_define_timeval.h"
+#include "__fc_define_timespec.h"
__BEGIN_DECLS
/* assigns \result \from nfds, *readfds, *writefds,*errorfds,*timeout,*sigmask;
diff --git a/share/libc/getopt.h b/share/libc/getopt.h
index ed3f45384b71e51ed761a1e0d67c7f38462eb608..380abc7f5aba56b890fa82bd197dbce6e5acead3 100644
--- a/share/libc/getopt.h
+++ b/share/libc/getopt.h
@@ -24,10 +24,9 @@
#define __FC_GETOPT_H
#include "features.h"
__PUSH_FC_STDLIB
-
+#include "unistd.h"
__BEGIN_DECLS
-#include "unistd.h"
/* GNU specific */
struct option
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/select.h b/share/libc/sys/select.h
index c680c04d2e2ec48a879ee4b74dccc8468abfbdd2..d3ceb4b58487f35543d5c5fdf13ec56deea00c6a 100644
--- a/share/libc/sys/select.h
+++ b/share/libc/sys/select.h
@@ -28,6 +28,40 @@ __BEGIN_DECLS
#include "../__fc_select.h"
+/*@
+ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_CLR(int fd, fd_set *fdset);
+#define FD_CLR FD_CLR
+
+// Note: the 2nd argument in FD_ISSET is not const in some implementations
+// due to historical and compatibility reasons.
+/*@
+ requires valid_fdset: \valid_read(fdset);
+ requires initialization: \initialized(fdset);
+ assigns \result \from indirect:*fdset, indirect:fd;
+*/
+extern int FD_ISSET(int fd, const fd_set *fdset);
+#define FD_ISSET FD_ISSET
+
+/*@
+ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_SET(int fd, fd_set *fdset);
+#define FD_SET FD_SET
+
+/*@
+ requires valid_fdset: \valid(fdset);
+ assigns *fdset \from \nothing;
+ ensures initialization: \initialized(fdset);
+*/
+extern void FD_ZERO(fd_set *fdset);
+#define FD_ZERO FD_ZERO
+
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index fbd3da31927d47879bb7ef0c81bf878ba4b5fbc7..db0a5b17b0b5ce5a9eaac4e983ac9bdd0eb45abd 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -24,17 +24,12 @@
#define __FC_SYS_TIME_H__
#include "../features.h"
__PUSH_FC_STDLIB
-__BEGIN_DECLS
-
-#include "../__fc_define_time_t.h"
-#include "../__fc_define_suseconds_t.h"
#include "../__fc_define_fd_set_t.h"
-#include "../__fc_define_timespec.h"
+#include "../__fc_define_suseconds_t.h"
+#include "../__fc_define_time_t.h"
+#include "../__fc_define_timeval.h"
#include "../__fc_string_axiomatic.h"
-struct timeval {
- time_t tv_sec;
- suseconds_t tv_usec;
-};
+__BEGIN_DECLS
struct timezone {
int tz_minuteswest;
diff --git a/share/libc/sys/uio.h b/share/libc/sys/uio.h
index 7ef6ce26a73b7c58c36a3413b228658349faa9ff..b46a65c70647568e1d8dd517c2be12e83bd64bc7 100644
--- a/share/libc/sys/uio.h
+++ b/share/libc/sys/uio.h
@@ -28,15 +28,49 @@ __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..];
+
+
+/*@
+ 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));
+ requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
+ 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);
*/
extern ssize_t readv(int fd, const struct iovec *iov, int 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_read_iov: \valid_read(&iov[0 .. iovcnt-1]);
+ requires valid_read_iov_bases:
+ \forall integer i; 0 <= i < iovcnt ==>
+ \valid_read(((char*)iov[i].iov_base) + (0 .. iov[i].iov_len-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/time.h b/share/libc/time.h
index d156b59c620e759c9709a9b8da294049b57e0476..fe6304ce88d58490ddb41494e6608c6ffed332b0 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -24,14 +24,16 @@
#define __FC_TIME_H
#include "features.h"
__PUSH_FC_STDLIB
+#include "__fc_define_clockid_t.h"
#include "__fc_define_null.h"
#include "__fc_define_size_t.h"
-#include "__fc_define_clockid_t.h"
+#include "__fc_define_time_t.h"
#include "__fc_define_timer_t.h"
+#include "__fc_define_timespec.h"
#include "__fc_string_axiomatic.h"
-
#include "errno.h"
#include "signal.h"
+
/*
* Names of the interval timers, and structure
* defining a timer setting:
@@ -47,7 +49,6 @@ __BEGIN_DECLS
typedef unsigned int clock_t;
#define __clock_t_defined
#endif
-#include "__fc_define_time_t.h"
// From POSIX.1-2008: "The value of CLOCKS_PER_SEC shall be 1 million on
// XSI-conformant systems. [...]"
#define CLOCKS_PER_SEC ((time_t)1000000)
@@ -64,8 +65,6 @@ struct tm {
int tm_isdst; // Daylight Saving Time flag
};
-#include "__fc_define_timespec.h"
-
struct itimerspec {
struct timespec it_interval;
struct timespec it_value;
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index a8c71c4da66bfde812e77250d56ab9b6192509b8..5979b51c4d998f8883c3d332861a36a51cd86688 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -29,16 +29,16 @@ __PUSH_FC_STDLIB
#include "__fc_define_max_open_files.h"
#include "__fc_define_size_t.h"
#include "__fc_define_null.h"
+#include "__fc_define_seek_macros.h"
#include "__fc_define_ssize_t.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_off_t.h"
#include "__fc_define_pid_t.h"
#include "__fc_define_useconds_t.h"
#include "__fc_define_intptr_t.h"
-
-
-
+#include "__fc_define_fds.h"
#include "limits.h"
+__BEGIN_DECLS
extern volatile int Frama_C_entropy_source;
@@ -54,8 +54,6 @@ extern volatile int Frama_C_entropy_source;
#define STDOUT_FILENO 1 /* Standard output. */
#define STDERR_FILENO 2 /* Standard error output. */
-#include "__fc_define_seek_macros.h"
-
/* compatibility macros */
#ifndef __FC_NO_MONOTONIC_CLOCK
@@ -66,8 +64,6 @@ extern volatile int Frama_C_entropy_source;
#define _POSIX_MONOTONIC_CLOCK 0
#endif
-__BEGIN_DECLS
-
/* Values for the NAME argument to `pathconf' and `fpathconf'. */
enum __fc_pathconf_name
{
@@ -722,16 +718,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/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 1a7afd5bee9eaa585b2e079469cfdabf548079f3..313fcf00ef198538e9a90fa4e936f8e944731937 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -342,7 +342,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 487f9d89b834415fa5940e86bf8bd1822b28bedc..cb77e05860c921f2af86471a47a16fd3556fad20 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -187,7 +187,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 2e37d64c5d53416ced6c10ada81782b526bf3fb9..bb72f2bbc63f1b9bba44621ad6fa764bf561cf00 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -366,7 +366,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 44170551c065847fe09d7c0e1cebbfc1f4e0d11b..5288ad885239b257ee03115041beef1d1b10e5e5 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -161,7 +161,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index e5596bda75141d559c531b4d72aeb27b6bf732cd..355bf7bb1f029994a75c785588cf61c82170aeb9 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -8,7 +8,7 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index 077e7e1b7111003c5ae82c748c084ea16eaf0819..62a192f51bb497bafc4593371ad9b0a29aa1e3ef 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -66,7 +66,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 406978ac5f39a280b111b1dc00a11a06c240af64..6d74b78c4afc235b980f246374e40a7ed1a19c5c 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -60,7 +60,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index b1e0c13ab7c0c81ddca966a75862fbafdb2ce343..2a293aeb5a71df9b7843ceaf791a0bc6ab4ed61f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -63,7 +63,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 2ce7032a3b70da634ea4cb3411354f33cc617c46..665e3c0b1cc2ecddafda0d677d2f1f1a72337ef9 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -19,7 +19,7 @@
`logic functions or predicates with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 0fb3e03f963f1ca84c2d99208f7a971bf4e3ab08..09a3554adf54d4a676e021dc16c0d7fb3e087768 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -110,7 +110,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 3db1acf837ee0515dc48f8c484b27563489afa38..a4f24c803d736d1fbbdf9803ba71b612cb937a6a 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -903,7 +903,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 98b179a6be2383e26aac0d389ef7972ac799ecac..b09140dee729c28a7f1f65cee93f96e57c0e5fdc 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -96,7 +96,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
index 3964a37c4107508e018d69cb6119d25a96bbcbe6..d28bedfb6dede9344daeab4b60386b4636bcb9e2 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:814:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:819:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:824:
+[variadic] FRAMAC_SHARE/libc/unistd.h:810:
Declaration of variadic function execlp.
[variadic] tests/erroneous/exec.c:5: Warning:
Incorrect type for argument 3. The argument will be cast from int to char *.
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index d3df0e6caaecd4de576cc56e389dabf8762146eb..85b39e35a56ab3ba5e2efcf128af74add1b33744 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:814:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:819:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:824:
+[variadic] FRAMAC_SHARE/libc/unistd.h:810:
Declaration of variadic function execlp.
[variadic] tests/known/exec.c:9: Translating call to execle to a call to execve.
[variadic] tests/known/exec.c:11: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
index a8e29aef564f9e3150640adc472080a1bb437a93..f04568a4d68f71534e09b863b40a96c050d3b06a 100644
--- a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:814:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:819:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:824:
+[variadic] FRAMAC_SHARE/libc/unistd.h:810:
Declaration of variadic function execlp.
[variadic] tests/known/exec_failed_requirement.c:7:
Translating call to execl to a call to execv.
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 3fab55c7989fe06a0dd332dafeb7f3bb9c6c47d8..fabf605d2b8d14f9aa8503e6553d945e16256a37 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -81,6 +81,49 @@ struct
table
end
+let ident_to_be_ignored id headers =
+ Extlib.string_prefix "__" id ||
+ Extlib.string_prefix "Frama_C" id ||
+ List.filter (fun h -> not (Extlib.string_prefix "__fc" h)) headers = []
+
+let check_ident c11 posix glibc nonstandard c11_headers id headers =
+ if ident_to_be_ignored id headers then (* nothing to check *) ()
+ else begin
+ if Hashtbl.mem c11 id then begin
+ (* Check that the header is the expected one.
+ Note that some symbols may appear in more than one header,
+ possibly due to collisions
+ e.g. 'flock' as type and function). *)
+ let h = Hashtbl.find c11 id in
+ if not (StringSet.mem h c11_headers) then
+ Kernel.warning "<%a>:%s : C11 says %s"
+ (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
+ id h
+ end
+ else if Hashtbl.mem posix id then begin
+ (* check that the header is the expected one *)
+ let (h, _) = Hashtbl.find posix id in
+ (* arpa/inet.h and netinet/in.h are special cases: due to mutual
+ inclusion, there are always issues with their symbols;
+ also, timezone is a special case, since it is a type in
+ sys/time.h, but a variable in time.h in POSIX. However, its
+ declaration as extern is erased by rmtmps, since it is
+ unused. *)
+ if not (List.mem h headers) &&
+ not (List.mem "arpa/inet.h" headers && h = "netinet/in.h" ||
+ List.mem "netinet/in.h" headers && h = "arpa/inet.h") &&
+ id <> "timezone"
+ then
+ Kernel.warning "<%a>:%s : POSIX says %s"
+ (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
+ id h
+ end
+ else if not (StringSet.(mem id glibc || mem id nonstandard)) then
+ Kernel.warning "<%a>:%s : unknown identifier"
+ (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
+ id
+ end
+
let () =
Db.Main.extend (fun () ->
if not !run_once then begin
@@ -94,49 +137,6 @@ let () =
and glibc_idents = Json.(to_set (parse dir "glibc_functions.json"))
and posix_idents = Json.(to_table HeadersAndExtensions (parse dir "posix_identifiers.json"))
and nonstandard_idents = Json.(keys (parse dir "nonstandard_identifiers.json")) in
- Hashtbl.iter (fun id headers ->
- if not (Extlib.string_prefix "__" id) &&
- not (Extlib.string_prefix "Frama_C" id) &&
- List.filter (fun h -> not (Extlib.string_prefix "__fc" h))
- headers <> []
- then
- let id_in_c11 = Hashtbl.mem c11_idents id in
- let id_in_posix = Hashtbl.mem posix_idents id in
- let id_in_glibc = StringSet.mem id glibc_idents in
- let id_in_nonstd = StringSet.mem id nonstandard_idents in
- let header_in_c11 h = StringSet.mem h c11_headers in
- if id_in_c11 then begin
- (* Check that the header is the expected one.
- Note that some symbols may appear in more than one header,
- possibly due to collisions
- (e.g. 'flock' as type and function). *)
- let h = Hashtbl.find c11_idents id in
- if not (header_in_c11 h) then
- Kernel.warning "<%a>:%s : C11 says %s"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
- id h
- end
- else if id_in_posix then begin
- (* check the header is the expected one *)
- let (h, _) = Hashtbl.find posix_idents id in
- (* arpa/inet.h and netinet/in.h are special cases: due to mutual
- inclusion, there are always issues with their symbols;
- also, timezone is a special case, since it is a type in
- sys/time.h, but a variable in time.h in POSIX. However, its
- declaration as extern is erased by rmtmps, since it is
- unused. *)
- if not (List.mem h headers) &&
- not (List.mem "arpa/inet.h" headers && h = "netinet/in.h" ||
- List.mem "netinet/in.h" headers && h = "arpa/inet.h") &&
- id <> "timezone"
- then
- Kernel.warning "<%a>:%s : POSIX says %s"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
- id h
- end
- else if not (id_in_glibc || id_in_nonstd) then
- Kernel.warning "<%a>:%s : unknown identifier"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
- id
- ) fc_stdlib_idents;
+ let check_ident_fun = check_ident c11_idents posix_idents glibc_idents nonstandard_idents c11_headers in
+ Hashtbl.iter check_ident_fun fc_stdlib_idents
end)
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 1345145e950c37a80e559c9426ab5a2ce0dc968e..53b38f02cd517ecf8d921d0aefa51f5aa9693d40 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"
@@ -67,9 +68,10 @@
#include "__fc_define_ssize_t.h"
#include "__fc_define_stat.h"
#include "__fc_define_suseconds_t.h"
-#include "__fc_define_timespec.h"
#include "__fc_define_time_t.h"
#include "__fc_define_timer_t.h"
+#include "__fc_define_timespec.h"
+#include "__fc_define_timeval.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_useconds_t.h"
#include "__fc_define_wchar_t.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 881040218e6562ae1c75d17f17b57abbc7866064..c300bb3596b525db3b01f89b6ba8215600e143c2 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:164: assertion got status valid.
-[eva] tests/libc/fc_libc.c:165: assertion got status valid.
[eva] tests/libc/fc_libc.c:166: assertion got status valid.
[eva] tests/libc/fc_libc.c:167: assertion got status valid.
+[eva] tests/libc/fc_libc.c:168: assertion got status valid.
+[eva] tests/libc/fc_libc.c:169: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -47,7 +47,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (426)
+ Specified-only functions (427)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -175,20 +175,20 @@
wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
- wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ wmemcmp (0 call); wmemmove (0 call); write (0 call); writev (0 call);
Undefined and unspecified functions (1)
=======================================
__builtin_abort (1 call);
- 'Extern' global variables (21)
+ 'Extern' global variables (22)
==============================
- __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
- __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_heap_status;
- __fc_hostname; __fc_locale; __fc_locale_names; __fc_mblen_state;
- __fc_mbtowc_state; __fc_random_counter; __fc_socket_counter;
- __fc_stack_status; __fc_tz; __fc_wctomb_state; optarg; opterr; optopt;
- tzname
+ __fc_basename; __fc_dirname; __fc_fds; __fc_getpwuid_pw_dir;
+ __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell;
+ __fc_heap_status; __fc_hostname; __fc_locale; __fc_locale_names;
+ __fc_mblen_state; __fc_mbtowc_state; __fc_random_counter;
+ __fc_socket_counter; __fc_stack_status; __fc_tz; __fc_wctomb_state; optarg;
+ opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -204,7 +204,7 @@
Goto = 113
Assignment = 625
Exit point = 100
- Function = 527
+ Function = 528
Function call = 144
Pointer dereferencing = 254
Cyclomatic complexity = 371
@@ -214,6 +214,7 @@
#include "__fc_builtin.c"
#include "__fc_builtin.h"
#include "__fc_define_fd_set_t.h"
+#include "__fc_define_timeval.h"
#include "__fc_gcc_builtins.h"
#include "__fc_integer.h"
#include "__fc_select.h"
@@ -264,6 +265,7 @@
#include "stropts.h"
#include "sys/file.h"
#include "sys/resource.h"
+#include "sys/select.h"
#include "sys/sendfile.h"
#include "sys/socket.h"
#include "sys/stat.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index c794e4be1b1caaec773f9e4c3f342430a01ce82f..38af9dde42f8d8384e4405f44b8a48c050d6ff67 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -270,6 +270,10 @@ typedef struct __fc_FILE FILE;
typedef unsigned int id_t;
typedef int suseconds_t;
typedef int clockid_t;
+struct timespec {
+ long tv_sec ;
+ long tv_nsec ;
+};
typedef unsigned int clock_t;
struct tm {
int tm_sec ;
@@ -282,10 +286,6 @@ struct tm {
int tm_yday ;
int tm_isdst ;
};
-struct timespec {
- long tv_sec ;
- long tv_nsec ;
-};
struct dirent {
ino_t d_ino ;
off_t d_off ;
@@ -304,6 +304,10 @@ struct __fc_fd_set {
long __fc_fd_set[(unsigned int)1024 / ((unsigned int)8 * sizeof(long))] ;
};
typedef struct __fc_fd_set fd_set;
+struct timeval {
+ time_t tv_sec ;
+ suseconds_t tv_usec ;
+};
struct flock {
short l_type ;
short l_whence ;
@@ -311,18 +315,6 @@ struct flock {
off_t l_len ;
pid_t l_pid ;
};
-struct timeval {
- time_t tv_sec ;
- suseconds_t tv_usec ;
-};
-struct timezone {
- int tz_minuteswest ;
- int tz_dsttime ;
-};
-struct itimerval {
- struct timeval it_interval ;
- struct timeval it_value ;
-};
typedef void * iconv_t;
struct pollfd {
int fd ;
@@ -350,6 +342,14 @@ struct __fc_code {
int c_val ;
};
typedef struct __fc_code CODE;
+struct timezone {
+ int tz_minuteswest ;
+ int tz_dsttime ;
+};
+struct itimerval {
+ struct timeval it_interval ;
+ struct timeval it_value ;
+};
typedef unsigned long rlim_t;
struct rlimit {
rlim_t rlim_cur ;
@@ -2875,7 +2875,8 @@ int fesetenv(fenv_t const *envp)
return __retres;
}
-/*@ ghost int __fc_fds[1024]; */
+extern int volatile __fc_fds[1024];
+
/*@ requires valid_string_path: valid_read_string(path);
requires valid_amode: (amode & ~((4 | 2) | 1)) ≡ 0 ∨ amode ≡ 0;
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
@@ -4518,11 +4519,70 @@ extern int kill(pid_t pid, int sig);
*/
extern int killpg(pid_t pgrp, int sig);
-/*@ requires valid_read_iov: \valid_read(iov + (0 .. iovcnt - 1));
- assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..));
+/*@ requires valid_fd: 0 ≤ fd < 1024;
+ requires
+ initialization: initialized_inputs:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \initialized(&(iov + i)->iov_base) ∧
+ \initialized(&(iov + i)->iov_len);
+ requires
+ valid_iov:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \valid((char *)(&(iov + i)->iov_base) +
+ (0 .. (iov + i)->iov_len - 1));
+ requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
+ ensures
+ result_error_or_read_bytes:
+ \result ≡ -1 ∨
+ (0 ≤ \result ≤
+ \sum(0, \old(iovcnt) - 1, \lambda ℤ k; (\old(iov) + k)->iov_len));
+ 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]),
+ (indirect: *(iov + (0 ..))), (indirect: iovcnt);
*/
extern ssize_t readv(int fd, struct iovec const *iov, int iovcnt);
+/*@ requires valid_fd: 0 ≤ fd < 1024;
+ requires
+ initialization: initialized_inputs:
+ ∀ ℤ 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_bases:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \valid_read((char *)(iov + i)->iov_base +
+ (0 .. (iov + i)->iov_len - 1));
+ requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
+ requires
+ bounded_lengths:
+ \sum(0, iovcnt - 1, \lambda ℤ k; (iov + k)->iov_len) ≤ 2147483647;
+ ensures
+ result_error_or_written_bytes:
+ \result ≡ -1 ∨
+ (0 ≤ \result ≤
+ \sum(0, \old(iovcnt) - 1, \lambda ℤ k; (\old(iov) + k)->iov_len));
+ assigns \result, __fc_fds[fd];
+ assigns \result
+ \from (indirect: fd), (indirect: __fc_fds[fd]),
+ (indirect: *(iov + (0 ..))), (indirect: iovcnt);
+ assigns __fc_fds[fd]
+ \from (indirect: *(iov + (0 ..))), (indirect: iovcnt);
+ */
+extern ssize_t writev(int fd, struct iovec const *iov, int iovcnt);
+
/*@ ghost struct __fc_sockfds_type __fc_sockfds[1024]; */
/*@ ghost extern int __fc_socket_counter; */
@@ -7777,34 +7837,6 @@ extern DIR *opendir(char const *path);
*/
extern struct dirent *readdir(DIR *dirp);
-/*@ requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset;
- assigns *fdset \from *fdset, (indirect: fd);
- */
-extern void FD_CLR(int fd, fd_set *fdset);
-
-/*@ requires valid_fdset: \valid_read(fdset);
- requires initialization: \initialized(fdset);
- assigns \result;
- assigns \result \from (indirect: *fdset), (indirect: fd);
- */
-extern int FD_ISSET(int fd, fd_set const *fdset);
-
-/*@ requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset;
- assigns *fdset \from *fdset, (indirect: fd);
- */
-extern void FD_SET(int fd, fd_set *fdset);
-
-/*@ requires valid_fdset: \valid(fdset);
- ensures initialization: \initialized(\old(fdset));
- assigns *fdset;
- assigns *fdset \from \nothing;
- */
-extern void FD_ZERO(fd_set *fdset);
-
/*@ requires valid_res: \valid(res);
ensures initialization: res: \initialized(\old(res));
ensures res_wrapped: *\old(res) ≡ (int)(\old(a) + \old(b));
@@ -8220,192 +8252,6 @@ extern int __va_openat_void(int dirfd, char const *filename, int flags);
extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
mode_t mode);
-/*@ ghost extern int __fc_tz; */
-
-/*@ requires valid_path: valid_read_string(path);
- requires
- valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null;
- assigns \result;
- assigns \result
- \from (indirect: *(path + (0 .. strlen{Old}(path)))),
- (indirect: times), (indirect: *(times + (0 .. 1)));
- */
-extern int utimes(char const *path, struct timeval const times[2]);
-
-/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
- assigns tv->tv_sec \from __fc_time;
- assigns tv->tv_usec \from __fc_time;
- assigns *((struct timezone *)tz) \from __fc_tz;
- assigns \result
- \from (indirect: tv), (indirect: tz), *tv, *((struct timezone *)tz),
- __fc_tz;
-
- behavior tv_and_tz_null:
- assumes null_tv_tz: tv ≡ \null ∧ tz ≡ \null;
- assigns \result;
- assigns \result \from (indirect: __fc_tz);
-
- behavior tv_not_null:
- assumes non_null_tv_null_tz: tv ≢ \null ∧ tz ≡ \null;
- ensures
- initialization: tv_sec: tv_usec:
- \initialized(&\old(tv)->tv_sec) ∧
- \initialized(&\old(tv)->tv_usec);
- ensures tv_usec_bounded: 0 ≤ \old(tv)->tv_usec ≤ 999999;
- assigns tv->tv_sec, tv->tv_usec, \result;
- assigns tv->tv_sec \from (indirect: __fc_time);
- assigns tv->tv_usec \from (indirect: __fc_time);
- assigns \result \from (indirect: *tv), (indirect: __fc_tz);
-
- behavior tz_not_null:
- assumes null_tv_non_null_tz: tv ≡ \null ∧ tz ≢ \null;
- ensures initialization: tz: \initialized((struct timezone *)\old(tz));
- assigns *((struct timezone *)tz), \result;
- assigns *((struct timezone *)tz) \from __fc_tz;
- assigns \result
- \from (indirect: *((struct timezone *)tz)), (indirect: __fc_tz);
-
- behavior tv_and_tz_not_null:
- assumes non_null_tv_tz: tv ≢ \null ∧ tz ≢ \null;
- ensures
- initialization: tv_sec: tv_usec:
- \initialized(&\old(tv)->tv_sec) ∧
- \initialized(&\old(tv)->tv_usec);
- ensures initialization: tz: \initialized((struct timezone *)\old(tz));
- assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
- assigns tv->tv_sec \from (indirect: __fc_time);
- assigns tv->tv_usec \from (indirect: __fc_time);
- assigns *((struct timezone *)tz) \from __fc_tz;
- assigns \result
- \from (indirect: *tv), (indirect: *((struct timezone *)tz)),
- (indirect: __fc_tz);
-
- complete behaviors tv_and_tz_not_null,
- tz_not_null,
- tv_not_null,
- tv_and_tz_null;
- disjoint behaviors tv_and_tz_not_null,
- tz_not_null,
- tv_not_null,
- tv_and_tz_null;
- */
-extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
-
-/*@ requires valid_tv_or_null: \valid_read(tv) ∨ tv ≡ \null;
- requires valid_tz_or_null: \valid_read(tz) ∨ tz ≡ \null;
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns __fc_time, __fc_tz, \result;
- assigns __fc_time
- \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
- assigns __fc_tz
- \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
- assigns \result \from (indirect: *tv), (indirect: *tz);
- */
-extern int settimeofday(struct timeval const *tv, struct timezone const *tz);
-
-/*@ ghost struct itimerval volatile __fc_itimer_real; */
-/*@ ghost struct itimerval volatile __fc_itimer_virtual; */
-/*@ ghost struct itimerval volatile __fc_itimer_prof; */
-/*@ requires valid_curr_value: \valid(curr_value);
- ensures initialization: curr_value: \initialized(\old(curr_value));
- assigns \result, *curr_value;
- assigns \result \from (indirect: which);
- assigns *curr_value
- \from __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
-
- behavior real:
- assumes itimer_real: which ≡ 0;
- ensures result_ok: \result ≡ 0;
- assigns \result, *curr_value;
- assigns \result \from \nothing;
- assigns *curr_value \from __fc_itimer_real;
-
- behavior virtual:
- assumes itimer_virtual: which ≡ 1;
- ensures result_ok: \result ≡ 0;
- assigns \result, *curr_value;
- assigns \result \from \nothing;
- assigns *curr_value \from __fc_itimer_virtual;
-
- behavior prof:
- assumes itimer_prof: which ≡ 2;
- ensures result_ok: \result ≡ 0;
- assigns \result, *curr_value;
- assigns \result \from \nothing;
- assigns *curr_value \from __fc_itimer_prof;
-
- behavior invalid:
- assumes invalid_which: which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2;
- ensures result_error: \result ≡ -1;
- assigns \result;
- assigns \result \from \nothing;
-
- complete behaviors invalid, prof, virtual, real;
- disjoint behaviors invalid, prof, virtual, real;
- */
-extern int getitimer(int which, struct itimerval *curr_value);
-
-/*@ requires valid_new_value: \valid_read(new_value);
- requires
- old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns *old_value, \result;
- assigns *old_value
- \from (indirect: which), (indirect: old_value), (indirect: new_value),
- __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
- assigns \result
- \from (indirect: which), (indirect: new_value), (indirect: *new_value);
-
- behavior real:
- assumes
- itimer_real_and_valid:
- which ≡ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
- ensures result_ok: \result ≡ 0;
- ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, *old_value, __fc_itimer_real;
- assigns \result \from \nothing;
- assigns *old_value \from __fc_itimer_real;
- assigns __fc_itimer_real \from *new_value;
-
- behavior virtual:
- assumes
- itimer_virtual_and_valid:
- which ≡ 1 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
- ensures result_ok: \result ≡ 0;
- ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, *old_value;
- assigns \result \from \nothing;
- assigns *old_value \from __fc_itimer_virtual;
-
- behavior prof:
- assumes
- itimer_prof_and_valid:
- which ≡ 2 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
- ensures result_ok: \result ≡ 0;
- ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, *old_value;
- assigns \result \from \nothing;
- assigns *old_value \from __fc_itimer_prof;
-
- behavior invalid:
- assumes
- invalid_itimer_or_new_value:
- (which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2) ∨
- ¬(0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999);
- ensures result_error: \result ≡ -1;
- assigns \result;
- assigns \result \from \nothing;
-
- disjoint behaviors invalid, prof, virtual, real;
- */
-extern int setitimer(int which, struct itimerval const * restrict new_value,
- struct itimerval * restrict old_value);
-
/*@ ghost int volatile __fc_fds_state; */
/*@ requires nfds: nfds ≥ 0;
requires readfs: readfds ≡ \null ∨ \valid(readfds);
@@ -8861,6 +8707,220 @@ extern void syslog(int __x0, char const *__x1, void * const *__va_params);
/*@ assigns \nothing; */
extern void vsyslog(int __x0, char const *__x1, va_list __x2);
+/*@ ghost extern int __fc_tz; */
+
+/*@ requires valid_path: valid_read_string(path);
+ requires
+ valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: times), (indirect: *(times + (0 .. 1)));
+ */
+extern int utimes(char const *path, struct timeval const times[2]);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
+ assigns tv->tv_sec \from __fc_time;
+ assigns tv->tv_usec \from __fc_time;
+ assigns *((struct timezone *)tz) \from __fc_tz;
+ assigns \result
+ \from (indirect: tv), (indirect: tz), *tv, *((struct timezone *)tz),
+ __fc_tz;
+
+ behavior tv_and_tz_null:
+ assumes null_tv_tz: tv ≡ \null ∧ tz ≡ \null;
+ assigns \result;
+ assigns \result \from (indirect: __fc_tz);
+
+ behavior tv_not_null:
+ assumes non_null_tv_null_tz: tv ≢ \null ∧ tz ≡ \null;
+ ensures
+ initialization: tv_sec: tv_usec:
+ \initialized(&\old(tv)->tv_sec) ∧
+ \initialized(&\old(tv)->tv_usec);
+ ensures tv_usec_bounded: 0 ≤ \old(tv)->tv_usec ≤ 999999;
+ assigns tv->tv_sec, tv->tv_usec, \result;
+ assigns tv->tv_sec \from (indirect: __fc_time);
+ assigns tv->tv_usec \from (indirect: __fc_time);
+ assigns \result \from (indirect: *tv), (indirect: __fc_tz);
+
+ behavior tz_not_null:
+ assumes null_tv_non_null_tz: tv ≡ \null ∧ tz ≢ \null;
+ ensures initialization: tz: \initialized((struct timezone *)\old(tz));
+ assigns *((struct timezone *)tz), \result;
+ assigns *((struct timezone *)tz) \from __fc_tz;
+ assigns \result
+ \from (indirect: *((struct timezone *)tz)), (indirect: __fc_tz);
+
+ behavior tv_and_tz_not_null:
+ assumes non_null_tv_tz: tv ≢ \null ∧ tz ≢ \null;
+ ensures
+ initialization: tv_sec: tv_usec:
+ \initialized(&\old(tv)->tv_sec) ∧
+ \initialized(&\old(tv)->tv_usec);
+ ensures initialization: tz: \initialized((struct timezone *)\old(tz));
+ assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
+ assigns tv->tv_sec \from (indirect: __fc_time);
+ assigns tv->tv_usec \from (indirect: __fc_time);
+ assigns *((struct timezone *)tz) \from __fc_tz;
+ assigns \result
+ \from (indirect: *tv), (indirect: *((struct timezone *)tz)),
+ (indirect: __fc_tz);
+
+ complete behaviors tv_and_tz_not_null,
+ tz_not_null,
+ tv_not_null,
+ tv_and_tz_null;
+ disjoint behaviors tv_and_tz_not_null,
+ tz_not_null,
+ tv_not_null,
+ tv_and_tz_null;
+ */
+extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
+
+/*@ requires valid_tv_or_null: \valid_read(tv) ∨ tv ≡ \null;
+ requires valid_tz_or_null: \valid_read(tz) ∨ tz ≡ \null;
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns __fc_time, __fc_tz, \result;
+ assigns __fc_time
+ \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
+ assigns __fc_tz
+ \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
+ assigns \result \from (indirect: *tv), (indirect: *tz);
+ */
+extern int settimeofday(struct timeval const *tv, struct timezone const *tz);
+
+/*@ ghost struct itimerval volatile __fc_itimer_real; */
+/*@ ghost struct itimerval volatile __fc_itimer_virtual; */
+/*@ ghost struct itimerval volatile __fc_itimer_prof; */
+/*@ requires valid_curr_value: \valid(curr_value);
+ ensures initialization: curr_value: \initialized(\old(curr_value));
+ assigns \result, *curr_value;
+ assigns \result \from (indirect: which);
+ assigns *curr_value
+ \from __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+
+ behavior real:
+ assumes itimer_real: which ≡ 0;
+ ensures result_ok: \result ≡ 0;
+ assigns \result, *curr_value;
+ assigns \result \from \nothing;
+ assigns *curr_value \from __fc_itimer_real;
+
+ behavior virtual:
+ assumes itimer_virtual: which ≡ 1;
+ ensures result_ok: \result ≡ 0;
+ assigns \result, *curr_value;
+ assigns \result \from \nothing;
+ assigns *curr_value \from __fc_itimer_virtual;
+
+ behavior prof:
+ assumes itimer_prof: which ≡ 2;
+ ensures result_ok: \result ≡ 0;
+ assigns \result, *curr_value;
+ assigns \result \from \nothing;
+ assigns *curr_value \from __fc_itimer_prof;
+
+ behavior invalid:
+ assumes invalid_which: which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2;
+ ensures result_error: \result ≡ -1;
+ assigns \result;
+ assigns \result \from \nothing;
+
+ complete behaviors invalid, prof, virtual, real;
+ disjoint behaviors invalid, prof, virtual, real;
+ */
+extern int getitimer(int which, struct itimerval *curr_value);
+
+/*@ requires valid_new_value: \valid_read(new_value);
+ requires
+ old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns *old_value, \result;
+ assigns *old_value
+ \from (indirect: which), (indirect: old_value), (indirect: new_value),
+ __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+ assigns \result
+ \from (indirect: which), (indirect: new_value), (indirect: *new_value);
+
+ behavior real:
+ assumes
+ itimer_real_and_valid:
+ which ≡ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
+ ensures result_ok: \result ≡ 0;
+ ensures initialization: old_value: \initialized(\old(old_value));
+ assigns \result, *old_value, __fc_itimer_real;
+ assigns \result \from \nothing;
+ assigns *old_value \from __fc_itimer_real;
+ assigns __fc_itimer_real \from *new_value;
+
+ behavior virtual:
+ assumes
+ itimer_virtual_and_valid:
+ which ≡ 1 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
+ ensures result_ok: \result ≡ 0;
+ ensures initialization: old_value: \initialized(\old(old_value));
+ assigns \result, *old_value;
+ assigns \result \from \nothing;
+ assigns *old_value \from __fc_itimer_virtual;
+
+ behavior prof:
+ assumes
+ itimer_prof_and_valid:
+ which ≡ 2 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
+ ensures result_ok: \result ≡ 0;
+ ensures initialization: old_value: \initialized(\old(old_value));
+ assigns \result, *old_value;
+ assigns \result \from \nothing;
+ assigns *old_value \from __fc_itimer_prof;
+
+ behavior invalid:
+ assumes
+ invalid_itimer_or_new_value:
+ (which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2) ∨
+ ¬(0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999);
+ ensures result_error: \result ≡ -1;
+ assigns \result;
+ assigns \result \from \nothing;
+
+ disjoint behaviors invalid, prof, virtual, real;
+ */
+extern int setitimer(int which, struct itimerval const * restrict new_value,
+ struct itimerval * restrict old_value);
+
+/*@ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset;
+ assigns *fdset \from *fdset, (indirect: fd);
+ */
+extern void FD_CLR(int fd, fd_set *fdset);
+
+/*@ requires valid_fdset: \valid_read(fdset);
+ requires initialization: \initialized(fdset);
+ assigns \result;
+ assigns \result \from (indirect: *fdset), (indirect: fd);
+ */
+extern int FD_ISSET(int fd, fd_set const *fdset);
+
+/*@ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset;
+ assigns *fdset \from *fdset, (indirect: fd);
+ */
+extern void FD_SET(int fd, fd_set *fdset);
+
+/*@ requires valid_fdset: \valid(fdset);
+ ensures initialization: \initialized(\old(fdset));
+ assigns *fdset;
+ assigns *fdset \from \nothing;
+ */
+extern void FD_ZERO(fd_set *fdset);
+
/*@ assigns \result;
assigns \result \from which, who; */
extern int getpriority(int which, id_t who);
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 815b277af9e8e3fecf6f395a1b1b023ea8dd3ffa..eca9057a10e161facaeb91f1b8b069d8788ad038 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -6,6 +6,7 @@
[kernel] Parsing share/libc/__fc_define_dev_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_eof.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fd_set_t.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_define_fds.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_file.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fpos_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fs_cnt.h (with preprocessing)
@@ -32,6 +33,7 @@
[kernel] Parsing share/libc/__fc_define_time_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_timer_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_timespec.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_define_timeval.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_uid_and_gid.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_useconds_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_wchar_t.h (with preprocessing)
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 75b421147917c7fdf6b9f9bcbd1001f867f21829..884473c2427f4106a9d6c5fded60ee06f15b1c86 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -317,8 +317,8 @@
[eva:final-states] Values at end of function main:
__fc_errno ∈ [--..--]
__fc_heap_status ∈ [--..--]
+ __fc_fds[0..1023] ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- __fc_fds[0..1023] ∈ {0}
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
__fc_ghbn.host.h_name ∈ {{ NULL ; &__fc_ghbn.hostbuf[0] }}
diff --git a/tests/libc/oracle/socket.0.res.oracle b/tests/libc/oracle/socket.0.res.oracle
index c0f9285b9913c93af17f9c46cecdd5f9e2b994d1..276fcf21362da709bfb1e3539c7ad646d8272d88 100644
--- a/tests/libc/oracle/socket.0.res.oracle
+++ b/tests/libc/oracle/socket.0.res.oracle
@@ -68,24 +68,20 @@
[eva] Done for function test_read
[eva] computing for function test_readv <- main.
Called from tests/libc/socket.c:127.
-[eva] computing for function init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:68.
-[eva] computing for function bzero <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:43.
-[eva] Done for function bzero
-[eva] computing for function write <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:44.
-[eva] Done for function write
-[eva] Recording results for init_reception
-[eva] Done for function init_reception
+[eva] tests/libc/socket.c:68: Reusing old results for call to init_reception
[eva] computing for function readv <- test_readv <- main.
Called from tests/libc/socket.c:69.
[eva] using specification for function readv
[eva] tests/libc/socket.c:69:
- function readv: precondition 'valid_read_iov' got status valid.
-[eva] share/libc/sys/uio.h:37: Warning:
- no \from part
- for clause 'assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..));'
+ function readv: precondition 'valid_fd' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'valid_iov' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:52:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
[eva] Done for function readv
[eva:alarm] tests/libc/socket.c:72: Warning:
accessing uninitialized left-value.
@@ -240,8 +236,8 @@
[2].iov_len ∈ {3}
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_recvmsg:
- __fc_sockfds[0..1023] ∈ [--..--]
__fc_fds[0..1023] ∈ [--..--]
+ __fc_sockfds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
rcv_buffer_scattered1[0] ∈ [--..--]
[1] ∈ [--..--] or UNINITIALIZED
@@ -265,9 +261,9 @@
.msg_flags ∈ [--..--] or UNINITIALIZED
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_server_echo:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
addrlen ∈ {8}
@@ -276,9 +272,9 @@
r ∈ [-1..64]
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
socket_fd[0..1] ∈ [0..1023]
r ∈ {0; 1; 5; 20; 100; 200; 300; 400}
diff --git a/tests/libc/oracle/socket.1.res.oracle b/tests/libc/oracle/socket.1.res.oracle
index a60c6913b0fb68fee18a85d1c2bc363f9fadb3a7..82d1a5a2090728ffd2cadaba116d11e3f9084d6a 100644
--- a/tests/libc/oracle/socket.1.res.oracle
+++ b/tests/libc/oracle/socket.1.res.oracle
@@ -68,24 +68,20 @@
[eva] Done for function test_read
[eva] computing for function test_readv <- main.
Called from tests/libc/socket.c:127.
-[eva] computing for function init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:68.
-[eva] computing for function bzero <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:43.
-[eva] Done for function bzero
-[eva] computing for function write <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:44.
-[eva] Done for function write
-[eva] Recording results for init_reception
-[eva] Done for function init_reception
+[eva] tests/libc/socket.c:68: Reusing old results for call to init_reception
[eva] computing for function readv <- test_readv <- main.
Called from tests/libc/socket.c:69.
[eva] using specification for function readv
[eva] tests/libc/socket.c:69:
- function readv: precondition 'valid_read_iov' got status valid.
-[eva] share/libc/sys/uio.h:37: Warning:
- no \from part
- for clause 'assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..));'
+ function readv: precondition 'valid_fd' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'valid_iov' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:52:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
[eva] Done for function readv
[eva:alarm] tests/libc/socket.c:72: Warning:
accessing uninitialized left-value.
@@ -240,8 +236,8 @@
[2].iov_len ∈ {3}
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_recvmsg:
- __fc_sockfds[0..1023] ∈ [--..--]
__fc_fds[0..1023] ∈ [--..--]
+ __fc_sockfds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
rcv_buffer_scattered1[0] ∈ [--..--]
[1] ∈ [--..--] or UNINITIALIZED
@@ -267,9 +263,9 @@
.msg_flags ∈ [--..--] or UNINITIALIZED
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_server_echo:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
addrlen ∈ {8}
@@ -278,9 +274,9 @@
r ∈ [-1..64]
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
socket_fd[0..1] ∈ [0..1023]
r ∈ {0; 1; 5; 20; 100; 200; 300; 400}
diff --git a/tests/libc/oracle/sys_uio_h.res.oracle b/tests/libc/oracle/sys_uio_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..feee0f8a0d4570603b66fd56bf5d8a7389ebe5d3
--- /dev/null
+++ b/tests/libc/oracle/sys_uio_h.res.oracle
@@ -0,0 +1,112 @@
+[kernel] Parsing tests/libc/sys_uio_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+[eva] computing for function __va_open_mode_t <- main.
+ Called from tests/libc/sys_uio_h.c:17.
+[eva] using specification for function __va_open_mode_t
+[eva] tests/libc/sys_uio_h.c:17:
+ function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] tests/libc/sys_uio_h.c:19: assertion got status valid.
+[eva] tests/libc/sys_uio_h.c:20: assertion got status valid.
+[eva] tests/libc/sys_uio_h.c:21: assertion got status valid.
+[eva] computing for function writev <- main.
+ Called from tests/libc/sys_uio_h.c:22.
+[eva] using specification for function writev
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'valid_fd' got status valid.
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'valid_read_iov' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:22: Warning:
+ function writev: precondition 'valid_read_iov_bases' got status unknown.
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:67:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
+[eva:alarm] tests/libc/sys_uio_h.c:22: Warning:
+ function writev: precondition 'bounded_lengths' got status unknown.
+[eva] share/libc/sys/uio.h:72:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
+[eva] Done for function writev
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_uio_h.c:23.
+[eva] using specification for function close
+[eva] tests/libc/sys_uio_h.c:23:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] computing for function __va_open_void <- main.
+ Called from tests/libc/sys_uio_h.c:24.
+[eva] using specification for function __va_open_void
+[eva] tests/libc/sys_uio_h.c:24:
+ function __va_open_void: precondition 'valid_filename' got status valid.
+[eva] tests/libc/sys_uio_h.c:24:
+ function __va_open_void: precondition 'flag_not_CREAT' got status valid.
+[eva] Done for function __va_open_void
+[eva] computing for function readv <- main.
+ Called from tests/libc/sys_uio_h.c:25.
+[eva] using specification for function readv
+[eva:alarm] tests/libc/sys_uio_h.c:25: Warning:
+ function readv: precondition 'valid_fd' got status unknown.
+[eva] tests/libc/sys_uio_h.c:25:
+ function readv: precondition 'initialization,initialized_inputs' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:25: Warning:
+ function readv: precondition 'valid_iov' got status unknown.
+[eva] tests/libc/sys_uio_h.c:25:
+ function readv: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:52:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
+[eva] Done for function readv
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_uio_h.c:26.
+[eva] tests/libc/sys_uio_h.c:26:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] computing for function __va_open_mode_t <- main.
+ Called from tests/libc/sys_uio_h.c:37.
+[eva] tests/libc/sys_uio_h.c:37:
+ function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] computing for function writev <- main.
+ Called from tests/libc/sys_uio_h.c:39.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'valid_fd' got status valid.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'valid_read_iov' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:39: Warning:
+ function writev: precondition 'valid_read_iov_bases' got status unknown.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'bounded_iovcnt' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:39: Warning:
+ function writev: precondition 'bounded_lengths' got status unknown.
+[eva] Done for function writev
+[eva:alarm] tests/libc/sys_uio_h.c:40: Warning:
+ assertion 'unreachable' got status invalid (stopping propagation).
+[eva:alarm] tests/libc/sys_uio_h.c:43: Warning:
+ signed overflow. assert w + r ≤ 2147483647;
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
+ str ∈ {{ "A small string" }}
+ empty_buf ∈ {0}
+ buf[0..9] ∈ [--..--]
+ buf2[0..13] ∈ [--..--] or UNINITIALIZED
+ v[0].iov_base ∈ {{ "A small string" }}
+ [0].iov_len ∈ {15}
+ [1] ∈ {0}
+ [2].iov_base ∈ {{ (void *)&buf }}
+ [2].iov_len ∈ {10}
+ [3].iov_base ∈ {{ (void *)&buf2 }}
+ [3].iov_len ∈ {14}
+ fd ∈ [-1..1023]
+ w ∈ [-1..2147483647]
+ r ∈ [-1..2147483647]
+ __retres ∈ [-2..2147483647]
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 55e6a1c528de73a57f89e7f4b640206bc2f38233..5173981ab82804e60d054d1f19aea51cd3f81bc2 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -570,9 +570,8 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- __fc_fds[0] ∈ {0}
- [1..1023] ∈ [--..--]
r ∈ {-1; 0}
hostname[0..255] ∈ [--..--] or UNINITIALIZED
fd ∈ [-1..1023]
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 1ce6be573a566003223a378d330cfdb7e4c1744b..fa6d33a9d1b05edf653138dc9d4527f5421f3532 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -570,9 +570,8 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- __fc_fds[0] ∈ {0}
- [1..1023] ∈ [--..--]
r ∈ {-1; 0}
hostname[0..255] ∈ [--..--] or UNINITIALIZED
fd ∈ [-1..1023]
diff --git a/tests/libc/sys_uio_h.c b/tests/libc/sys_uio_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..2bde83999ac582c7c96456c572735e9c3ceef108
--- /dev/null
+++ b/tests/libc/sys_uio_h.c
@@ -0,0 +1,44 @@
+#include <sys/uio.h>
+#include <unistd.h>
+#include <fcntl.h>
+volatile int nondet;
+int main() {
+ char *str = "A small string";
+ char *empty_buf = 0;
+ char buf[10] = "\n\n\nbuffer";
+ char buf2[14];
+ struct iovec v[4] =
+ {
+ {str, 15},
+ {empty_buf, 0},
+ {buf, 10},
+ {buf2, 14},
+ };
+ int fd = open("/tmp/uio.txt", O_WRONLY | O_CREAT, 0660);
+ if (fd < 0) return 1;
+ //@ assert \valid_read(((char*)v[0].iov_base) + (0 .. v[0].iov_len-1));
+ //@ assert \valid_read(((char*)v[1].iov_base) + (0 .. v[1].iov_len-1));
+ //@ assert \valid_read(((char*)v[2].iov_base) + (0 .. v[2].iov_len-1));
+ ssize_t w = writev(fd, v, 3);
+ close(fd);
+ fd = open("/tmp/uio.txt", O_RDONLY);
+ ssize_t r = readv(fd, v+2, 2);
+ close(fd);
+
+ if (nondet) {
+ char buf3[10] = "\n\n\nbuffer";
+ char buf4[14];
+ struct iovec v2[4] =
+ {
+ {str, 15},
+ {empty_buf, 0},
+ {buf3, 11}, // invalid length
+ };
+ int fd2 = open("/tmp/uio2.txt", O_WRONLY | O_CREAT, 0660);
+ if (fd2 < 0) return 1;
+ ssize_t w = writev(fd2, v2, 3); // must fail
+ //@ assert unreachable: \false;
+ }
+
+ return w + r;
+}
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index a57305d1570190ba61230b014b4c0bec1da423ae..189a5298dc644b531bbc585f569754593b007010 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -44,10 +44,11 @@
=======================================
- 'Extern' global variables (11)
+ 'Extern' global variables (12)
==============================
- Frama_C_entropy_source; __fc_errno; __fc_heap_status; __fc_hostname;
- __fc_stdin; __fc_stdout; __fc_ttyname; optarg; opterr; optind; optopt
+ Frama_C_entropy_source; __fc_errno; __fc_fds; __fc_heap_status;
+ __fc_hostname; __fc_stdin; __fc_stdout; __fc_ttyname; optarg; opterr;
+ optind; optopt
Potential entry points (2)
==========================
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
index afe73bccdad6b27be86cc5b509fb01fda44e6ce4..de14067e7a65d53a82dd943adb71c6cb31536f68 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -136,7 +136,7 @@
],
"undefined-functions": [],
"extern-global-vars": [
- "Frama_C_entropy_source", "__fc_errno", "__fc_heap_status",
+ "Frama_C_entropy_source", "__fc_errno", "__fc_fds", "__fc_heap_status",
"__fc_hostname", "__fc_stdin", "__fc_stdout", "__fc_ttyname", "optarg",
"opterr", "optind", "optopt"
],