Skip to content
Snippets Groups Projects
Commit ea4ffdac authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[libc] a few more fixes; test oracle updates

parent 011d9d2c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
share/libc/locale.c
+ 1
− 1
View file @ ea4ffdac
......@@ -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;
}
......
share/libc/netdb.c
+ 3
− 1
View file @ ea4ffdac
......@@ -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;
......
tests/libc/oracle/fc_libc.0.res.oracle
+ 10
− 10
View file @ ea4ffdac
......@@ -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"
......
tests/libc/oracle/fc_libc.1.res.oracle
+ 8
− 3
View file @ ea4ffdac
......@@ -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;
......
tests/libc/oracle/netdb_c.res.oracle
+ 48
− 30
View file @ ea4ffdac
......@@ -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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment