From 9db127da11aba2bff6ab59ab0e8db14ce5583dbb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 1 Feb 2019 18:53:34 +0100
Subject: [PATCH] [Libc] add stub for gethostbyname
---
share/libc/netdb.c | 81 ++
tests/libc/netdb_c.c | 5 +
tests/libc/oracle/fc_libc.0.res.oracle | 61 +-
tests/libc/oracle/fc_libc.1.res.oracle | 1342 +++++++++++++-----------
tests/libc/oracle/netdb_c.res.oracle | 181 +++-
5 files changed, 987 insertions(+), 683 deletions(-)
diff --git a/share/libc/netdb.c b/share/libc/netdb.c
index cfdea15cc7f..d8380dd1d5f 100644
--- a/share/libc/netdb.c
+++ b/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
diff --git a/tests/libc/netdb_c.c b/tests/libc/netdb_c.c
index ab3f26fe01c..6e8f905b5d8 100644
--- a/tests/libc/netdb_c.c
+++ b/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;
}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 27fb20cb71c..b48eca2cad5 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/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"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 0abbc1a3822..8fbee9224b0 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -184,6 +184,13 @@ enum __anonenum_22 {
IPPROTO_RAW = 255,
IPPROTO_MAX = 256
};
+struct hostent {
+ char *h_name ;
+ char **h_aliases ;
+ int h_addrtype ;
+ int h_length ;
+ char **h_addr_list ;
+};
struct addrinfo {
int ai_flags ;
int ai_family ;
@@ -194,6 +201,13 @@ struct addrinfo {
char *ai_canonname ;
struct addrinfo *ai_next ;
};
+struct __fc_gethostbyname {
+ struct hostent host ;
+ unsigned char host_addr[sizeof(struct in_addr)] ;
+ char *h_addr_ptrs[2 + 1] ;
+ char *host_aliases[2] ;
+ char hostbuf[128] ;
+};
typedef void * const * va_list;
typedef unsigned int ino_t;
typedef long time_t;
@@ -3230,422 +3244,779 @@ int getaddrinfo(char const * __restrict nodename,
struct addrinfo const * __restrict hints,
struct addrinfo ** __restrict res);
-static unsigned int volatile getaddrinfo_net_state;
-/*@ requires
- nodename_string: nodename ≡ \null ∨ valid_read_string(nodename);
- requires
- servname_string: servname ≡ \null ∨ valid_read_string(servname);
- requires hints_option: hints ≡ \null ∨ \valid_read(hints);
- requires valid_res: \valid(res);
- assigns *res, \result, __fc_errno;
- assigns *res
- \from (indirect: nodename), (indirect: servname), (indirect: hints);
- assigns \result
- \from (indirect: nodename), (indirect: servname), (indirect: hints);
- assigns __fc_errno
- \from (indirect: nodename), (indirect: servname), (indirect: hints);
- allocates *\old(res);
-
- behavior empty_request:
- assumes empty: nodename ≡ \null ∧ servname ≡ \null;
- ensures no_name: \result ≡ -2;
- assigns \result;
- assigns \result \from (indirect: nodename), (indirect: servname);
-
- behavior normal_request:
- assumes has_name: nodename ≢ \null ∨ servname ≢ \null;
- ensures
- initialization: allocation: success_or_error:
- (\result ≡ 0 ∧
- \fresh{Old, Here}(*\old(res),sizeof(*\old(res))) ∧
- \initialized(*\old(res))) ∨
- \result ≡ -3 ∨ \result ≡ -1 ∨ \result ≡ -4 ∨
- \result ≡ -6 ∨ \result ≡ -10 ∨ \result ≡ -8 ∨
- \result ≡ -7 ∨ \result ≡ -11;
-
- complete behaviors normal_request, empty_request;
- disjoint behaviors normal_request, empty_request;
+struct hostent *gethostbyname(char const *name);
+
+/*@
+predicate non_escaping{L}(void *s, size_t n) =
+ ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\dangling((char *)s + i);
*/
-int getaddrinfo(char const * __restrict nodename,
- char const * __restrict servname,
- struct addrinfo const * __restrict hints,
- struct addrinfo ** __restrict res)
-{
- int __retres;
- if (nodename == (char const *)0)
- if (servname == (char const *)0) {
- __retres = -2;
- goto return_label;
- }
- switch (getaddrinfo_net_state) {
- case (unsigned int)0: __retres = -1;
- goto return_label;
- case (unsigned int)1: __retres = -3;
- goto return_label;
- case (unsigned int)2: __retres = -4;
- goto return_label;
- case (unsigned int)3: __retres = -6;
- goto return_label;
- case (unsigned int)5: __retres = -8;
- goto return_label;
- case (unsigned int)6: __retres = -7;
- goto return_label;
- case (unsigned int)7:
- {
- __fc_errno = 5;
- __retres = -11;
- goto return_label;
- }
- default:
- {
- struct addrinfo *tmp_0;
- struct sockaddr *tmp_2;
- int tmp_3;
- struct addrinfo *ai = malloc(sizeof(*tmp_0));
- if (! ai) {
- __retres = -10;
- goto return_label;
- }
- struct sockaddr *sa = malloc(sizeof(*tmp_2));
- if (! sa) {
- __retres = -10;
- goto return_label;
- }
- tmp_3 = Frama_C_interval(0,43);
- sa->sa_family = (unsigned short)tmp_3;
- /*@ slevel 15; */
- {
- int i = 0;
- while (i < 14) {
- {
- int tmp_4;
- tmp_4 = Frama_C_interval(-128,127);
- sa->sa_data[i] = (char)tmp_4;
- }
- i ++;
- }
- }
- /*@ slevel default; */
- ai->ai_flags = 0;
- ai->ai_family = (int)sa->sa_family;
- ai->ai_socktype = Frama_C_interval(0,5);
- ai->ai_protocol = Frama_C_interval(0,IPPROTO_MAX);
- ai->ai_addrlen = sizeof(*sa);
- ai->ai_addr = sa;
- ai->ai_canonname = (char *)"dummy";
- ai->ai_next = (struct addrinfo *)0;
- *res = ai;
- __retres = 0;
- goto return_label;
- }
- }
- return_label: return __retres;
-}
+/*@
+predicate empty_block{L}(void *s) =
+ \block_length((char *)s) ≡ 0 ∧ \offset((char *)s) ≡ 0;
+ */
+/*@
+predicate valid_or_empty{L}(void *s, size_t n) =
+ (empty_block(s) ∨ \valid_read((char *)s)) ∧
+ \valid((char *)s + (0 .. n - 1));
+ */
+/*@
+predicate valid_read_or_empty{L}(void *s, size_t n) =
+ (empty_block(s) ∨ \valid_read((char *)s)) ∧
+ \valid_read((char *)s + (1 .. n - 1));
-FILE *__fc_stderr;
+*/
+int memcmp(void const *s1, void const *s2, size_t n);
-FILE *__fc_stdin;
+void *memchr(void const *s, int c, size_t n);
-FILE *__fc_stdout;
+void *memcpy(void * __restrict dest, void const * __restrict src, size_t n);
-/*@ assigns \nothing; */
-extern int remove(char const *filename);
+void *memmove(void *dest, void const *src, size_t n);
-/*@ assigns \nothing; */
-extern int rename(char const *old_name, char const *new_name);
+void *memset(void *s, int c, size_t n);
-FILE __fc_fopen[16];
-FILE * const __fc_p_fopen = __fc_fopen;
-/*@ ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
- assigns \result;
- assigns \result \from __fc_p_fopen;
- */
-extern FILE *tmpfile(void);
+size_t strlen(char const *s);
-/*@ assigns \result, *(s + (..));
- assigns \result \from *(s + (..));
- assigns *(s + (..)) \from \nothing;
- */
-extern char *tmpnam(char *s);
+size_t strnlen(char const *s, size_t maxlen);
-/*@ requires valid_stream: \valid(stream);
- ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result \from stream, stream->__fc_FILE_id;
- */
-extern int fclose(FILE *stream);
+int strcmp(char const *s1, char const *s2);
-/*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream);
- ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+int strncmp(char const *s1, char const *s2, size_t n);
+
+/*@ requires valid_string_s1: valid_read_string(s1);
+ requires valid_string_s2: valid_read_string(s2);
assigns \result;
- assigns \result \from stream, stream->__fc_FILE_id;
+ assigns \result
+ \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
-extern int fflush(FILE *stream);
+extern int strcoll(char const *s1, char const *s2);
-/*@ requires valid_filename: valid_read_string(filename);
- requires valid_mode: valid_read_string(mode);
- ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+char *strchr(char const *s, int c);
+
+char *strrchr(char const *s, int c);
+
+/*@ requires valid_string_s: valid_read_string(s);
+ requires valid_string_reject: valid_read_string(reject);
+ ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result;
assigns \result
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen;
+ \from (indirect: *(s + (0 ..))), (indirect: *(reject + (0 ..)));
*/
-extern FILE *fopen(char const * __restrict filename,
- char const * __restrict mode);
+extern size_t strcspn(char const *s, char const *reject);
-/*@ requires valid_mode: valid_read_string(mode);
- ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
- assigns \result, __fc_fopen[fd];
+/*@ requires valid_string_s: valid_read_string(s);
+ requires valid_string_accept: valid_read_string(accept);
+ ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
+ assigns \result, \result;
+ assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
- (indirect: __fc_fopen[fd]), __fc_p_fopen;
- assigns __fc_fopen[fd]
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
- (indirect: __fc_fopen[fd]), __fc_p_fopen;
+ \from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
*/
-extern FILE *fdopen(int fd, char const *mode);
+extern size_t strspn(char const *s, char const *accept);
-/*@ requires valid_filename: valid_read_string(filename);
- requires valid_mode: valid_read_string(mode);
- requires valid_stream: \valid(stream);
+/*@ requires valid_string_s: valid_read_string(s);
+ requires valid_string_accept: valid_read_string(accept);
ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \result ∈ &__fc_fopen[0 .. 16 - 1];
- ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1];
- assigns \result, *stream;
- assigns \result
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen, (indirect: stream);
- assigns *stream
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen, (indirect: stream);
+ result_null_or_same_base:
+ \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
*/
-extern FILE *freopen(char const * __restrict filename,
- char const * __restrict mode, FILE * __restrict stream);
-
-/*@ assigns *stream;
- assigns *stream \from buf; */
-extern void setbuf(FILE * __restrict stream, char * __restrict buf);
-
-/*@ assigns *stream;
- assigns *stream \from buf, mode, size; */
-extern int setvbuf(FILE * __restrict stream, char * __restrict buf, int mode,
- size_t size);
-
-/*@ axiomatic format_length {
- logic ℤ format_length{L}(char *format) ;
-
- }
+extern char *strpbrk(char const *s, char const *accept);
-*/
-/*@ assigns *stream;
- assigns *stream \from *(format + (..)), arg; */
-extern int vfprintf(FILE * __restrict stream, char const * __restrict format,
- va_list arg);
+char *strstr(char const *haystack, char const *needle);
-/*@ assigns *stream;
- assigns *stream \from *(format + (..)), *stream; */
-extern int vfscanf(FILE * __restrict stream, char const * __restrict format,
- va_list arg);
-
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from arg; */
-extern int vprintf(char const * __restrict format, va_list arg);
-
-/*@ assigns *__fc_stdin;
- assigns *__fc_stdin \from *(format + (..)); */
-extern int vscanf(char const * __restrict format, va_list arg);
-
-/*@ assigns *(s + (0 .. n - 1));
- assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
- */
-extern int vsnprintf(char * __restrict s, size_t n,
- char const * __restrict format, va_list arg);
-
-/*@ assigns *(s + (0 ..));
- assigns *(s + (0 ..)) \from *(format + (..)), arg;
+char *__fc_strtok_ptr;
+/*@ requires valid_string_delim: valid_read_string(delim);
+ assigns *(s + (0 ..)), *(__fc_strtok_ptr + (0 ..)), \result,
+ __fc_strtok_ptr;
+ assigns *(s + (0 ..))
+ \from *(s + (0 ..)), (indirect: s), (indirect: __fc_strtok_ptr),
+ (indirect: *(delim + (0 ..)));
+ assigns *(__fc_strtok_ptr + (0 ..))
+ \from *(__fc_strtok_ptr + (0 ..)), (indirect: s),
+ (indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..)));
+ assigns \result
+ \from s, __fc_strtok_ptr, (indirect: *(s + (0 ..))),
+ (indirect: *(__fc_strtok_ptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+ assigns __fc_strtok_ptr
+ \from \old(__fc_strtok_ptr), s,
+ (indirect: *(__fc_strtok_ptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+
+ behavior new_str:
+ assumes s_not_null: s ≢ \null;
+ requires
+ valid_string_s_or_delim_not_found:
+ valid_string(s) ∨
+ (valid_read_string(s) ∧
+ (∀ int i;
+ 0 ≤ i < strlen(delim) ⇒
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
+ ensures
+ result_subset:
+ \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
+ ensures ptr_subset: \subset(__fc_strtok_ptr, \old(s) + (0 ..));
+ assigns __fc_strtok_ptr, *(s + (0 ..)), \result;
+ assigns __fc_strtok_ptr
+ \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
+ assigns *(s + (0 ..))
+ \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
+ assigns \result
+ \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
+
+ behavior resume_str:
+ assumes s_null: s ≡ \null;
+ requires not_first_call: __fc_strtok_ptr ≢ \null;
+ ensures
+ result_subset:
+ \result ≡ \null ∨
+ \subset(\result, \old(__fc_strtok_ptr) + (0 ..));
+ ensures
+ ptr_subset: \subset(__fc_strtok_ptr, \old(__fc_strtok_ptr) + (0 ..));
+ assigns *(__fc_strtok_ptr + (0 ..)), __fc_strtok_ptr, \result;
+ assigns *(__fc_strtok_ptr + (0 ..))
+ \from *(__fc_strtok_ptr + (0 ..)), (indirect: __fc_strtok_ptr),
+ (indirect: *(delim + (0 ..)));
+ assigns __fc_strtok_ptr
+ \from \old(__fc_strtok_ptr), (indirect: *(__fc_strtok_ptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+ assigns \result
+ \from __fc_strtok_ptr, (indirect: *(__fc_strtok_ptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+
+ complete behaviors resume_str, new_str;
+ disjoint behaviors resume_str, new_str;
*/
-extern int vsprintf(char * __restrict s, char const * __restrict format,
- va_list arg);
+extern char *strtok(char * __restrict s, char const * __restrict delim);
-/*@ requires valid_stream: \valid(stream);
- ensures result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1;
- assigns *stream, \result;
- assigns *stream \from *stream;
- assigns \result \from (indirect: *stream);
+/*@ requires valid_string_delim: valid_read_string(delim);
+ requires valid_saveptr: \valid(saveptr);
+ assigns *(s + (0 ..)), *(*saveptr + (0 ..)), \result, *saveptr;
+ assigns *(s + (0 ..))
+ \from *(s + (0 ..)), (indirect: s), (indirect: *saveptr),
+ (indirect: *(delim + (0 ..)));
+ assigns *(*saveptr + (0 ..))
+ \from *(*saveptr + (0 ..)), (indirect: s), (indirect: *saveptr),
+ (indirect: *(delim + (0 ..)));
+ assigns \result
+ \from s, *saveptr, (indirect: *(s + (0 ..))),
+ (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..)));
+ assigns *saveptr
+ \from \old(*saveptr), s, (indirect: *(*saveptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+
+ behavior new_str:
+ assumes s_not_null: s ≢ \null;
+ requires
+ valid_string_s_or_delim_not_found:
+ valid_string(s) ∨
+ (valid_read_string(s) ∧
+ (∀ int i;
+ 0 ≤ i < strlen(delim) ⇒
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
+ ensures
+ result_subset:
+ \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
+ ensures initialization: \initialized(\old(saveptr));
+ ensures saveptr_subset: \subset(*\old(saveptr), \old(s) + (0 ..));
+ assigns *saveptr, *(s + (0 ..)), \result;
+ assigns *saveptr
+ \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
+ assigns *(s + (0 ..))
+ \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
+ assigns \result
+ \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
+
+ behavior resume_str:
+ assumes s_null: s ≡ \null;
+ requires not_first_call: *saveptr ≢ \null;
+ requires initialization: saveptr: \initialized(saveptr);
+ ensures
+ result_subset:
+ \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
+ ensures
+ saveptr_subset: \subset(*\old(saveptr), \old(*saveptr) + (0 ..));
+ assigns *(*saveptr + (0 ..)), *saveptr, \result;
+ assigns *(*saveptr + (0 ..))
+ \from *(*saveptr + (0 ..)), (indirect: *saveptr),
+ (indirect: *(delim + (0 ..)));
+ assigns *saveptr
+ \from \old(*saveptr), (indirect: *(*saveptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+ assigns \result
+ \from *saveptr, (indirect: *(*saveptr + (0 ..))),
+ (indirect: *(delim + (0 ..)));
+
+ complete behaviors resume_str, new_str;
+ disjoint behaviors resume_str, new_str;
*/
-extern int fgetc(FILE *stream);
+extern char *strtok_r(char * __restrict s, char const * __restrict delim,
+ char ** __restrict saveptr);
-/*@ requires valid_stream: \valid(stream);
- ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s);
- ensures
- terminated_string_on_success:
- \result ≢ \null ⇒ valid_string(\old(s));
- assigns *(s + (0 .. size)), \result;
- assigns *(s + (0 .. size)) \from (indirect: size), (indirect: *stream);
- assigns \result \from s, (indirect: size), (indirect: *stream);
+/*@ requires
+ valid_string_stringp: \valid(stringp) ∧ valid_string(*stringp);
+ requires valid_string_delim: valid_read_string(delim);
+ assigns *stringp, \result;
+ assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
+ assigns \result \from *(delim + (..)), *(*(stringp + (..)));
*/
-extern char *fgets(char * __restrict s, int size, FILE * __restrict stream);
+extern char *strsep(char **stringp, char const *delim);
-/*@ assigns *stream; */
-extern int fputc(int c, FILE *stream);
+extern char __fc_strerror[64];
-/*@ assigns *stream;
- assigns *stream \from *(s + (..)); */
-extern int fputs(char const * __restrict s, FILE * __restrict stream);
+char * const __fc_p_strerror = __fc_strerror;
+char *strerror(int errnum);
-/*@ assigns \result, *stream;
- assigns \result \from *stream;
- assigns *stream \from *stream;
- */
-extern int getc(FILE *stream);
+char *strcpy(char *dest, char const *src);
-/*@ assigns \result;
- assigns \result \from *__fc_stdin; */
-extern int getchar(void);
+char *strncpy(char *dest, char const *src, size_t n);
-/*@ ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
- assigns *(s + (..)), \result;
- assigns *(s + (..)) \from *__fc_stdin;
- assigns \result \from s, __fc_stdin;
- */
-extern char *gets(char *s);
+char *strcat(char *dest, char const *src);
-/*@ assigns *stream;
- assigns *stream \from c; */
-extern int putc(int c, FILE *stream);
+char *strncat(char *dest, char const *src, size_t n);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from c; */
-extern int putchar(int c);
+/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
+ requires valid_string_src: valid_read_string(src);
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1))
+ \from (indirect: *(src + (0 ..))), (indirect: n);
+ assigns \result \from dest;
+ */
+extern size_t strxfrm(char * __restrict dest, char const * __restrict src,
+ size_t n);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(s + (..)); */
-extern int puts(char const *s);
+char *strdup(char const *s);
-/*@ assigns *stream;
- assigns *stream \from c; */
-extern int ungetc(int c, FILE *stream);
+char *strndup(char const *s, size_t n);
-/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
- requires valid_stream: \valid(stream);
- ensures size_read: \result ≤ \old(nmemb);
+/*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
ensures
- initialization:
- \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
- assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
- assigns *((char *)ptr + (0 .. nmemb * size - 1))
- \from size, nmemb, *stream;
- assigns \result \from size, *stream;
+ s_initialized: initialization:
+ \initialized((char *)\old(s) + (0 .. \old(n) - 1));
+ ensures
+ zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
+ assigns *((char *)s + (0 .. n - 1));
+ assigns *((char *)s + (0 .. n - 1)) \from \nothing;
*/
-extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
- FILE * __restrict stream);
+extern void bzero(void *s, size_t n);
-/*@ requires
- valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1));
- requires valid_stream: \valid(stream);
- ensures size_written: \result ≤ \old(nmemb);
- assigns *stream, \result;
- assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
- assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
+int strcasecmp(char const *s1, char const *s2);
+
+/*@ requires valid_string_s1: valid_read_nstring(s1, n);
+ requires valid_string_s2: valid_read_nstring(s2, n);
+ assigns \result;
+ assigns \result
+ \from (indirect: n), (indirect: *(s1 + (0 .. n - 1))),
+ (indirect: *(s2 + (0 .. n - 1)));
*/
-extern size_t fwrite(void const * __restrict ptr, size_t size, size_t nmemb,
- FILE * __restrict stream);
+extern int strncasecmp(char const *s1, char const *s2, size_t n);
-/*@ assigns *pos;
- assigns *pos \from *stream; */
-extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
-
-/*@ requires valid_stream: \valid(stream);
- requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
- assigns *stream, \result, __fc_errno;
- assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+static unsigned int volatile getaddrinfo_net_state;
+/*@ requires
+ nodename_string: nodename ≡ \null ∨ valid_read_string(nodename);
+ requires
+ servname_string: servname ≡ \null ∨ valid_read_string(servname);
+ requires hints_option: hints ≡ \null ∨ \valid_read(hints);
+ requires valid_res: \valid(res);
+ assigns *res, \result, __fc_errno;
+ assigns *res
+ \from (indirect: nodename), (indirect: servname), (indirect: hints);
assigns \result
- \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ \from (indirect: nodename), (indirect: servname), (indirect: hints);
assigns __fc_errno
- \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ \from (indirect: nodename), (indirect: servname), (indirect: hints);
+ allocates *\old(res);
+
+ behavior empty_request:
+ assumes empty: nodename ≡ \null ∧ servname ≡ \null;
+ ensures no_name: \result ≡ -2;
+ assigns \result;
+ assigns \result \from (indirect: nodename), (indirect: servname);
+
+ behavior normal_request:
+ assumes has_name: nodename ≢ \null ∨ servname ≢ \null;
+ ensures
+ initialization: allocation: success_or_error:
+ (\result ≡ 0 ∧
+ \fresh{Old, Here}(*\old(res),sizeof(*\old(res))) ∧
+ \initialized(*\old(res))) ∨
+ \result ≡ -3 ∨ \result ≡ -1 ∨ \result ≡ -4 ∨
+ \result ≡ -6 ∨ \result ≡ -10 ∨ \result ≡ -8 ∨
+ \result ≡ -7 ∨ \result ≡ -11;
+
+ complete behaviors normal_request, empty_request;
+ disjoint behaviors normal_request, empty_request;
*/
-extern int fseek(FILE *stream, long offset, int whence);
-
-/*@ assigns *stream;
- assigns *stream \from *pos; */
-extern int fsetpos(FILE *stream, fpos_t const *pos);
+int getaddrinfo(char const * __restrict nodename,
+ char const * __restrict servname,
+ struct addrinfo const * __restrict hints,
+ struct addrinfo ** __restrict res)
+{
+ int __retres;
+ if (nodename == (char const *)0)
+ if (servname == (char const *)0) {
+ __retres = -2;
+ goto return_label;
+ }
+ switch (getaddrinfo_net_state) {
+ case (unsigned int)0: __retres = -1;
+ goto return_label;
+ case (unsigned int)1: __retres = -3;
+ goto return_label;
+ case (unsigned int)2: __retres = -4;
+ goto return_label;
+ case (unsigned int)3: __retres = -6;
+ goto return_label;
+ case (unsigned int)5: __retres = -8;
+ goto return_label;
+ case (unsigned int)6: __retres = -7;
+ goto return_label;
+ case (unsigned int)7:
+ {
+ __fc_errno = 5;
+ __retres = -11;
+ goto return_label;
+ }
+ default:
+ {
+ struct addrinfo *tmp_0;
+ struct sockaddr *tmp_2;
+ int tmp_3;
+ struct addrinfo *ai = malloc(sizeof(*tmp_0));
+ if (! ai) {
+ __retres = -10;
+ goto return_label;
+ }
+ struct sockaddr *sa = malloc(sizeof(*tmp_2));
+ if (! sa) {
+ __retres = -10;
+ goto return_label;
+ }
+ tmp_3 = Frama_C_interval(0,43);
+ sa->sa_family = (unsigned short)tmp_3;
+ /*@ slevel 15; */
+ {
+ int i = 0;
+ while (i < 14) {
+ {
+ int tmp_4;
+ tmp_4 = Frama_C_interval(-128,127);
+ sa->sa_data[i] = (char)tmp_4;
+ }
+ i ++;
+ }
+ }
+ /*@ slevel default; */
+ ai->ai_flags = 0;
+ ai->ai_family = (int)sa->sa_family;
+ ai->ai_socktype = Frama_C_interval(0,5);
+ ai->ai_protocol = Frama_C_interval(0,IPPROTO_MAX);
+ ai->ai_addrlen = sizeof(*sa);
+ ai->ai_addr = sa;
+ ai->ai_canonname = (char *)"dummy";
+ ai->ai_next = (struct addrinfo *)0;
+ *res = ai;
+ __retres = 0;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+}
-/*@ requires valid_stream: \valid(stream);
- ensures
- success_or_error:
- \result ≡ -1 ∨
- (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
- assigns \result, __fc_errno;
- assigns \result \from (indirect: *stream);
- assigns __fc_errno \from (indirect: *stream);
- */
-extern long ftell(FILE *stream);
+struct __fc_gethostbyname __fc_ghbn;
+int res_search(char const *dname, int class, int type, char *answer,
+ int anslen)
+{
+ int tmp;
+ {
+ int i = 0;
+ while (i < anslen - 1) {
+ *(answer + i) = Frama_C_char_interval((char)(-128),(char)127);
+ i ++;
+ }
+ }
+ *(answer + (anslen - 1)) = (char)0;
+ tmp = Frama_C_interval(-1,anslen);
+ return tmp;
+}
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
-extern void rewind(FILE *stream);
+struct hostent *gethostbyname(char const *name)
+{
+ struct hostent *__retres;
+ char buf[128];
+ char const *cp;
+ int n;
+ int tmp;
+ __fc_ghbn.host.h_addrtype = 2;
+ __fc_ghbn.host.h_length = (int)sizeof(struct in_addr);
+ if ((int)*name >= '0')
+ if ((int)*name <= '9') {
+ cp = name;
+ while (1) {
+ if (! *cp) {
+ struct in_addr addr;
+ cp --;
+ ;
+ if ((int)*cp == '.') break;
+ addr.s_addr = inet_addr(name);
+ if (addr.s_addr == 0xffffffff) {
+ __retres = (struct hostent *)0;
+ goto return_label;
+ }
+ memcpy((void *)(__fc_ghbn.host_addr),(void const *)(& addr),
+ (unsigned int)__fc_ghbn.host.h_length);
+ strncpy(__fc_ghbn.hostbuf,name,(unsigned int)(128 - 1));
+ __fc_ghbn.hostbuf[128 - 1] = (char)'\000';
+ __fc_ghbn.host.h_name = __fc_ghbn.hostbuf;
+ __fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases;
+ __fc_ghbn.host_aliases[0] = (char *)0;
+ __fc_ghbn.h_addr_ptrs[0] = (char *)(__fc_ghbn.host_addr);
+ __fc_ghbn.h_addr_ptrs[1] = (char *)0;
+ __fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs;
+ __retres = & __fc_ghbn.host;
+ goto return_label;
+ }
+ if ((int)*cp < '0')
+ if ((int)*cp > '9')
+ if ((int)*cp != '.') break;
+ cp ++;
+ }
+ }
+ n = res_search(name,1,1,buf,(int)sizeof(buf));
+ if (n < 0) {
+ __retres = (struct hostent *)0;
+ goto return_label;
+ }
+ tmp = Frama_C_nondet(0,1);
+ if (tmp) {
+ __retres = (struct hostent *)0;
+ goto return_label;
+ }
+ else {
+ struct in_addr addr_0;
+ addr_0.s_addr = inet_addr(name);
+ memcpy((void *)(__fc_ghbn.host_addr),(void const *)(& addr_0),
+ (unsigned int)__fc_ghbn.host.h_length);
+ strncpy(__fc_ghbn.hostbuf,name,(unsigned int)(128 - 1));
+ __fc_ghbn.hostbuf[128 - 1] = (char)'\000';
+ __fc_ghbn.host.h_name = __fc_ghbn.hostbuf;
+ __fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases;
+ __fc_ghbn.host_aliases[0] = (char *)0;
+ __fc_ghbn.h_addr_ptrs[0] = (char *)(__fc_ghbn.host_addr);
+ __fc_ghbn.h_addr_ptrs[1] = (char *)0;
+ __fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs;
+ __retres = & __fc_ghbn.host;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
-extern void clearerr(FILE *stream);
+FILE *__fc_stderr;
-/*@ assigns \result;
- assigns \result \from *stream; */
-extern int feof(FILE *stream);
+FILE *__fc_stdin;
-/*@ assigns \result;
- assigns \result \from *stream; */
-extern int fileno(FILE *stream);
+FILE *__fc_stdout;
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
-extern void flockfile(FILE *stream);
+/*@ assigns \nothing; */
+extern int remove(char const *filename);
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
-extern void funlockfile(FILE *stream);
+/*@ assigns \nothing; */
+extern int rename(char const *old_name, char const *new_name);
-/*@ assigns \result, *stream;
- assigns \result \from \nothing;
- assigns *stream \from \nothing;
+FILE __fc_fopen[16];
+FILE * const __fc_p_fopen = __fc_fopen;
+/*@ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result \from __fc_p_fopen;
*/
-extern int ftrylockfile(FILE *stream);
-
-/*@ assigns \result;
- assigns \result \from *stream; */
-extern int ferror(FILE *stream);
+extern FILE *tmpfile(void);
-/*@ assigns __fc_stdout;
- assigns __fc_stdout \from __fc_errno, *(s + (..));
+/*@ assigns \result, *(s + (..));
+ assigns \result \from *(s + (..));
+ assigns *(s + (..)) \from \nothing;
*/
-extern void perror(char const *s);
+extern char *tmpnam(char *s);
-/*@ assigns \result, *stream;
- assigns \result \from *stream;
- assigns *stream \from *stream;
+/*@ requires valid_stream: \valid(stream);
+ ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from stream, stream->__fc_FILE_id;
*/
-extern int getc_unlocked(FILE *stream);
+extern int fclose(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *__fc_stdin; */
-extern int getchar_unlocked(void);
+/*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream);
+ ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from stream, stream->__fc_FILE_id;
+ */
+extern int fflush(FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from c; */
-extern int putc_unlocked(int c, FILE *stream);
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
+ __fc_p_fopen;
+ */
+extern FILE *fopen(char const * __restrict filename,
+ char const * __restrict mode);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from c; */
-extern int putchar_unlocked(int c);
+/*@ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result, __fc_fopen[fd];
+ assigns \result
+ \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ (indirect: __fc_fopen[fd]), __fc_p_fopen;
+ assigns __fc_fopen[fd]
+ \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ (indirect: __fc_fopen[fd]), __fc_p_fopen;
+ */
+extern FILE *fdopen(int fd, char const *mode);
-/*@ assigns *stream;
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ requires valid_stream: \valid(stream);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \result ∈ &__fc_fopen[0 .. 16 - 1];
+ ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1];
+ assigns \result, *stream;
+ assigns \result
+ \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
+ __fc_p_fopen, (indirect: stream);
+ assigns *stream
+ \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
+ __fc_p_fopen, (indirect: stream);
+ */
+extern FILE *freopen(char const * __restrict filename,
+ char const * __restrict mode, FILE * __restrict stream);
+
+/*@ assigns *stream;
+ assigns *stream \from buf; */
+extern void setbuf(FILE * __restrict stream, char * __restrict buf);
+
+/*@ assigns *stream;
+ assigns *stream \from buf, mode, size; */
+extern int setvbuf(FILE * __restrict stream, char * __restrict buf, int mode,
+ size_t size);
+
+/*@ axiomatic format_length {
+ logic ℤ format_length{L}(char *format) ;
+
+ }
+
+*/
+/*@ assigns *stream;
+ assigns *stream \from *(format + (..)), arg; */
+extern int vfprintf(FILE * __restrict stream, char const * __restrict format,
+ va_list arg);
+
+/*@ assigns *stream;
+ assigns *stream \from *(format + (..)), *stream; */
+extern int vfscanf(FILE * __restrict stream, char const * __restrict format,
+ va_list arg);
+
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from arg; */
+extern int vprintf(char const * __restrict format, va_list arg);
+
+/*@ assigns *__fc_stdin;
+ assigns *__fc_stdin \from *(format + (..)); */
+extern int vscanf(char const * __restrict format, va_list arg);
+
+/*@ assigns *(s + (0 .. n - 1));
+ assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
+ */
+extern int vsnprintf(char * __restrict s, size_t n,
+ char const * __restrict format, va_list arg);
+
+/*@ assigns *(s + (0 ..));
+ assigns *(s + (0 ..)) \from *(format + (..)), arg;
+ */
+extern int vsprintf(char * __restrict s, char const * __restrict format,
+ va_list arg);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1;
+ assigns *stream, \result;
+ assigns *stream \from *stream;
+ assigns \result \from (indirect: *stream);
+ */
+extern int fgetc(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s);
+ ensures
+ terminated_string_on_success:
+ \result ≢ \null ⇒ valid_string(\old(s));
+ assigns *(s + (0 .. size)), \result;
+ assigns *(s + (0 .. size)) \from (indirect: size), (indirect: *stream);
+ assigns \result \from s, (indirect: size), (indirect: *stream);
+ */
+extern char *fgets(char * __restrict s, int size, FILE * __restrict stream);
+
+/*@ assigns *stream; */
+extern int fputc(int c, FILE *stream);
+
+/*@ assigns *stream;
+ assigns *stream \from *(s + (..)); */
+extern int fputs(char const * __restrict s, FILE * __restrict stream);
+
+/*@ assigns \result, *stream;
+ assigns \result \from *stream;
+ assigns *stream \from *stream;
+ */
+extern int getc(FILE *stream);
+
+/*@ assigns \result;
+ assigns \result \from *__fc_stdin; */
+extern int getchar(void);
+
+/*@ ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
+ assigns *(s + (..)), \result;
+ assigns *(s + (..)) \from *__fc_stdin;
+ assigns \result \from s, __fc_stdin;
+ */
+extern char *gets(char *s);
+
+/*@ assigns *stream;
+ assigns *stream \from c; */
+extern int putc(int c, FILE *stream);
+
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from c; */
+extern int putchar(int c);
+
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from *(s + (..)); */
+extern int puts(char const *s);
+
+/*@ assigns *stream;
+ assigns *stream \from c; */
+extern int ungetc(int c, FILE *stream);
+
+/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_read: \result ≤ \old(nmemb);
+ ensures
+ initialization:
+ \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1))
+ \from size, nmemb, *stream;
+ assigns \result \from size, *stream;
+ */
+extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
+ FILE * __restrict stream);
+
+/*@ requires
+ valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_written: \result ≤ \old(nmemb);
+ assigns *stream, \result;
+ assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
+ assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
+ */
+extern size_t fwrite(void const * __restrict ptr, size_t size, size_t nmemb,
+ FILE * __restrict stream);
+
+/*@ assigns *pos;
+ assigns *pos \from *stream; */
+extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
+
+/*@ requires valid_stream: \valid(stream);
+ requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ assigns *stream, \result, __fc_errno;
+ assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+ assigns \result
+ \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ assigns __fc_errno
+ \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ */
+extern int fseek(FILE *stream, long offset, int whence);
+
+/*@ assigns *stream;
+ assigns *stream \from *pos; */
+extern int fsetpos(FILE *stream, fpos_t const *pos);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures
+ success_or_error:
+ \result ≡ -1 ∨
+ (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *stream);
+ assigns __fc_errno \from (indirect: *stream);
+ */
+extern long ftell(FILE *stream);
+
+/*@ assigns *stream;
+ assigns *stream \from \nothing; */
+extern void rewind(FILE *stream);
+
+/*@ assigns *stream;
+ assigns *stream \from \nothing; */
+extern void clearerr(FILE *stream);
+
+/*@ assigns \result;
+ assigns \result \from *stream; */
+extern int feof(FILE *stream);
+
+/*@ assigns \result;
+ assigns \result \from *stream; */
+extern int fileno(FILE *stream);
+
+/*@ assigns *stream;
+ assigns *stream \from \nothing; */
+extern void flockfile(FILE *stream);
+
+/*@ assigns *stream;
+ assigns *stream \from \nothing; */
+extern void funlockfile(FILE *stream);
+
+/*@ assigns \result, *stream;
+ assigns \result \from \nothing;
+ assigns *stream \from \nothing;
+ */
+extern int ftrylockfile(FILE *stream);
+
+/*@ assigns \result;
+ assigns \result \from *stream; */
+extern int ferror(FILE *stream);
+
+/*@ assigns __fc_stdout;
+ assigns __fc_stdout \from __fc_errno, *(s + (..));
+ */
+extern void perror(char const *s);
+
+/*@ assigns \result, *stream;
+ assigns \result \from *stream;
+ assigns *stream \from *stream;
+ */
+extern int getc_unlocked(FILE *stream);
+
+/*@ assigns \result;
+ assigns \result \from *__fc_stdin; */
+extern int getchar_unlocked(void);
+
+/*@ assigns *stream;
+ assigns *stream \from c; */
+extern int putc_unlocked(int c, FILE *stream);
+
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from c; */
+extern int putchar_unlocked(int c);
+
+/*@ assigns *stream;
assigns *stream \from \nothing; */
extern void clearerr_unlocked(FILE *stream);
@@ -3797,273 +4168,6 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream)
return_label: return __retres;
}
-/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\dangling((char *)s + i);
- */
-/*@
-predicate empty_block{L}(void *s) =
- \block_length((char *)s) ≡ 0 ∧ \offset((char *)s) ≡ 0;
- */
-/*@
-predicate valid_or_empty{L}(void *s, size_t n) =
- (empty_block(s) ∨ \valid_read((char *)s)) ∧
- \valid((char *)s + (0 .. n - 1));
- */
-/*@
-predicate valid_read_or_empty{L}(void *s, size_t n) =
- (empty_block(s) ∨ \valid_read((char *)s)) ∧
- \valid_read((char *)s + (1 .. n - 1));
-
-*/
-int memcmp(void const *s1, void const *s2, size_t n);
-
-void *memchr(void const *s, int c, size_t n);
-
-void *memcpy(void * __restrict dest, void const * __restrict src, size_t n);
-
-void *memmove(void *dest, void const *src, size_t n);
-
-void *memset(void *s, int c, size_t n);
-
-size_t strlen(char const *s);
-
-size_t strnlen(char const *s, size_t maxlen);
-
-int strcmp(char const *s1, char const *s2);
-
-int strncmp(char const *s1, char const *s2, size_t n);
-
-/*@ requires valid_string_s1: valid_read_string(s1);
- requires valid_string_s2: valid_read_string(s2);
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
- */
-extern int strcoll(char const *s1, char const *s2);
-
-char *strchr(char const *s, int c);
-
-char *strrchr(char const *s, int c);
-
-/*@ requires valid_string_s: valid_read_string(s);
- requires valid_string_reject: valid_read_string(reject);
- ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
- assigns \result;
- assigns \result
- \from (indirect: *(s + (0 ..))), (indirect: *(reject + (0 ..)));
- */
-extern size_t strcspn(char const *s, char const *reject);
-
-/*@ requires valid_string_s: valid_read_string(s);
- requires valid_string_accept: valid_read_string(accept);
- ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
- assigns \result, \result;
- assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
- assigns \result
- \from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
- */
-extern size_t strspn(char const *s, char const *accept);
-
-/*@ requires valid_string_s: valid_read_string(s);
- requires valid_string_accept: valid_read_string(accept);
- ensures
- result_null_or_same_base:
- \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
- assigns \result;
- assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
- */
-extern char *strpbrk(char const *s, char const *accept);
-
-char *strstr(char const *haystack, char const *needle);
-
-char *__fc_strtok_ptr;
-/*@ requires valid_string_delim: valid_read_string(delim);
- assigns *(s + (0 ..)), *(__fc_strtok_ptr + (0 ..)), \result,
- __fc_strtok_ptr;
- assigns *(s + (0 ..))
- \from *(s + (0 ..)), (indirect: s), (indirect: __fc_strtok_ptr),
- (indirect: *(delim + (0 ..)));
- assigns *(__fc_strtok_ptr + (0 ..))
- \from *(__fc_strtok_ptr + (0 ..)), (indirect: s),
- (indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..)));
- assigns \result
- \from s, __fc_strtok_ptr, (indirect: *(s + (0 ..))),
- (indirect: *(__fc_strtok_ptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
- assigns __fc_strtok_ptr
- \from \old(__fc_strtok_ptr), s,
- (indirect: *(__fc_strtok_ptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
-
- behavior new_str:
- assumes s_not_null: s ≢ \null;
- requires
- valid_string_s_or_delim_not_found:
- valid_string(s) ∨
- (valid_read_string(s) ∧
- (∀ int i;
- 0 ≤ i < strlen(delim) ⇒
- ¬(strchr(s, *(delim + i)) ≡ \true)));
- ensures
- result_subset:
- \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
- ensures ptr_subset: \subset(__fc_strtok_ptr, \old(s) + (0 ..));
- assigns __fc_strtok_ptr, *(s + (0 ..)), \result;
- assigns __fc_strtok_ptr
- \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
- assigns *(s + (0 ..))
- \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
- assigns \result
- \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
-
- behavior resume_str:
- assumes s_null: s ≡ \null;
- requires not_first_call: __fc_strtok_ptr ≢ \null;
- ensures
- result_subset:
- \result ≡ \null ∨
- \subset(\result, \old(__fc_strtok_ptr) + (0 ..));
- ensures
- ptr_subset: \subset(__fc_strtok_ptr, \old(__fc_strtok_ptr) + (0 ..));
- assigns *(__fc_strtok_ptr + (0 ..)), __fc_strtok_ptr, \result;
- assigns *(__fc_strtok_ptr + (0 ..))
- \from *(__fc_strtok_ptr + (0 ..)), (indirect: __fc_strtok_ptr),
- (indirect: *(delim + (0 ..)));
- assigns __fc_strtok_ptr
- \from \old(__fc_strtok_ptr), (indirect: *(__fc_strtok_ptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
- assigns \result
- \from __fc_strtok_ptr, (indirect: *(__fc_strtok_ptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
-
- complete behaviors resume_str, new_str;
- disjoint behaviors resume_str, new_str;
- */
-extern char *strtok(char * __restrict s, char const * __restrict delim);
-
-/*@ requires valid_string_delim: valid_read_string(delim);
- requires valid_saveptr: \valid(saveptr);
- assigns *(s + (0 ..)), *(*saveptr + (0 ..)), \result, *saveptr;
- assigns *(s + (0 ..))
- \from *(s + (0 ..)), (indirect: s), (indirect: *saveptr),
- (indirect: *(delim + (0 ..)));
- assigns *(*saveptr + (0 ..))
- \from *(*saveptr + (0 ..)), (indirect: s), (indirect: *saveptr),
- (indirect: *(delim + (0 ..)));
- assigns \result
- \from s, *saveptr, (indirect: *(s + (0 ..))),
- (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..)));
- assigns *saveptr
- \from \old(*saveptr), s, (indirect: *(*saveptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
-
- behavior new_str:
- assumes s_not_null: s ≢ \null;
- requires
- valid_string_s_or_delim_not_found:
- valid_string(s) ∨
- (valid_read_string(s) ∧
- (∀ int i;
- 0 ≤ i < strlen(delim) ⇒
- ¬(strchr(s, *(delim + i)) ≡ \true)));
- ensures
- result_subset:
- \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
- ensures initialization: \initialized(\old(saveptr));
- ensures saveptr_subset: \subset(*\old(saveptr), \old(s) + (0 ..));
- assigns *saveptr, *(s + (0 ..)), \result;
- assigns *saveptr
- \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
- assigns *(s + (0 ..))
- \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..)));
- assigns \result
- \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..)));
-
- behavior resume_str:
- assumes s_null: s ≡ \null;
- requires not_first_call: *saveptr ≢ \null;
- requires initialization: saveptr: \initialized(saveptr);
- ensures
- result_subset:
- \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..));
- ensures
- saveptr_subset: \subset(*\old(saveptr), \old(*saveptr) + (0 ..));
- assigns *(*saveptr + (0 ..)), *saveptr, \result;
- assigns *(*saveptr + (0 ..))
- \from *(*saveptr + (0 ..)), (indirect: *saveptr),
- (indirect: *(delim + (0 ..)));
- assigns *saveptr
- \from \old(*saveptr), (indirect: *(*saveptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
- assigns \result
- \from *saveptr, (indirect: *(*saveptr + (0 ..))),
- (indirect: *(delim + (0 ..)));
-
- complete behaviors resume_str, new_str;
- disjoint behaviors resume_str, new_str;
- */
-extern char *strtok_r(char * __restrict s, char const * __restrict delim,
- char ** __restrict saveptr);
-
-/*@ requires
- valid_string_stringp: \valid(stringp) ∧ valid_string(*stringp);
- requires valid_string_delim: valid_read_string(delim);
- assigns *stringp, \result;
- assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
- assigns \result \from *(delim + (..)), *(*(stringp + (..)));
- */
-extern char *strsep(char **stringp, char const *delim);
-
-extern char __fc_strerror[64];
-
-char * const __fc_p_strerror = __fc_strerror;
-char *strerror(int errnum);
-
-char *strcpy(char *dest, char const *src);
-
-char *strncpy(char *dest, char const *src, size_t n);
-
-char *strcat(char *dest, char const *src);
-
-char *strncat(char *dest, char const *src, size_t n);
-
-/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
- requires valid_string_src: valid_read_string(src);
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1))
- \from (indirect: *(src + (0 ..))), (indirect: n);
- assigns \result \from dest;
- */
-extern size_t strxfrm(char * __restrict dest, char const * __restrict src,
- size_t n);
-
-char *strdup(char const *s);
-
-char *strndup(char const *s, size_t n);
-
-/*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
- ensures
- s_initialized: initialization:
- \initialized((char *)\old(s) + (0 .. \old(n) - 1));
- ensures
- zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
- assigns *((char *)s + (0 .. n - 1));
- assigns *((char *)s + (0 .. n - 1)) \from \nothing;
- */
-extern void bzero(void *s, size_t n);
-
-int strcasecmp(char const *s1, char const *s2);
-
-/*@ requires valid_string_s1: valid_read_nstring(s1, n);
- requires valid_string_s2: valid_read_nstring(s2, n);
- assigns \result;
- assigns \result
- \from (indirect: n), (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1)));
- */
-extern int strncasecmp(char const *s1, char const *s2, size_t n);
-
/*@ requires abs_representable: i > -2147483647 - 1;
assigns \result;
assigns \result \from i;
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index b8c3b75e0ae..d928b74c99c 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/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] ∈ [--..--]
--
GitLab