Skip to content
Snippets Groups Projects
Commit a8493c39 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/andre/libc-socket-consts' into 'master' 

[libc] add missing POSIX constants

See merge request !1156
parents f75d5227 f9cad12c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
share/libc/sys/socket.h
+ 10
− 0
View file @ a8493c39
......@@ -140,6 +140,16 @@ struct msghdr {
#define SOMAXCONN 0xFF
enum {
SHUT_RD,
SHUT_WR,
SHUT_RDWR
};
// POSIX requires these SHUT_* constants to be defined as macros
#define SHUT_RD SHUT_RD
#define SHUT_WR SHUT_WR
#define SHUT_RDWR SHUT_RDWR
#ifndef __FC_MAX_OPEN_SOCKETS
// arbitrary number
#define __FC_MAX_OPEN_SOCKETS 1024
......
tests/libc/oracle/fc_libc.1.res.oracle
+ 4
− 4
View file @ a8493c39
......@@ -138,10 +138,10 @@ struct DIR {
struct dirent **__fc_dir_entries ;
};
typedef struct DIR DIR;
struct __anonstruct_fd_set_5 {
struct __anonstruct_fd_set_6 {
char __fc_fd_set ;
};
typedef struct __anonstruct_fd_set_5 fd_set;
typedef struct __anonstruct_fd_set_6 fd_set;
typedef unsigned int id_t;
typedef unsigned int pid_t;
typedef unsigned long sigset_t;
......@@ -164,11 +164,11 @@ struct timezone {
};
typedef void * iconv_t;
typedef int ( jmp_buf)[5];
struct __anonstruct_sigjmp_buf_13 {
struct __anonstruct_sigjmp_buf_14 {
jmp_buf buf ;
sigset_t sigs ;
};
typedef struct __anonstruct_sigjmp_buf_13 sigjmp_buf;
typedef struct __anonstruct_sigjmp_buf_14 sigjmp_buf;
struct _code {
char const *c_name ;
int c_val ;
......
tests/libc/oracle/socket.0.res.oracle
+ 12
− 12
View file @ a8493c39
......@@ -41,7 +41,7 @@
[value] computing for function socketpair <- init_sockets <- main.
Called from tests/libc/socket.c:50.
[value] using specification for function socketpair
share/libc/sys/socket.h:326:[value] function socketpair: precondition got status valid.
share/libc/sys/socket.h:336:[value] function socketpair: precondition got status valid.
[value] Done for function socketpair
[value] computing for function fprintf <- init_sockets <- main.
Called from tests/libc/socket.c:52.
......@@ -118,10 +118,10 @@ tests/libc/socket.c:72:[value] warning: accessing uninitialized left-value.
[value] computing for function recvmsg <- test_recvmsg <- main.
Called from tests/libc/socket.c:90.
[value] using specification for function recvmsg
share/libc/sys/socket.h:273:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:274:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:275:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:276:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:283:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:284:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:285:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:286:[value] function recvmsg: precondition got status valid.
[value] Done for function recvmsg
tests/libc/socket.c:92:[value] warning: accessing uninitialized left-value.
assert \initialized((char *)rcv_buffer_scattered1);
......@@ -145,26 +145,26 @@ tests/libc/socket.c:103:[value] cannot evaluate ACSL term, unsupported ACSL cons
[value] computing for function bind <- test_server_echo <- main.
Called from tests/libc/socket.c:107.
[value] using specification for function bind
share/libc/sys/socket.h:181:[value] function bind: precondition got status valid.
share/libc/sys/socket.h:182:[value] function bind: precondition got status valid.
share/libc/sys/socket.h:191:[value] function bind: precondition got status valid.
share/libc/sys/socket.h:192:[value] function bind: precondition got status valid.
[value] Done for function bind
[value] computing for function listen <- test_server_echo <- main.
Called from tests/libc/socket.c:108.
[value] using specification for function listen
share/libc/sys/socket.h:247:[value] function listen: precondition got status valid.
share/libc/sys/socket.h:257:[value] function listen: precondition got status valid.
[value] Done for function listen
[value] computing for function accept <- test_server_echo <- main.
Called from tests/libc/socket.c:111.
[value] using specification for function accept
share/libc/sys/socket.h:162:[value] function accept: precondition got status valid.
share/libc/sys/socket.h:172:[value] function accept: precondition got status valid.
tests/libc/socket.c:111:[value] function accept, behavior addr_null: assumes got status invalid; behavior not evaluated.
share/libc/sys/socket.h:172:[value] function accept, behavior addr_not_null: precondition got status valid.
share/libc/sys/socket.h:173:[value] function accept, behavior addr_not_null: precondition got status valid.
share/libc/sys/socket.h:182:[value] function accept, behavior addr_not_null: precondition got status valid.
share/libc/sys/socket.h:183:[value] function accept, behavior addr_not_null: precondition got status valid.
[value] Done for function accept
[value] computing for function accept <- test_server_echo <- main.
Called from tests/libc/socket.c:112.
tests/libc/socket.c:112:[value] function accept, behavior addr_not_null: assumes got status invalid; behavior not evaluated.
share/libc/sys/socket.h:168:[value] function accept, behavior addr_null: precondition got status valid.
share/libc/sys/socket.h:178:[value] function accept, behavior addr_null: precondition got status valid.
tests/libc/socket.c:112:[value] warning: Completely invalid destination for assigns
clause *((char *)addr + (0 .. *addrlen - 1)). Ignoring.
[value] Done for function accept
......
tests/libc/oracle/socket.1.res.oracle
+ 12
− 12
View file @ a8493c39
......@@ -41,7 +41,7 @@
[value] computing for function socketpair <- init_sockets <- main.
Called from tests/libc/socket.c:50.
[value] using specification for function socketpair
share/libc/sys/socket.h:326:[value] function socketpair: precondition got status valid.
share/libc/sys/socket.h:336:[value] function socketpair: precondition got status valid.
[value] Done for function socketpair
[value] computing for function fprintf <- init_sockets <- main.
Called from tests/libc/socket.c:52.
......@@ -118,10 +118,10 @@ tests/libc/socket.c:72:[value] warning: accessing uninitialized left-value.
[value] computing for function recvmsg <- test_recvmsg <- main.
Called from tests/libc/socket.c:90.
[value] using specification for function recvmsg
share/libc/sys/socket.h:273:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:274:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:275:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:276:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:283:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:284:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:285:[value] function recvmsg: precondition got status valid.
share/libc/sys/socket.h:286:[value] function recvmsg: precondition got status valid.
[value] Done for function recvmsg
tests/libc/socket.c:92:[value] warning: accessing uninitialized left-value.
assert \initialized((char *)rcv_buffer_scattered1);
......@@ -145,26 +145,26 @@ tests/libc/socket.c:103:[value] cannot evaluate ACSL term, unsupported ACSL cons
[value] computing for function bind <- test_server_echo <- main.
Called from tests/libc/socket.c:107.
[value] using specification for function bind
share/libc/sys/socket.h:181:[value] function bind: precondition got status valid.
share/libc/sys/socket.h:182:[value] function bind: precondition got status valid.
share/libc/sys/socket.h:191:[value] function bind: precondition got status valid.
share/libc/sys/socket.h:192:[value] function bind: precondition got status valid.
[value] Done for function bind
[value] computing for function listen <- test_server_echo <- main.
Called from tests/libc/socket.c:108.
[value] using specification for function listen
share/libc/sys/socket.h:247:[value] function listen: precondition got status valid.
share/libc/sys/socket.h:257:[value] function listen: precondition got status valid.
[value] Done for function listen
[value] computing for function accept <- test_server_echo <- main.
Called from tests/libc/socket.c:111.
[value] using specification for function accept
share/libc/sys/socket.h:162:[value] function accept: precondition got status valid.
share/libc/sys/socket.h:172:[value] function accept: precondition got status valid.
tests/libc/socket.c:111:[value] function accept, behavior addr_null: assumes got status invalid; behavior not evaluated.
share/libc/sys/socket.h:172:[value] function accept, behavior addr_not_null: precondition got status valid.
share/libc/sys/socket.h:173:[value] function accept, behavior addr_not_null: precondition got status valid.
share/libc/sys/socket.h:182:[value] function accept, behavior addr_not_null: precondition got status valid.
share/libc/sys/socket.h:183:[value] function accept, behavior addr_not_null: precondition got status valid.
[value] Done for function accept
[value] computing for function accept <- test_server_echo <- main.
Called from tests/libc/socket.c:112.
tests/libc/socket.c:112:[value] function accept, behavior addr_not_null: assumes got status invalid; behavior not evaluated.
share/libc/sys/socket.h:168:[value] function accept, behavior addr_null: precondition got status valid.
share/libc/sys/socket.h:178:[value] function accept, behavior addr_null: precondition got status valid.
tests/libc/socket.c:112:[value] warning: Completely invalid destination for assigns
clause *((char *)addr + (0 .. *addrlen - 1)). Ignoring.
[value] Done for function accept
......
tests/libc/oracle/socket_h.res.oracle
+ 7
− 7
View file @ a8493c39
......@@ -36,8 +36,8 @@ share/libc/arpa/inet.h:42:[value] function inet_addr: precondition got status va
[value] computing for function connect <- main.
Called from tests/libc/socket_h.c:13.
[value] using specification for function connect
share/libc/sys/socket.h:192:[value] function connect: precondition got status valid.
share/libc/sys/socket.h:193:[value] function connect: precondition got status valid.
share/libc/sys/socket.h:202:[value] function connect: precondition got status valid.
share/libc/sys/socket.h:203:[value] function connect: precondition got status valid.
[value] Done for function connect
[value] computing for function exit <- main.
Called from tests/libc/socket_h.c:14.
......@@ -45,11 +45,11 @@ share/libc/sys/socket.h:193:[value] function connect: precondition got status va
[value] computing for function getsockopt <- main.
Called from tests/libc/socket_h.c:18.
[value] using specification for function getsockopt
share/libc/sys/socket.h:213:[value] function getsockopt: precondition got status valid.
share/libc/sys/socket.h:214:[value] function getsockopt: precondition got status valid.
share/libc/sys/socket.h:225:[value] function getsockopt, behavior so_error: precondition got status valid.
share/libc/sys/socket.h:226:[value] function getsockopt, behavior so_error: precondition got status valid.
share/libc/sys/socket.h:227:[value] function getsockopt, behavior so_error: precondition got status valid.
share/libc/sys/socket.h:223:[value] function getsockopt: precondition got status valid.
share/libc/sys/socket.h:224:[value] function getsockopt: precondition got status valid.
share/libc/sys/socket.h:235:[value] function getsockopt, behavior so_error: precondition got status valid.
share/libc/sys/socket.h:236:[value] function getsockopt, behavior so_error: precondition got status valid.
share/libc/sys/socket.h:237:[value] function getsockopt, behavior so_error: precondition got status valid.
[value] Done for function getsockopt
[value] Recording results for main
[value] done for function main
......
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