[Libc] add stub for gethostbyname

share/libc/netdb.c

@@ -25,6 +25,7 @@
 #include "netinet/in.h"
 #include "stdlib.h"
 #include "stddef.h"
+#include "string.h"
 #include "errno.h"
 #include "__fc_builtin.h"
 __PUSH_FC_STDLIB
@@ -76,4 +77,84 @@ int getaddrinfo(
   }
 }
 
+#define __FC_MAX_HOST_ADDRS 2
+#define __FC_MAX_HOST_ALIASES 2
+#define __FC_HOSTBUF_SIZE 128
+#define __FC_QUERYBUF_SIZE 128
+struct __fc_gethostbyname {
+  struct hostent host;
+  unsigned char host_addr[sizeof(struct in_addr)];
+  char *h_addr_ptrs[__FC_MAX_HOST_ADDRS + 1];
+  char *host_aliases[__FC_MAX_HOST_ALIASES];
+  char hostbuf[__FC_HOSTBUF_SIZE];
+};
+
+struct __fc_gethostbyname __fc_ghbn;
+
+int res_search(const char *dname, int class, int type,
+               char *answer, int anslen) {
+  for (int i = 0; i < anslen-1; i++) {
+    answer[i] = Frama_C_char_interval(CHAR_MIN, CHAR_MAX);
+  }
+  answer[anslen-1] = 0;
+  return Frama_C_interval(-1, anslen);
+}
+
+struct hostent *gethostbyname(const char *name) {
+  char buf[__FC_QUERYBUF_SIZE];
+  const char *cp;
+  int n;
+  __fc_ghbn.host.h_addrtype = AF_INET;
+  __fc_ghbn.host.h_length = sizeof(struct in_addr);
+
+  // Disallow names consisting only of digits/dots, unless they end in a dot
+  if (*name >= '0' && *name <= '9') {
+    for (cp = name;; ++cp) {
+      if (!*cp) {
+        struct in_addr addr;
+
+        if (*--cp == '.') break;
+
+        // All-numeric, no dot at the end. Fake up a hostent as if we'd actually done a lookup.
+        addr.s_addr = inet_addr(name);
+        if (addr.s_addr == INADDR_NONE) return NULL;
+
+        memcpy(__fc_ghbn.host_addr, &addr, __fc_ghbn.host.h_length);
+        strncpy(__fc_ghbn.hostbuf, name, __FC_HOSTBUF_SIZE - 1);
+        __fc_ghbn.hostbuf[__FC_HOSTBUF_SIZE - 1] = '\0';
+        __fc_ghbn.host.h_name = __fc_ghbn.hostbuf;
+        __fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases;
+        __fc_ghbn.host_aliases[0] = NULL;
+        __fc_ghbn.h_addr_ptrs[0] = (char *) __fc_ghbn.host_addr;
+        __fc_ghbn.h_addr_ptrs[1] = NULL;
+        __fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs;
+
+        return &__fc_ghbn.host;
+      }
+
+      if (*cp < '0' && *cp > '9' && *cp != '.') break;
+    }
+  }
+
+  n = res_search(name, 1, 1, buf, sizeof(buf));
+  if (n < 0) return NULL;
+
+  if (Frama_C_nondet(0, 1)) return NULL;
+  else {
+    struct in_addr addr;
+    addr.s_addr = inet_addr(name);
+    memcpy(__fc_ghbn.host_addr, &addr, __fc_ghbn.host.h_length);
+    strncpy(__fc_ghbn.hostbuf, name, __FC_HOSTBUF_SIZE - 1);
+    __fc_ghbn.hostbuf[__FC_HOSTBUF_SIZE - 1] = '\0';
+    __fc_ghbn.host.h_name = __fc_ghbn.hostbuf;
+    __fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases;
+    __fc_ghbn.host_aliases[0] = NULL;
+    __fc_ghbn.h_addr_ptrs[0] = (char *) __fc_ghbn.host_addr;
+    __fc_ghbn.h_addr_ptrs[1] = NULL;
+    __fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs;
+    return &__fc_ghbn.host;
+  }
+}
+
+
 __POP_FC_STDLIB

tests/libc/netdb_c.c

@@ -68,5 +68,10 @@ int main() {
 
   freeaddrinfo(result);           /* No longer needed */
 
+  struct hostent *h = gethostbyname("localhost");
+  if (h) {
+    char *addrs = h->h_addr;
+    int l = h->h_length;
+  }
   return 0;
 }

tests/libc/oracle/fc_libc.0.res.oracle

@@ -13,34 +13,35 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
-[metrics] Defined functions (74)
+[metrics] Defined functions (76)
   ======================
    Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
-   Frama_C_interval (13 calls); Frama_C_nondet (11 calls);
+   Frama_C_interval (14 calls); Frama_C_nondet (12 calls);
    Frama_C_nondet_ptr (0 call); __FC_assert (0 call); __fc_initenv (4 calls);
    __finite (0 call); __finitef (0 call); abs (0 call); atoi (0 call);
    calloc (0 call); char_equal_ignore_case (1 call); fabs (0 call);
    fabsf (0 call); feholdexcept (0 call); fesetenv (0 call);
    fetestexcept (0 call); getaddrinfo (0 call); getenv (0 call);
-   getline (0 call); glob (0 call); globfree (0 call); imaxabs (0 call);
-   imaxdiv (0 call); isalnum (0 call); isalpha (0 call); isblank (0 call);
-   iscntrl (0 call); isdigit (3 calls); isgraph (0 call); islower (0 call);
-   isprint (0 call); ispunct (0 call); isspace (1 call); isupper (0 call);
-   isxdigit (0 call); localeconv (0 call); main (0 call); memchr (0 call);
-   memcmp (0 call); memcpy (2 calls); memmove (0 call); memrchr (0 call);
-   memset (1 call); posix_memalign (0 call); putenv (0 call); setenv (0 call);
-   setlocale (0 call); strcasecmp (0 call); strcat (0 call); strchr (3 calls);
-   strcmp (0 call); strcpy (0 call); strdup (0 call); strerror (0 call);
-   strlen (6 calls); strncat (0 call); strncmp (0 call); strncpy (0 call);
-   strndup (0 call); strnlen (0 call); strrchr (0 call); strstr (0 call);
-   tolower (0 call); toupper (0 call); unsetenv (0 call); wcscat (0 call);
-   wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
-   wmemcpy (0 call); wmemset (0 call); 
+   gethostbyname (0 call); getline (0 call); glob (0 call); globfree (0 call);
+   imaxabs (0 call); imaxdiv (0 call); isalnum (0 call); isalpha (0 call);
+   isblank (0 call); iscntrl (0 call); isdigit (3 calls); isgraph (0 call);
+   islower (0 call); isprint (0 call); ispunct (0 call); isspace (1 call);
+   isupper (0 call); isxdigit (0 call); localeconv (0 call); main (0 call);
+   memchr (0 call); memcmp (0 call); memcpy (4 calls); memmove (0 call);
+   memrchr (0 call); memset (1 call); posix_memalign (0 call); putenv (0 call);
+   res_search (1 call); setenv (0 call); setlocale (0 call);
+   strcasecmp (0 call); strcat (0 call); strchr (3 calls); strcmp (0 call);
+   strcpy (0 call); strdup (0 call); strerror (0 call); strlen (6 calls);
+   strncat (0 call); strncmp (0 call); strncpy (2 calls); strndup (0 call);
+   strnlen (0 call); strrchr (0 call); strstr (0 call); tolower (0 call);
+   toupper (0 call); unsetenv (0 call); wcscat (0 call); wcscpy (0 call);
+   wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
+   wmemset (0 call); 
   
   Undefined functions (360)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
-   Frama_C_abort (1 call); Frama_C_char_interval (0 call);
+   Frama_C_abort (1 call); Frama_C_char_interval (1 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
    Frama_C_long_long_interval (0 call); Frama_C_make_unknown (2 calls);
    Frama_C_real_interval_as_double (0 call); Frama_C_short_interval (0 call);
@@ -98,7 +99,7 @@
    getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
    getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
    iconv (0 call); iconv_close (0 call); iconv_open (0 call);
-   inet_addr (0 call); inet_ntoa (0 call); inet_ntop (0 call);
+   inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
    inet_pton (0 call); isascii (0 call); kill (0 call); labs (0 call);
    ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
    localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
@@ -162,18 +163,18 @@
   
   Global metrics
   ============== 
-  Sloc = 956
-  Decision point = 184
-  Global variables = 58
-  If = 175
-  Loop = 40
-  Goto = 79
-  Assignment = 382
-  Exit point = 74
-  Function = 434
-  Function call = 74
-  Pointer dereferencing = 148
-  Cyclomatic complexity = 258
+  Sloc = 1026
+  Decision point = 195
+  Global variables = 59
+  If = 186
+  Loop = 42
+  Goto = 84
+  Assignment = 415
+  Exit point = 76
+  Function = 436
+  Function call = 84
+  Pointer dereferencing = 157
+  Cyclomatic complexity = 271
 /* Generated by Frama-C */
 #include "__fc_builtin.c"
 #include "__fc_builtin.h"

tests/libc/oracle/netdb_c.res.oracle

@@ -35,10 +35,13 @@
   \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
@@ -52,68 +55,68 @@
   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:55: Call to builtin malloc
-[eva] share/libc/netdb.c:55: allocating variable __malloc_getaddrinfo_l55
-[eva] share/libc/netdb.c:57: Call to builtin malloc
-[eva] share/libc/netdb.c:57: allocating variable __malloc_getaddrinfo_l57
+[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:59.
+  Called from share/libc/netdb.c:60.
 [eva] using specification for function Frama_C_interval
-[eva] share/libc/netdb.c:59: 
+[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:62.
-[eva] share/libc/netdb.c:62: 
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:62.
+  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:67.
-[eva] share/libc/netdb.c:67: 
+  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:68.
-[eva] share/libc/netdb.c:68: 
+  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
@@ -168,6 +171,83 @@
 [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_string_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:369: 
+  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 ======
@@ -175,20 +255,42 @@
   __fc_errno ∈ [--..--]
   __fc_heap_status ∈ [--..--]
   Frama_C_entropy_source ∈ [--..--]
-  result ∈ {{ &__malloc_getaddrinfo_l55 }} or UNINITIALIZED
+  result ∈ {{ &__malloc_getaddrinfo_l56 }} or UNINITIALIZED
   __retres ∈ [-11..0]
-  __malloc_getaddrinfo_l55.ai_flags ∈ {0} or UNINITIALIZED
+  __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_l57 }} or UNINITIALIZED
+                          {{ &__malloc_getaddrinfo_l58 }} or UNINITIALIZED
                           .ai_canonname ∈ {{ "dummy" }} or UNINITIALIZED
                           .ai_next ∈ {0} or UNINITIALIZED
-  __malloc_getaddrinfo_l57.sa_family ∈ [0..43]
+  __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 ∈ [--..--]
@@ -196,24 +298,35 @@
   __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_l55 }}
-  rp ∈ {{ &__malloc_getaddrinfo_l55 }}
+  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_l55.ai_flags ∈ {0}
+  __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_l57 }}
+                          .ai_addr ∈ {{ &__malloc_getaddrinfo_l58 }}
                           .ai_canonname ∈ {{ "dummy" }}
                           .ai_next ∈ {0}
-  __malloc_getaddrinfo_l57.sa_family ∈ [0..43]
+  __malloc_getaddrinfo_l58.sa_family ∈ [0..43]
                           .sa_data[0..13] ∈ [--..--]