diff --git a/share/libc/locale.c b/share/libc/locale.c
index 4052774e8873ad93a712740ed8426ffe8a2f07d2..eb60516c520e490a92aeeaeb5228f8ce70a27632 100644
--- a/share/libc/locale.c
+++ b/share/libc/locale.c
@@ -35,7 +35,7 @@ const char *__frama_c_locale_names[512] = {"C"};
char *setlocale(int category, const char *locale) {
if (*locale == 'C')
{ __frama_c_locale = &__C_locale;
- return __frama_c_locale_names[0];
+ return (char*)__frama_c_locale_names[0];
};
return NULL;
}
diff --git a/share/libc/netdb.c b/share/libc/netdb.c
index 493d1fc84ae2450e5a5a17fe1a15da3983c0aa2e..c208d255aa940004a5719f9dd2b568dd1dbf0811 100644
--- a/share/libc/netdb.c
+++ b/share/libc/netdb.c
@@ -69,7 +69,9 @@ int getaddrinfo(
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_canonname = malloc(6);
+ if (!ai -> ai_canonname) return EAI_MEMORY;
+ strcpy(ai -> ai_canonname, "dummy");
ai -> ai_next = NULL;
*res = ai;
return 0;
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 021a17bb5853e7fe12f5ff54cf7256a8dc2baae8..7955573b0c8101d35d2a7b324dcc54e1a9266e80 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -37,7 +37,7 @@
posix_memalign (0 call); putenv (0 call); realpath (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);
+ strcpy (1 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); strsignal (0 call); strstr (0 call);
tolower (0 call); toupper (0 call); unsetenv (0 call); wcscat (0 call);
@@ -119,7 +119,7 @@
log10f (0 call); log10l (0 call); log2 (0 call); log2f (0 call);
log2l (0 call); logf (0 call); logl (0 call); longjmp (0 call);
lrand48 (0 call); lseek (0 call); lstat (0 call); makedev (0 call);
- malloc (9 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+ malloc (10 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
@@ -189,18 +189,18 @@
Global metrics
==============
- Sloc = 1140
- Decision point = 214
+ Sloc = 1145
+ Decision point = 215
Global variables = 86
- If = 199
+ If = 200
Loop = 43
- Goto = 98
- Assignment = 465
+ Goto = 99
+ Assignment = 466
Exit point = 84
Function = 500
- Function call = 96
- Pointer dereferencing = 159
- Cyclomatic complexity = 298
+ Function call = 98
+ Pointer dereferencing = 161
+ Cyclomatic complexity = 299
/* 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 7427bb1a8188a01036b73a5b0b9d85891cc8a6c2..7ede7566e8cec61541875f914b64a6038a2c83e4 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2740,7 +2740,7 @@ struct lconv __C_locale =
.int_p_sign_posn = (char)127,
.int_n_sign_posn = (char)127};
struct lconv *__frama_c_locale = & __C_locale;
-char *__frama_c_locale_names[512] = {(char *)"C"};
+char const *__frama_c_locale_names[512] = {"C"};
/*@ requires
locale_null_or_valid_string:
locale ≡ \null ∨ valid_read_string(locale);
@@ -2757,7 +2757,7 @@ char *setlocale(int category, char const *locale)
char *__retres;
if ((int)*locale == 'C') {
__frama_c_locale = & __C_locale;
- __retres = __frama_c_locale_names[0];
+ __retres = (char *)__frama_c_locale_names[0];
goto return_label;
}
__retres = (char *)0;
@@ -4399,7 +4399,12 @@ int getaddrinfo(char const * restrict nodename,
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_canonname = (char *)malloc((unsigned int)6);
+ if (! ai->ai_canonname) {
+ __retres = -10;
+ goto return_label;
+ }
+ strcpy(ai->ai_canonname,"dummy");
ai->ai_next = (struct addrinfo *)0;
*res = ai;
__retres = 0;
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index ad28a9c0f300e79e1e8f34ca36efbc7476c18e37..ce170ab4761f6c58b3616ea4f242c97c7524ccec 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -125,6 +125,20 @@
[eva] share/libc/netdb.c:69:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
+[eva] share/libc/netdb.c:72: Call to builtin malloc
+[eva] share/libc/netdb.c:72: allocating variable __malloc_getaddrinfo_l72
+[eva] computing for function strcpy <- getaddrinfo <- main.
+ Called from share/libc/netdb.c:74.
+[eva] using specification for function strcpy
+[eva] share/libc/netdb.c:74:
+ function strcpy: precondition 'valid_string_src' got status valid.
+[eva] share/libc/netdb.c:74:
+ function strcpy: precondition 'room_string' got status valid.
+[eva] share/libc/netdb.c:74:
+ function strcpy: precondition 'separation' got status valid.
+[eva] share/libc/string.h:360:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva] Done for function strcpy
[eva] Recording results for getaddrinfo
[eva] Done for function getaddrinfo
[eva] computing for function gai_strerror <- main.
@@ -180,74 +194,74 @@
[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.
+ Called from share/libc/netdb.c:141.
[eva] computing for function Frama_C_char_interval <- res_search <-
gethostbyname <- main.
- Called from share/libc/netdb.c:97.
+ Called from share/libc/netdb.c:99.
[eva] using specification for function Frama_C_char_interval
-[eva] share/libc/netdb.c:97:
+[eva] share/libc/netdb.c:99:
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.
+ Called from share/libc/netdb.c:99.
[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.
+ Called from share/libc/netdb.c:99.
[eva] Done for function Frama_C_char_interval
-[eva] share/libc/netdb.c:96: starting to merge loop iterations
+[eva] share/libc/netdb.c:98: starting to merge loop iterations
[eva] computing for function Frama_C_char_interval <- res_search <-
gethostbyname <- main.
- Called from share/libc/netdb.c:97.
+ Called from share/libc/netdb.c:99.
[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.
+ Called from share/libc/netdb.c:99.
[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.
+ Called from share/libc/netdb.c:99.
[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.
+ Called from share/libc/netdb.c:99.
[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:
+ Called from share/libc/netdb.c:102.
+[eva] share/libc/netdb.c:102:
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.
+ Called from share/libc/netdb.c:144.
[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.
+ Called from share/libc/netdb.c:147.
[eva] using specification for function inet_addr
-[eva] share/libc/netdb.c:145:
+[eva] share/libc/netdb.c:147:
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:
+[eva] share/libc/netdb.c:148: Call to builtin memcpy
+[eva] share/libc/netdb.c:148:
function memcpy: precondition 'valid_dest' got status valid.
-[eva] share/libc/netdb.c:146:
+[eva] share/libc/netdb.c:148:
function memcpy: precondition 'valid_src' got status valid.
-[eva] share/libc/netdb.c:146:
+[eva] share/libc/netdb.c:148:
function memcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:101:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] computing for function strncpy <- gethostbyname <- main.
- Called from share/libc/netdb.c:147.
+ Called from share/libc/netdb.c:149.
[eva] using specification for function strncpy
-[eva] share/libc/netdb.c:147:
+[eva] share/libc/netdb.c:149:
function strncpy: precondition 'valid_nstring_src' got status valid.
-[eva] share/libc/netdb.c:147:
+[eva] share/libc/netdb.c:149:
function strncpy: precondition 'room_nstring' got status valid.
-[eva] share/libc/netdb.c:147:
+[eva] share/libc/netdb.c:149:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:376:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
@@ -257,6 +271,11 @@
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[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 getaddrinfo:
__fc_errno ∈ [--..--]
__fc_heap_status ∈ [--..--]
@@ -271,15 +290,12 @@
.ai_addrlen ∈ {16} or UNINITIALIZED
.ai_addr ∈
{{ &__malloc_getaddrinfo_l58 }} or UNINITIALIZED
- .ai_canonname ∈ {{ "dummy" }} or UNINITIALIZED
+ .ai_canonname ∈
+ {{ NULL ; &__malloc_getaddrinfo_l72[0] }} 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}
+ __malloc_getaddrinfo_l72[0..5] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function gethostbyname:
Frama_C_entropy_source ∈ [--..--]
__fc_ghbn.host.h_name ∈ {{ NULL ; &__fc_ghbn.hostbuf[0] }}
@@ -332,7 +348,9 @@
.ai_protocol ∈ [0..256]
.ai_addrlen ∈ {16}
.ai_addr ∈ {{ &__malloc_getaddrinfo_l58 }}
- .ai_canonname ∈ {{ "dummy" }}
+ .ai_canonname ∈
+ {{ &__malloc_getaddrinfo_l72[0] }}
.ai_next ∈ {0}
__malloc_getaddrinfo_l58.sa_family ∈ [0..43]
.sa_data[0..13] ∈ [--..--]
+ __malloc_getaddrinfo_l72[0..5] ∈ [--..--] or UNINITIALIZED