[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] ∈ [--..--]