-
Andre Maroneze authoredAndre Maroneze authored
socket.0.res.oracle 12.96 KiB
[kernel] Parsing tests/libc/socket.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
sent_msg ∈ {{ "World" }}
rcv_buffer[0..9] ∈ {0}
socket_fd[0..1] ∈ {0}
nondet ∈ [--..--]
[eva] computing for function init_sockets <- main.
Called from tests/libc/socket.c:125.
[eva] computing for function socketpair <- init_sockets <- main.
Called from tests/libc/socket.c:50.
[eva] using specification for function socketpair
[eva] tests/libc/socket.c:50:
function socketpair: precondition 'valid_socket_sector' got status valid.
[eva] Done for function socketpair
[eva] computing for function fprintf_va_1 <- init_sockets <- main.
Called from tests/libc/socket.c:52.
[eva] using specification for function fprintf_va_1
[eva] tests/libc/socket.c:52:
function fprintf_va_1: precondition got status valid.
[eva] Done for function fprintf_va_1
[eva] computing for function exit <- init_sockets <- main.
Called from tests/libc/socket.c:53.
[eva] using specification for function exit
[eva] Done for function exit
[eva] tests/libc/socket.c:55: assertion got status valid.
[eva] Recording results for init_sockets
[eva] Done for function init_sockets
[eva] computing for function test_read <- main.
Called from tests/libc/socket.c:126.
[eva] computing for function init_reception <- test_read <- main.
Called from tests/libc/socket.c:60.
[eva] computing for function bzero <- init_reception <- test_read <- main.
Called from tests/libc/socket.c:43.
[eva] using specification for function bzero
[eva] tests/libc/socket.c:43:
function bzero: precondition 'valid_memory_area' got status valid.
[eva] Done for function bzero
[eva] computing for function write <- init_reception <- test_read <- main.
Called from tests/libc/socket.c:44.
[eva] using specification for function write
[eva] tests/libc/socket.c:44:
function write: precondition 'valid_fd' got status valid.
[eva] tests/libc/socket.c:44:
function write: precondition 'buf_has_room' got status valid.
[eva] Done for function write
[eva] Recording results for init_reception
[eva] Done for function init_reception
[eva] computing for function read <- test_read <- main.
Called from tests/libc/socket.c:61.
[eva] using specification for function read
[eva] tests/libc/socket.c:61:
function read: precondition 'valid_fd' got status valid.
[eva] tests/libc/socket.c:61:
function read: precondition 'buf_has_room' got status valid.
[eva] Done for function read
[eva] computing for function printf_va_1 <- test_read <- main.
Called from tests/libc/socket.c:62.
[eva] using specification for function printf_va_1
[eva] tests/libc/socket.c:62:
function printf_va_1: precondition valid_read_string(format) got status valid.
[eva:alarm] tests/libc/socket.c:62: Warning:
function printf_va_1: precondition valid_read_string(param0) got status unknown.
[eva] Done for function printf_va_1
[eva] Recording results for test_read
[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] 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 ..));'
[eva] Done for function readv
[eva:alarm] tests/libc/socket.c:72: Warning:
accessing uninitialized left-value.
assert \initialized((char *)rcv_buffer_scattered1);
[eva] computing for function printf_va_2 <- test_readv <- main.
Called from tests/libc/socket.c:75.
[eva] using specification for function printf_va_2
[eva] tests/libc/socket.c:75:
function printf_va_2: precondition valid_read_string(format) got status valid.
[eva:alarm] tests/libc/socket.c:75: Warning:
function printf_va_2: precondition valid_read_nstring(param1, 3) got status unknown.
[eva:alarm] tests/libc/socket.c:75: Warning:
function printf_va_2: precondition valid_read_nstring(param0, 2) got status unknown.
[eva] Done for function printf_va_2
[eva] Recording results for test_readv
[eva] Done for function test_readv
[eva] computing for function test_recvmsg <- main.
Called from tests/libc/socket.c:128.
[eva] tests/libc/socket.c:82: Reusing old results for call to init_reception
[eva] computing for function recvmsg <- test_recvmsg <- main.
Called from tests/libc/socket.c:90.
[eva] using specification for function recvmsg
[eva] tests/libc/socket.c:90:
function recvmsg: precondition 'valid_sockfd' got status valid.
[eva] tests/libc/socket.c:90:
function recvmsg: precondition 'msg_control_has_room' got status valid.
[eva] tests/libc/socket.c:90:
function recvmsg: precondition 'msg_iov_has_room' got status valid.
[eva] tests/libc/socket.c:90:
function recvmsg: precondition 'msg_name_null_or_has_room' got status valid.
[eva] Done for function recvmsg
[eva:alarm] tests/libc/socket.c:92: Warning:
accessing uninitialized left-value.
assert \initialized((char *)rcv_buffer_scattered1);
[eva] computing for function printf_va_3 <- test_recvmsg <- main.
Called from tests/libc/socket.c:95.
[eva] using specification for function printf_va_3
[eva] tests/libc/socket.c:95:
function printf_va_3: precondition valid_read_string(format) got status valid.
[eva:alarm] tests/libc/socket.c:95: Warning:
function printf_va_3: precondition valid_read_nstring(param1, 3) got status unknown.
[eva:alarm] tests/libc/socket.c:95: Warning:
function printf_va_3: precondition valid_read_nstring(param0, 2) got status unknown.
[eva] Done for function printf_va_3
[eva] Recording results for test_recvmsg
[eva] Done for function test_recvmsg
[eva] computing for function test_server_echo <- main.
Called from tests/libc/socket.c:129.
[eva] computing for function socket <- test_server_echo <- main.
Called from tests/libc/socket.c:100.
[eva] using specification for function socket
[eva] Done for function socket[eva] computing for function memset <- test_server_echo <- main.
Called from tests/libc/socket.c:103.
[eva] using specification for function memset
[eva] tests/libc/socket.c:103:
function memset: precondition 'valid_s' got status valid.
[eva] share/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] Done for function memset
[eva] computing for function bind <- test_server_echo <- main.
Called from tests/libc/socket.c:107.
[eva] using specification for function bind
[eva] tests/libc/socket.c:107:
function bind: precondition 'valid_sockfd,sockfd' got status valid.
[eva] tests/libc/socket.c:107:
function bind: precondition 'valid_read_addr' got status valid.
[eva] Done for function bind
[eva] computing for function listen <- test_server_echo <- main.
Called from tests/libc/socket.c:108.
[eva] using specification for function listen
[eva] tests/libc/socket.c:108:
function listen: precondition 'valid_sockfd' got status valid.
[eva] Done for function listen
[eva] computing for function accept <- test_server_echo <- main.
Called from tests/libc/socket.c:111.
[eva] using specification for function accept
[eva] tests/libc/socket.c:111:
function accept: precondition 'valid_sockfd' got status valid.
[eva] tests/libc/socket.c:111:
function accept, behavior addr_null: assumes got status invalid; behavior not evaluated.
[eva] tests/libc/socket.c:111:
function accept, behavior addr_not_null: precondition 'valid_addrlen' got status valid.
[eva] tests/libc/socket.c:111:
function accept, behavior addr_not_null: precondition 'addr_has_room' got status valid.
[eva] Done for function accept
[eva] computing for function accept <- test_server_echo <- main.
Called from tests/libc/socket.c:112.
[eva] tests/libc/socket.c:112:
function accept: precondition 'valid_sockfd' got status valid.
[eva] tests/libc/socket.c:112:
function accept, behavior addr_not_null: assumes got status invalid; behavior not evaluated.
[eva] tests/libc/socket.c:112:
function accept, behavior addr_null: precondition 'addrlen_should_be_null' got status valid.
[eva] Done for function accept
[eva] computing for function read <- test_server_echo <- main.
Called from tests/libc/socket.c:115.
[eva] tests/libc/socket.c:115:
function read: precondition 'valid_fd' got status valid.
[eva] tests/libc/socket.c:115:
function read: precondition 'buf_has_room' got status valid.
[eva] Done for function read
[eva] computing for function write <- test_server_echo <- main.
Called from tests/libc/socket.c:117.
[eva] tests/libc/socket.c:117:
function write: precondition 'valid_fd' got status valid.
[eva] tests/libc/socket.c:117:
function write: precondition 'buf_has_room' got status valid.
[eva] Done for function write
[eva] computing for function close <- test_server_echo <- main.
Called from tests/libc/socket.c:118.
[eva] using specification for function close
[eva] tests/libc/socket.c:118:
function close: precondition 'valid_fd' got status valid.
[eva] Done for function close
[eva] computing for function close <- test_server_echo <- main.
Called from tests/libc/socket.c:119.
[eva] tests/libc/socket.c:119:
function close: precondition 'valid_fd' got status valid.
[eva] Done for function close
[eva] Recording results for test_server_echo
[eva] Done for function test_server_echo[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_sockets:
__fc_socket_counter ∈ [--..--]
socket_fd[0..1] ∈ [0..1023]
S___fc_stderr[0..1] ∈ [--..--]
[eva:final-states] Values at end of function init_reception:
__fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
[eva:final-states] Values at end of function test_read:
__fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ [--..--]
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_readv:
__fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
rcv_buffer_scattered1[0] ∈ [--..--]
[1] ∈ [--..--] or UNINITIALIZED
rcv_buffer_scattered2[0..4] ∈ [--..--] or UNINITIALIZED
rcv_buffer_scattered3[0..2] ∈ [--..--] or UNINITIALIZED
rcv_buffer_scattered_iovec[0].iov_base ∈
{{ (void *)&rcv_buffer_scattered1 }}
[0].iov_len ∈ {2}
[1].iov_base ∈
{{ (void *)&rcv_buffer_scattered2 }}
[1].iov_len ∈ {5}
[2].iov_base ∈
{{ (void *)&rcv_buffer_scattered3 }}
[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] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
rcv_buffer_scattered1[0] ∈ [--..--]
[1] ∈ [--..--] or UNINITIALIZED
rcv_buffer_scattered2[0..4] ∈ [--..--] or UNINITIALIZED
rcv_buffer_scattered3[0..2] ∈ [--..--] or UNINITIALIZED
rcv_buffer_scattered_iovec[0].iov_base ∈
{{ (void *)&rcv_buffer_scattered1 }}
[0].iov_len ∈ {2}
[1].iov_base ∈
{{ (void *)&rcv_buffer_scattered2 }}
[1].iov_len ∈ {5}
[2].iov_base ∈
{{ (void *)&rcv_buffer_scattered3 }}
[2].iov_len ∈ {3}
hdr.msg_name ∈ {0}
.msg_namelen ∈ [--..--]
.msg_iov ∈ {{ &rcv_buffer_scattered_iovec[0] }}
.msg_iovlen ∈ {3}
.msg_control ∈ {0}
.msg_controllen ∈ [--..--]
.msg_flags ∈ [--..--] or UNINITIALIZED
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_server_echo:
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
__fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
addrlen ∈ {8}
client_fd ∈ [-1..1023]
buf[0..63] ∈ [--..--] or UNINITIALIZED
r ∈ [-1..64]
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
__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}
__retres ∈ {0}
S___fc_stderr[0..1] ∈ [--..--]
S___fc_stdout[0..1] ∈ [--..--]