[kernel] Parsing tests/libc/netdb_c.c (with preprocessing)
[eva] Splitting return states on:
  \return(tmpfile) == 0 (auto)
  \return(tmpnam) == 0 (auto)
  \return(fopen) == 0 (auto)
  \return(fdopen) == 0 (auto)
  \return(freopen) == 0 (auto)
  \return(fgets) == 0 (auto)
  \return(gets) == 0 (auto)
  \return(popen) == 0 (auto)
  \return(seed48) == 0 (auto)
  \return(calloc) == 0 (auto)
  \return(malloc) == 0 (auto)
  \return(realloc) == 0 (auto)
  \return(getenv) == 0 (auto)
  \return(bsearch) == 0 (auto)
  \return(getcwd) == 0 (auto)
  \return(ttyname) == 0 (auto)
  \return(memchr) == 0 (auto)
  \return(memcpy) == 0 (auto)
  \return(memmove) == 0 (auto)
  \return(memset) == 0 (auto)
  \return(strchr) == 0 (auto)
  \return(strrchr) == 0 (auto)
  \return(strpbrk) == 0 (auto)
  \return(strstr) == 0 (auto)
  \return(strcasestr) == 0 (auto)
  \return(strtok) == 0 (auto)
  \return(strtok_r) == 0 (auto)
  \return(strsep) == 0 (auto)
  \return(strerror) == 0 (auto)
  \return(strcpy) == 0 (auto)
  \return(strncpy) == 0 (auto)
  \return(stpcpy) == 0 (auto)
  \return(strcat) == 0 (auto)
  \return(strncat) == 0 (auto)
  \return(strdup) == 0 (auto)
  \return(strndup) == 0 (auto)
  \return(strsignal) == 0 (auto)
  \return(bind) == 0 (auto)
  \return(socket) == -1 (auto)
  \return(signal) == 0 (auto)
  \return(inet_addr) == 4294967295 (auto)
  \return(inet_ntoa) == 0 (auto)
  \return(inet_ntop) == 0 (auto)
  \return(gai_strerror) == 0 (auto)
  \return(getaddrinfo) == 0 (auto)
  \return(gethostbyname) == 0 (auto)
  \return(Frama_C_nondet) == 0 (auto)
  \return(Frama_C_nondet_ptr) == 0 (auto)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva] tests/libc/netdb_c.c:33: Call to builtin memset
[eva] tests/libc/netdb_c.c:33: 
  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] computing for function getaddrinfo <- main.
  Called from tests/libc/netdb_c.c:42.
[eva] share/libc/netdb.c:56: Call to builtin malloc
[eva] share/libc/netdb.c:56: allocating variable __malloc_getaddrinfo_l56
[eva] share/libc/netdb.c:58: Call to builtin malloc
[eva] share/libc/netdb.c:58: allocating variable __malloc_getaddrinfo_l58
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:60.
[eva] using specification for function Frama_C_interval
[eva] share/libc/netdb.c:60: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] share/libc/netdb.c:63: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:63.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:68.
[eva] share/libc/netdb.c:68: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- getaddrinfo <- main.
  Called from share/libc/netdb.c:69.
[eva] share/libc/netdb.c:69: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] Recording results for getaddrinfo
[eva] Done for function getaddrinfo
[eva] computing for function gai_strerror <- main.
  Called from tests/libc/netdb_c.c:44.
[eva] using specification for function gai_strerror
[eva] Done for function gai_strerror
[eva] computing for function fprintf_va_1 <- main.
  Called from tests/libc/netdb_c.c:44.
[eva] using specification for function fprintf_va_1
[eva] tests/libc/netdb_c.c:44: 
  function fprintf_va_1: precondition valid_read_string(format) got status valid.
[eva] tests/libc/netdb_c.c:44: 
  function fprintf_va_1: precondition valid_read_string(param0) got status valid.
[eva] Done for function fprintf_va_1
[eva] computing for function exit <- main.
  Called from tests/libc/netdb_c.c:45.
[eva] using specification for function exit
[eva] Done for function exit
[eva] computing for function socket <- main.
  Called from tests/libc/netdb_c.c:54.
[eva] using specification for function socket
[eva] Done for function socket
[eva] computing for function bind <- main.
  Called from tests/libc/netdb_c.c:59.
[eva] using specification for function bind
[eva] tests/libc/netdb_c.c:59: 
  function bind: precondition 'valid_sockfd,sockfd' got status valid.
[eva] tests/libc/netdb_c.c:59: 
  function bind: precondition 'valid_read_addr' got status valid.
[eva] Done for function bind
[eva] computing for function close <- main.
  Called from tests/libc/netdb_c.c:62.
[eva] using specification for function close
[eva] tests/libc/netdb_c.c:62: 
  function close: precondition 'valid_fd' got status valid.
[eva] Done for function close
[eva] computing for function fprintf_va_2 <- main.
  Called from tests/libc/netdb_c.c:65.
[eva] using specification for function fprintf_va_2
[eva] tests/libc/netdb_c.c:65: 
  function fprintf_va_2: precondition got status valid.
[eva] Done for function fprintf_va_2
[eva] computing for function exit <- main.
  Called from tests/libc/netdb_c.c:66.
[eva] Done for function exit
[eva] computing for function freeaddrinfo <- main.
  Called from tests/libc/netdb_c.c:69.
[eva] using specification for function freeaddrinfo
[eva] tests/libc/netdb_c.c:69: Warning: ignoring unsupported \allocates clause
[eva] tests/libc/netdb_c.c:69: 
  function freeaddrinfo: precondition 'addrinfo_valid' got status valid.
[eva] Done for function freeaddrinfo
[eva] computing for function gethostbyname <- main.
  Called from tests/libc/netdb_c.c:71.
[eva] computing for function res_search <- gethostbyname <- main.
  Called from share/libc/netdb.c:139.
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] using specification for function Frama_C_char_interval
[eva] share/libc/netdb.c:97: 
  function Frama_C_char_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_char_interval
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] Done for function Frama_C_char_interval
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] Done for function Frama_C_char_interval
[eva] share/libc/netdb.c:96: starting to merge loop iterations
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] Done for function Frama_C_char_interval
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] Done for function Frama_C_char_interval
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] Done for function Frama_C_char_interval
[eva] computing for function Frama_C_char_interval <- res_search <- 
                          gethostbyname <- main.
  Called from share/libc/netdb.c:97.
[eva] Done for function Frama_C_char_interval
[eva] computing for function Frama_C_interval <- res_search <- gethostbyname <- 
                          main.
  Called from share/libc/netdb.c:100.
[eva] share/libc/netdb.c:100: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] Recording results for res_search
[eva] Done for function res_search
[eva] computing for function Frama_C_nondet <- gethostbyname <- main.
  Called from share/libc/netdb.c:142.
[eva] using specification for function Frama_C_nondet
[eva] Done for function Frama_C_nondet
[eva] computing for function inet_addr <- gethostbyname <- main.
  Called from share/libc/netdb.c:145.
[eva] using specification for function inet_addr
[eva] share/libc/netdb.c:145: 
  function inet_addr: precondition 'valid_arg' got status valid.
[eva] Done for function inet_addr
[eva] share/libc/netdb.c:146: Call to builtin memcpy
[eva] share/libc/netdb.c:146: 
  function memcpy: precondition 'valid_dest' got status valid.
[eva] share/libc/netdb.c:146: 
  function memcpy: precondition 'valid_src' got status valid.
[eva] share/libc/netdb.c:146: 
  function memcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:98: 
  cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] computing for function strncpy <- gethostbyname <- main.
  Called from share/libc/netdb.c:147.
[eva] using specification for function strncpy
[eva] share/libc/netdb.c:147: 
  function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] share/libc/netdb.c:147: 
  function strncpy: precondition 'room_nstring' got status valid.
[eva] share/libc/netdb.c:147: 
  function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:367: 
  cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strncpy
[eva] Recording results for gethostbyname
[eva] Done for function gethostbyname
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function getaddrinfo:
  __fc_errno ∈ [--..--]
  __fc_heap_status ∈ [--..--]
  Frama_C_entropy_source ∈ [--..--]
  result ∈ {{ &__malloc_getaddrinfo_l56 }} or UNINITIALIZED
  __retres ∈ [-11..0]
  __malloc_getaddrinfo_l56.ai_flags ∈ {0} or UNINITIALIZED
                          .ai_family ∈ [0..43] or UNINITIALIZED
                          .ai_socktype ∈
                          {0; 1; 2; 3; 4; 5} or UNINITIALIZED
                          .ai_protocol ∈ [0..256] or UNINITIALIZED
                          .ai_addrlen ∈ {16} or UNINITIALIZED
                          .ai_addr ∈
                          {{ &__malloc_getaddrinfo_l58 }} or UNINITIALIZED
                          .ai_canonname ∈ {{ "dummy" }} or UNINITIALIZED
                          .ai_next ∈ {0} or UNINITIALIZED
  __malloc_getaddrinfo_l58.sa_family ∈ [0..43]
                          .sa_data[0..13] ∈ [--..--]
[eva:final-states] Values at end of function res_search:
  Frama_C_entropy_source ∈ [--..--]
  buf[0..1] ∈ [--..--]
     [2..126] ∈ [--..--] or UNINITIALIZED
     [127] ∈ {0}
[eva:final-states] Values at end of function gethostbyname:
  Frama_C_entropy_source ∈ [--..--]
  __fc_ghbn.host.h_name ∈ {{ NULL ; &__fc_ghbn.hostbuf[0] }}
           .host.h_aliases ∈ {{ NULL ; &__fc_ghbn.host_aliases[0] }}
           .host.h_addrtype ∈ {2}
           .host.h_length ∈ {4}
           .host.h_addr_list ∈ {{ NULL ; &__fc_ghbn.h_addr_ptrs[0] }}
           .host_addr[0..3] ∈ [--..--]
           .h_addr_ptrs[0] ∈ {{ NULL ; (char *)&__fc_ghbn.host_addr }}
           {.h_addr_ptrs[1..2]; .host_aliases[0..1]} ∈ {0}
           .hostbuf[0..126] ∈ [--..--]
           .hostbuf[127] ∈ {0}
  buf[0..1] ∈ [--..--]
     [2..126] ∈ [--..--] or UNINITIALIZED
     [127] ∈ {0}
  n ∈ [-1..128]
  __retres ∈ {{ NULL ; &__fc_ghbn.host }}
[eva:final-states] Values at end of function main:
  __fc_errno ∈ [--..--]
  __fc_heap_status ∈ [--..--]
  Frama_C_entropy_source ∈ [--..--]
  __fc_fds[0..1023] ∈ {0}
  __fc_sockfds[0..1023] ∈ [--..--]
  __fc_socket_counter ∈ [--..--]
  __fc_ghbn.host.h_name ∈ {{ NULL ; &__fc_ghbn.hostbuf[0] }}
           .host.h_aliases ∈ {{ NULL ; &__fc_ghbn.host_aliases[0] }}
           .host.h_addrtype ∈ {2}
           .host.h_length ∈ {4}
           .host.h_addr_list ∈ {{ NULL ; &__fc_ghbn.h_addr_ptrs[0] }}
           .host_addr[0..3] ∈ [--..--]
           .h_addr_ptrs[0] ∈ {{ NULL ; (char *)&__fc_ghbn.host_addr }}
           {.h_addr_ptrs[1..2]; .host_aliases[0..1]} ∈ {0}
           .hostbuf[0..126] ∈ [--..--]
           .hostbuf[127] ∈ {0}
  hints.ai_flags ∈ {1}
       .ai_family ∈ {0}
       .ai_socktype ∈ {2}
       {.ai_protocol; .ai_addrlen; .ai_addr; .ai_canonname; .ai_next} ∈ {0}
  result ∈ {{ &__malloc_getaddrinfo_l56 }}
  rp ∈ {{ &__malloc_getaddrinfo_l56 }}
  sfd ∈ [0..1023]
  s ∈ {0}
  addr ∈ {{ "localhost" }}
  h ∈ {{ NULL ; &__fc_ghbn.host }}
  __retres ∈ {0}
  S___fc_stderr[0..1] ∈ [--..--]
  __malloc_getaddrinfo_l56.ai_flags ∈ {0}
                          .ai_family ∈ [0..43]
                          .ai_socktype ∈ {0; 1; 2; 3; 4; 5}
                          .ai_protocol ∈ [0..256]
                          .ai_addrlen ∈ {16}
                          .ai_addr ∈ {{ &__malloc_getaddrinfo_l58 }}
                          .ai_canonname ∈ {{ "dummy" }}
                          .ai_next ∈ {0}
  __malloc_getaddrinfo_l58.sa_family ∈ [0..43]
                          .sa_data[0..13] ∈ [--..--]