diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index bbfa44c8c4870a434e4ad392dd8e6f673e9bbe3d..114226d440b98d6ddeb1f02ee7ef9249709a3be9 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -443,11 +443,10 @@ extern int listen(int sockfd, int backlog);
*/
extern ssize_t recv(int sockfd, void * buf, size_t len, int flags);
-
/*@
requires valid_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
requires valid_buffer_length: \valid((char *)buf+(0 .. len-1));
- requires valid_addrbuf_or_null: (\valid(addrbuf_len) &&
+ requires valid_addrbuf_or_null:initialization: (\valid(addrbuf_len) &&
\initialized(addrbuf_len) &&
\valid((char *)addrbuf+(0 .. *addrbuf_len-1)))
|| (addrbuf == \null && addrbuf_len == \null);
@@ -503,7 +502,23 @@ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags);
ensures error_or_chars_sent: \result == -1 || 0 <= \result <= len;
*/
extern ssize_t send(int sockfd, const void *buf, size_t len, int flags);
-extern ssize_t sendmsg(int, const struct msghdr *, int);
+
+/*@
+ requires available_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
+ requires valid_message: \valid_read(message);
+ requires valid_msg_iov:
+ \valid_read(message->msg_iov+(0 .. message->msg_iovlen - 1));
+ assigns __fc_sockfds[sockfd]
+ \from __fc_sockfds[sockfd],
+ indirect:*message,
+ indirect:message->msg_iov[0 .. message->msg_iovlen - 1],
+ indirect:flags;
+ assigns \result \from indirect:sockfd, indirect:__fc_sockfds[sockfd],
+ indirect:*message,
+ indirect:message->msg_iov[0 .. message->msg_iovlen - 1];
+ ensures error_or_chars_sent: \result == -1 || 0 <= \result;
+ */
+extern ssize_t sendmsg(int sockfd, const struct msghdr *message, int flags);
/*@
requires available_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 34961a42ef36a7b529797e1df57f6a644cc90a8a..f26a5b8ed9b284074e578891a1bd46a8c3d6d20b 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -947,7 +947,21 @@ extern char *getwd(char *);
extern int isatty(int fd);
extern int lchown(const char *, uid_t, gid_t);
-extern int link(const char *, const char *);
+
+/*@ //missing: may assign to errno: EACCES, EEXIST, ELOOP, EMLINK, ENAMETOOLONG,
+ // ENOENT, ENOSPC, ENOTDIR, EPERM, EROFS,
+ // EXDEV, EBADF, ENOTDIR, EINVAL;
+ // missing: assigns 'filesystem' \from path1[0..strlen(path1)],
+ // path2[0..strlen(path2)];
+ // missing: assigns \result \from 'paths in filesystem'
+ requires valid_path: valid_read_string(path1);
+ requires valid_path: valid_read_string(path2);
+ assigns \result \from indirect:path1[0 .. strlen(path1)],
+ indirect:path2[0 .. strlen(path2)];
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int link(const char *path1, const char *path2);
+
extern int lockf(int, int, off_t);
/*@ //missing: may assign to errno: EBADF, EINVAL, EOVERFLOW, ESPIPE, ENXIO (Linux);
@@ -1108,7 +1122,7 @@ extern useconds_t ualarm(useconds_t, useconds_t);
// missing: assigns 'filesystem' \from path[0..];
// missing: assigns \result \from 'filesystem';
requires valid_string_path: valid_read_string(path);
- assigns \result \from path[0..];
+ assigns \result \from indirect:path[0..strlen(path)];
ensures result_ok_or_error: \result == 0 || \result == -1;
*/
extern int unlink(const char *path);
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 4cc020e5cf67e2cd14bf36a7352becb045d90275..64302fc49a200a36a4598d1a0179f3b0f3eda298 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -14,8 +14,6 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
-[kernel] FRAMAC_SHARE/libc/sys/socket.h:451: Warning:
- clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 783ce70eb1f3618495a6167da824d512425c6c18..6ba53d2036b480268f8f925ee06e00879500715d 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3180,6 +3180,16 @@ extern uid_t getuid(void);
*/
extern int isatty(int fd);
+/*@ requires valid_path: valid_read_string(path1);
+ requires valid_path: valid_read_string(path2);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(path1 + (0 .. strlen{Old}(path1)))),
+ (indirect: *(path2 + (0 .. strlen{Old}(path2))));
+ */
+extern int link(char const *path1, char const *path2);
+
/*@ requires valid_fd: 0 ≤ fd < 1024;
requires valid_whence: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
ensures result_error_or_offset: \result ≡ -1 ∨ 0 ≤ \result;
@@ -3300,7 +3310,7 @@ extern char *ttyname(int fildes);
/*@ requires valid_string_path: valid_read_string(path);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
- assigns \result \from *(path + (0 ..));
+ assigns \result \from (indirect: *(path + (0 .. strlen{Old}(path))));
*/
extern int unlink(char const *path);
@@ -4854,7 +4864,7 @@ extern ssize_t recv(int sockfd, void *buf, size_t len, int flags);
/*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
requires valid_buffer_length: \valid((char *)buf + (0 .. len - 1));
requires
- valid_addrbuf_or_null:
+ valid_addrbuf_or_null: initialization:
(\valid(addrbuf_len) ∧ \initialized(addrbuf_len) ∧
\valid((char *)addrbuf + (0 .. *addrbuf_len - 1))) ∨
(addrbuf ≡ \null ∧ addrbuf_len ≡ \null);
@@ -4936,6 +4946,24 @@ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags);
*/
extern ssize_t send(int sockfd, void const *buf, size_t len, int flags);
+/*@ requires available_sockfd: 0 ≤ sockfd < 1024;
+ requires valid_message: \valid_read(message);
+ requires
+ valid_msg_iov:
+ \valid_read(message->msg_iov + (0 .. message->msg_iovlen - 1));
+ ensures error_or_chars_sent: \result ≡ -1 ∨ 0 ≤ \result;
+ assigns __fc_sockfds[sockfd], \result;
+ assigns __fc_sockfds[sockfd]
+ \from __fc_sockfds[sockfd], (indirect: *message),
+ (indirect: *(message->msg_iov + (0 .. message->msg_iovlen - 1))),
+ (indirect: flags);
+ assigns \result
+ \from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]),
+ (indirect: *message),
+ (indirect: *(message->msg_iov + (0 .. message->msg_iovlen - 1)));
+ */
+extern ssize_t sendmsg(int sockfd, struct msghdr const *message, int flags);
+
/*@ requires available_sockfd: 0 ≤ sockfd < 1024;
requires buf_len_ok: \valid_read((char *)buf + (0 .. len - 1));
ensures
diff --git a/tests/libc/oracle/socket_h.res.oracle b/tests/libc/oracle/socket_h.res.oracle
index 1b50d5781ffd4b976d3805c528190ddde6247bf0..f46e7a13fd1552f6249cbd35da7871aa2c345fd1 100644
--- a/tests/libc/oracle/socket_h.res.oracle
+++ b/tests/libc/oracle/socket_h.res.oracle
@@ -82,7 +82,7 @@
[eva] socket_h.c:31:
function recvfrom: precondition 'valid_buffer_length' got status valid.
[eva] socket_h.c:31:
- function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
+ function recvfrom: precondition 'valid_addrbuf_or_null,initialization' got status valid.
[eva] Done for function recvfrom
[eva] socket_h.c:35: assertion got status valid.
[eva] computing for function recvfrom <- main.
@@ -92,7 +92,7 @@
[eva] socket_h.c:37:
function recvfrom: precondition 'valid_buffer_length' got status valid.
[eva] socket_h.c:37:
- function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
+ function recvfrom: precondition 'valid_addrbuf_or_null,initialization' got status valid.
[eva:invalid-assigns] socket_h.c:37:
Completely invalid destination for assigns clause *addrbuf_len. Ignoring.
[eva:invalid-assigns] socket_h.c:37:
diff --git a/tests/libc/oracle/sys_socket_h.res.oracle b/tests/libc/oracle/sys_socket_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bd668507be702ce8fb2db931063de1a8cea31f2a
--- /dev/null
+++ b/tests/libc/oracle/sys_socket_h.res.oracle
@@ -0,0 +1,65 @@
+[kernel] Parsing sys_socket_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
+ dest ∈ [--..--]
+ v ∈ [--..--]
+[eva] sys_socket_h.c:26: Call to builtin strlen
+[eva] sys_socket_h.c:26:
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function socket <- main.
+ Called from sys_socket_h.c:40.
+[eva] using specification for function socket
+[eva] Done for function socket
+[eva] computing for function sendmsg <- main.
+ Called from sys_socket_h.c:42.
+[eva] using specification for function sendmsg
+[eva] sys_socket_h.c:42:
+ function sendmsg: precondition 'available_sockfd' got status valid.
+[eva] sys_socket_h.c:42:
+ function sendmsg: precondition 'valid_message' got status valid.
+[eva] sys_socket_h.c:42:
+ function sendmsg: precondition 'valid_msg_iov' got status valid.
+[eva] Done for function sendmsg
+[eva] sys_socket_h.c:43: assertion 'valid' got status valid.
+[eva] computing for function sendmsg <- main.
+ Called from sys_socket_h.c:47.
+[eva] sys_socket_h.c:47:
+ function sendmsg: precondition 'available_sockfd' got status valid.
+[eva] sys_socket_h.c:47:
+ function sendmsg: precondition 'valid_message' got status valid.
+[eva:alarm] sys_socket_h.c:47: Warning:
+ function sendmsg: precondition 'valid_msg_iov' got status invalid.
+[eva] Done for function sendmsg
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_sockfds[0..1023] ∈ [--..--]
+ __fc_socket_counter ∈ [--..--]
+ d1 ∈ {{ "message" }}
+ s1.a ∈ {42}
+ .b ∈ {65}
+ .[bits 40 to 63] ∈ {0}
+ s2.p ∈ {0}
+ .d ∈ {3.125}
+ n ∈ {501}
+ d ∈ {5.5}
+ iov[0].iov_base ∈ {{ "message" }}
+ [0].iov_len ∈ {7}
+ [1].iov_base ∈ {{ (void *)&s1 }}
+ [1].iov_len ∈ {8}
+ [2].iov_base ∈ {{ (void *)&s2 }}
+ [2].iov_len ∈ {12}
+ [3].iov_base ∈ {{ (void *)&n }}
+ [3].iov_len ∈ {4}
+ [4].iov_base ∈ {{ (void *)&d }}
+ [4].iov_len ∈ {8}
+ msg{.msg_name; .msg_namelen} ∈ {0}
+ .msg_iov ∈ {{ &iov[0] }}
+ .msg_iovlen ∈ {5; 6}
+ {.msg_control; .msg_controllen; .msg_flags} ∈ UNINITIALIZED
+ sockfd ∈ [-1..1023]
+ r ∈ [-1..2147483647]
+ __retres ∈ {0; 1}
diff --git a/tests/libc/sys_socket_h.c b/tests/libc/sys_socket_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..77aeabb54afb2eb690f4cfdd5df1149aed570a9d
--- /dev/null
+++ b/tests/libc/sys_socket_h.c
@@ -0,0 +1,51 @@
+#include <sys/socket.h>
+#include <netinet/in.h>
+#include <string.h>
+
+struct s1 {
+ int a;
+ char b;
+};
+
+struct s2 {
+ int *p;
+ double d;
+};
+
+volatile struct sockaddr_in dest;
+volatile int v;
+
+int main() {
+ char *d1 = "message";
+ struct s1 s1 = {42, 'A'};
+ struct s2 s2 = {0, 3.125};
+ int n = 501;
+ double d = 5.5;
+ struct iovec iov[5];
+ iov[0].iov_base = d1;
+ iov[0].iov_len = strlen(d1);
+ iov[1].iov_base = &s1;
+ iov[1].iov_len = sizeof(struct s1);
+ iov[2].iov_base = &s2;
+ iov[2].iov_len = sizeof(struct s2);
+ iov[3].iov_base = &n;
+ iov[3].iov_len = sizeof(int);
+ iov[4].iov_base = &d;
+ iov[4].iov_len = sizeof(double);
+ struct msghdr msg;
+ msg.msg_name = 0;
+ msg.msg_namelen = 0;
+ msg.msg_iov = iov;
+ msg.msg_iovlen = 5;
+ int sockfd = socket(AF_INET, SOCK_STREAM, 0);
+ if (sockfd < 0) return 1;
+ int r = sendmsg(sockfd, &msg, 0);
+ //@ assert valid: r == -1 || r >= 0;
+
+ msg.msg_iovlen = 6; // invalid length
+ if (v) {
+ sendmsg(sockfd, &msg, 0); // must fail
+ //@ assert unreachable: \false;
+ }
+ return 0;
+}
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
index 8a649c6d13357fbe4cfde951f36879f8c534a506..7acca29f4fea0e177826075be8ee65194383e8da 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -88,6 +88,7 @@
{ "isspace": { "calls": 0, "address_taken": false } },
{ "isupper": { "calls": 0, "address_taken": false } },
{ "isxdigit": { "calls": 0, "address_taken": false } },
+ { "link": { "calls": 0, "address_taken": false } },
{ "lseek": { "calls": 0, "address_taken": false } },
{ "pathconf": { "calls": 0, "address_taken": false } },
{ "pclose": { "calls": 0, "address_taken": false } },