diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index f440e7fba8c91ba66bd5b4874b992a93aa9c5735..ddd988809200e62411824aaa1f6319b035b23287 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 5979b51c4d998f8883c3d332861a36a51cd86688..4dd08614227cf0105780abb9016bf80b60a1e613 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 96ad940d69778adf1aee7a90d46c4d25b63c46c2..e6cd5c1976c5f1ee699bb4d9bc33852458d258ef 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 566c5af75a06db659d7b28cacb1c2f2a69a9640d..4ada2331e0413447eb3e48baaf2895c7e2c5edd6 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3098,6 +3098,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;
@@ -3218,7 +3228,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);
@@ -4772,7 +4782,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);
@@ -4854,6 +4864,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 de14067e7a65d53a82dd943adb71c6cb31536f68..4216280930594e36a24f4db3ea2baca79bd5ee12 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -87,6 +87,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 } },