Commit 37f8ca70 authored by David Bühler's avatar David Bühler
Browse files

Merge branch 'feature/andre/libc-sendto-recvfrom' into 'master'

[Libc] add specs for sendto and recvfrom

See merge request frama-c/frama-c!2872
parents ca9c296b f7019816
......@@ -443,8 +443,29 @@ extern int listen(int sockfd, int backlog);
*/
extern ssize_t recv(int sockfd, void * buf, size_t len, int flags);
extern ssize_t recvfrom(int, void *, size_t, int,
struct sockaddr *, socklen_t *);
/*@
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) &&
\initialized(addrbuf_len) &&
\valid((char *)addrbuf+(0 .. *addrbuf_len-1)))
|| (addrbuf == \null && addrbuf_len == \null);
assigns *((char *)buf+(0 .. len-1)), __fc_sockfds[sockfd], \result
\from sockfd, len, flags, __fc_sockfds[sockfd];
assigns *addrbuf_len \from indirect:sockfd, indirect: len,
indirect:flags, __fc_sockfds[sockfd];
assigns *((char *)addrbuf+(0 .. \old(*addrbuf_len)-1))
\from indirect:sockfd, indirect: len,
indirect:flags, __fc_sockfds[sockfd];
ensures result_error_or_received_length: \result == -1 || 0 <= \result <= len;
ensures initialization:buf: \initialized(((char *)buf+(0 .. \result-1)));
ensures initialization:addrbuf:
addrbuf != \null ==>
\initialized(((char *)addrbuf+(0 .. \old(*addrbuf_len)-1)));
*/
extern ssize_t recvfrom(int sockfd, void *buf, size_t len, int flags,
struct sockaddr *addrbuf, socklen_t *addrbuf_len);
/*@ requires valid_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
@ requires msg_control_has_room:
......@@ -483,8 +504,22 @@ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags);
*/
extern ssize_t send(int sockfd, const void *buf, size_t len, int flags);
extern ssize_t sendmsg(int, const struct msghdr *, int);
extern ssize_t sendto(int, const void *, size_t, int, const struct sockaddr *,
socklen_t);
/*@
requires available_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
requires buf_len_ok: \valid_read(((char*)buf)+(0 .. len - 1));
assigns errno
\from indirect:sockfd, indirect:__fc_sockfds[sockfd],
indirect:((char *)buf)[0..len], flags;
assigns __fc_sockfds[sockfd]
\from __fc_sockfds[sockfd], ((char *)buf)[0..len], flags;
assigns \result
\from indirect:sockfd, indirect:__fc_sockfds[sockfd],
indirect:((char*)buf)[0..len], indirect:flags;
ensures error_or_chars_sent: \result == -1 || 0 <= \result <= len;
*/
extern ssize_t sendto(int sockfd, const void *buf, size_t len, int flags,
const struct sockaddr *address, socklen_t address_len);
/*@
requires valid_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
......
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
[kernel] share/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -41,7 +43,7 @@
wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
wmemcpy (0 call); wmemset (0 call);
Specified-only functions (411)
Specified-only functions (413)
==============================
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);
......@@ -133,38 +135,39 @@
putchar (0 call); putchar_unlocked (0 call); puts (0 call); qsort (0 call);
quick_exit (0 call); raise (0 call); rand (0 call); random (0 call);
read (0 call); readdir (0 call); readv (0 call); realloc (3 calls);
recv (0 call); recvmsg (0 call); remove (0 call); rename (0 call);
rewind (0 call); round (0 call); roundf (0 call); roundl (0 call);
seed48 (0 call); select (0 call); send (0 call); setbuf (0 call);
setegid (0 call); seteuid (0 call); setgid (0 call); sethostname (0 call);
setitimer (0 call); setjmp (0 call); setlogmask (0 call); setpgid (0 call);
setpriority (0 call); setregid (0 call); setresgid (0 call);
setresuid (0 call); setreuid (0 call); setrlimit (0 call); setsid (0 call);
setsockopt (0 call); settimeofday (0 call); setuid (0 call);
setvbuf (0 call); shutdown (0 call); sigaction (0 call); sigaddset (0 call);
sigdelset (0 call); sigemptyset (0 call); sigfillset (0 call);
sigismember (0 call); siglongjmp (0 call); signal (0 call);
sigprocmask (0 call); sin (0 call); sinf (0 call); sinl (0 call);
socket (0 call); socketpair (0 call); sqrt (0 call); sqrtf (0 call);
sqrtl (0 call); srand (0 call); srand48 (0 call); srandom (0 call);
stat (0 call); stpcpy (0 call); strcasestr (0 call); strchrnul (0 call);
strcoll (0 call); strcspn (0 call); strftime (0 call); strlcat (0 call);
strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call); strsep (0 call);
strspn (0 call); strtod (0 call); strtof (0 call); strtoimax (0 call);
strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
umask (0 call); uname (0 call); ungetc (0 call); unlink (0 call);
usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
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);
recv (0 call); recvfrom (0 call); recvmsg (0 call); remove (0 call);
rename (0 call); rewind (0 call); round (0 call); roundf (0 call);
roundl (0 call); seed48 (0 call); select (0 call); send (0 call);
sendto (0 call); setbuf (0 call); setegid (0 call); seteuid (0 call);
setgid (0 call); sethostname (0 call); setitimer (0 call); setjmp (0 call);
setlogmask (0 call); setpgid (0 call); setpriority (0 call);
setregid (0 call); setresgid (0 call); setresuid (0 call);
setreuid (0 call); setrlimit (0 call); setsid (0 call); setsockopt (0 call);
settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
strcasestr (0 call); strchrnul (0 call); strcoll (0 call); strcspn (0 call);
strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
ttyname (0 call); tzset (0 call); umask (0 call); uname (0 call);
ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
waitpid (0 call); wcschr (0 call); 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);
Undefined and unspecified functions (1)
=======================================
......@@ -191,7 +194,7 @@
Goto = 97
Assignment = 459
Exit point = 83
Function = 495
Function = 497
Function call = 93
Pointer dereferencing = 159
Cyclomatic complexity = 296
......
......@@ -3686,6 +3686,40 @@ 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 < 1024;
requires valid_buffer_length: \valid((char *)buf + (0 .. len - 1));
requires
valid_addrbuf_or_null:
(\valid(addrbuf_len) ∧ \initialized(addrbuf_len) ∧
\valid((char *)addrbuf + (0 .. *addrbuf_len - 1))) ∨
(addrbuf ≡ \null ∧ addrbuf_len ≡ \null);
ensures
result_error_or_received_length:
\result ≡ -1 ∨ (0 ≤ \result ≤ \old(len));
ensures
initialization: buf:
\initialized((char *)\old(buf) + (0 .. \result - 1));
ensures
initialization: addrbuf:
\old(addrbuf) ≢ \null ⇒
\initialized((char *)\old(addrbuf) + (0 .. \old(*addrbuf_len) - 1));
assigns *((char *)buf + (0 .. len - 1)), __fc_sockfds[sockfd], \result,
*addrbuf_len, *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1));
assigns *((char *)buf + (0 .. len - 1))
\from sockfd, len, flags, __fc_sockfds[sockfd];
assigns __fc_sockfds[sockfd]
\from sockfd, len, flags, __fc_sockfds[sockfd];
assigns \result \from sockfd, len, flags, __fc_sockfds[sockfd];
assigns *addrbuf_len
\from (indirect: sockfd), (indirect: len), (indirect: flags),
__fc_sockfds[sockfd];
assigns *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1))
\from (indirect: sockfd), (indirect: len), (indirect: flags),
__fc_sockfds[sockfd];
*/
extern ssize_t recvfrom(int sockfd, void *buf, size_t len, int flags,
struct sockaddr *addrbuf, socklen_t *addrbuf_len);
/*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
requires
msg_control_has_room:
......@@ -3737,6 +3771,23 @@ 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 buf_len_ok: \valid_read((char *)buf + (0 .. len - 1));
ensures
error_or_chars_sent: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(len));
assigns __fc_errno, __fc_sockfds[sockfd], \result;
assigns __fc_errno
\from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]),
(indirect: *((char *)buf + (0 .. len))), flags;
assigns __fc_sockfds[sockfd]
\from __fc_sockfds[sockfd], *((char *)buf + (0 .. len)), flags;
assigns \result
\from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]),
(indirect: *((char *)buf + (0 .. len))), (indirect: flags);
*/
extern ssize_t sendto(int sockfd, void const *buf, size_t len, int flags,
struct sockaddr const *address, socklen_t address_len);
/*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
requires
optval_null_or_has_room:
......
......@@ -59,10 +59,52 @@
[eva] tests/libc/socket_h.c:21:
function getsockname: precondition 'valid_address' got status valid.
[eva] Done for function getsockname
[eva] computing for function sendto <- main.
Called from tests/libc/socket_h.c:24.
[eva] using specification for function sendto
[eva] tests/libc/socket_h.c:24:
function sendto: precondition 'available_sockfd' got status valid.
[eva] tests/libc/socket_h.c:24:
function sendto: precondition 'buf_len_ok' got status valid.
[eva] Done for function sendto
[eva] computing for function sendto <- main.
Called from tests/libc/socket_h.c:27.
[eva] tests/libc/socket_h.c:27:
function sendto: precondition 'available_sockfd' got status valid.
[eva] tests/libc/socket_h.c:27:
function sendto: precondition 'buf_len_ok' got status valid.
[eva] Done for function sendto
[eva] computing for function recvfrom <- main.
Called from tests/libc/socket_h.c:31.
[eva] using specification for function recvfrom
[eva] tests/libc/socket_h.c:31:
function recvfrom: precondition 'valid_sockfd' got status valid.
[eva] tests/libc/socket_h.c:31:
function recvfrom: precondition 'valid_buffer_length' got status valid.
[eva] tests/libc/socket_h.c:31:
function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
[eva] Done for function recvfrom
[eva] tests/libc/socket_h.c:35: assertion got status valid.
[eva] computing for function recvfrom <- main.
Called from tests/libc/socket_h.c:37.
[eva] tests/libc/socket_h.c:37:
function recvfrom: precondition 'valid_sockfd' got status valid.
[eva] tests/libc/socket_h.c:37:
function recvfrom: precondition 'valid_buffer_length' got status valid.
[eva] tests/libc/socket_h.c:37:
function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
[eva:invalid-assigns] tests/libc/socket_h.c:37:
Completely invalid destination for assigns clause *addrbuf_len. Ignoring.
[eva:invalid-assigns] tests/libc/socket_h.c:37:
Completely invalid destination
for assigns clause *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1)).
Ignoring.
[eva] Done for function recvfrom
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_errno ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
sockfd ∈ [0..1023]
......@@ -73,3 +115,10 @@
optlen ∈ {4}
addr2 ∈ [--..--] or UNINITIALIZED
socklen ∈ [0..8]
buf[0..39] ∈ [--..--]
sent ∈ {-1; 0; 1; 2; 3}
sent2 ∈ {-1; 0; 1; 2; 3}
recvfrom_addr ∈ [--..--]
recvfrom_addr_len ∈ [--..--]
received ∈ [-1..40]
received2 ∈ [-1..40]
......@@ -19,5 +19,21 @@ int main() {
struct sockaddr_in addr2;
socklen_t socklen = sizeof(addr2);
rc = getsockname(sockfd, (struct sockaddr *)&addr2, &socklen);
char buf[40] = {'a', 'b', 'c'};
ssize_t sent = sendto(sockfd, buf, 3, 0, (struct sockaddr *)&addr,
sizeof(addr));
ssize_t sent2 = sendto(sockfd, buf, 3, 0, 0, 0);
struct sockaddr_in recvfrom_addr;
socklen_t recvfrom_addr_len = sizeof(recvfrom_addr);
ssize_t received = recvfrom(sockfd, buf, sizeof(buf), 0,
(struct sockaddr *)&recvfrom_addr,
&recvfrom_addr_len);
if (received != -1) {
//@ assert \initialized(&recvfrom_addr);
}
ssize_t received2 = recvfrom(sockfd, buf, sizeof(buf), 0, 0, 0);
return rc;
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment