Skip to content

GitLab

F
frama-c
Commit 8a541e84 authored by Andre Maroneze's avatar Andre Maroneze
Browse files
Options

update oracles

parent 80c09779
Hide whitespace changes
Inline Side-by-side
Showing with 143 additions and 91 deletions
tests/builtins/oracle/memcpy.res.oracle
View file @ 8a541e84
...@@ -1575,11 +1575,11 @@ ...@@ -1575,11 +1575,11 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Post-condition 'bounded_result' [ Extern ] Post-condition 'bounded_result'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/string.h, line 380) [ Extern ] Assigns (file share/libc/string.h, line 382)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 380) [ Extern ] Froms (file share/libc/string.h, line 382)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 381) [ Extern ] Froms (file share/libc/string.h, line 383)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Default behavior [ Valid ] Default behavior
by Frama-C kernel. by Frama-C kernel.
...@@ -1592,11 +1592,11 @@ ...@@ -1592,11 +1592,11 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Post-condition 'points_to_end' [ Extern ] Post-condition 'points_to_end'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/string.h, line 392) [ Extern ] Assigns (file share/libc/string.h, line 394)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 392) [ Extern ] Froms (file share/libc/string.h, line 394)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 393) [ Extern ] Froms (file share/libc/string.h, line 395)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Default behavior [ Valid ] Default behavior
by Frama-C kernel. by Frama-C kernel.
...@@ -1613,11 +1613,11 @@ ...@@ -1613,11 +1613,11 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr' [ Extern ] Post-condition 'result_ptr'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/string.h, line 403) [ Extern ] Assigns (file share/libc/string.h, line 405)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 403) [ Extern ] Froms (file share/libc/string.h, line 405)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 406) [ Extern ] Froms (file share/libc/string.h, line 408)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Default behavior [ Valid ] Default behavior
by Frama-C kernel. by Frama-C kernel.
...@@ -1632,24 +1632,24 @@ ...@@ -1632,24 +1632,24 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Post-condition for 'partial' 'sum_of_bounded_lengths' [ Extern ] Post-condition for 'partial' 'sum_of_bounded_lengths'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 423) [ Extern ] Assigns for 'complete' (file share/libc/string.h, line 425)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/string.h, line 417) [ Extern ] Assigns (file share/libc/string.h, line 419)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 431) [ Extern ] Assigns for 'partial' (file share/libc/string.h, line 433)
Unverifiable but considered Valid.
[ Extern ] Froms for 'complete' (file share/libc/string.h, line 423)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'complete' (file share/libc/string.h, line 425) [ Extern ] Froms for 'complete' (file share/libc/string.h, line 425)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 417) [ Extern ] Froms for 'complete' (file share/libc/string.h, line 427)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 418) [ Extern ] Froms (file share/libc/string.h, line 419)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'partial' (file share/libc/string.h, line 431) [ Extern ] Froms (file share/libc/string.h, line 420)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'partial' (file share/libc/string.h, line 433) [ Extern ] Froms for 'partial' (file share/libc/string.h, line 433)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'partial' (file share/libc/string.h, line 435)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete' [ Valid ] Behavior 'complete'
by Frama-C kernel. by Frama-C kernel.
[ Valid ] Default behavior [ Valid ] Default behavior
...@@ -1663,11 +1663,11 @@ ...@@ -1663,11 +1663,11 @@
[ Extern ] Post-condition 'bounded_result' [ Extern ] Post-condition 'bounded_result'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/string.h, line 443) [ Extern ] Assigns (file share/libc/string.h, line 445)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 443) [ Extern ] Froms (file share/libc/string.h, line 445)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 444) [ Extern ] Froms (file share/libc/string.h, line 446)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Default behavior [ Valid ] Default behavior
by Frama-C kernel. by Frama-C kernel.
...@@ -1676,11 +1676,11 @@ ...@@ -1676,11 +1676,11 @@
--- Properties of Function 'strxfrm' --- Properties of Function 'strxfrm'
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
[ Extern ] Assigns (file share/libc/string.h, line 452) [ Extern ] Assigns (file share/libc/string.h, line 454)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 452) [ Extern ] Froms (file share/libc/string.h, line 454)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 453) [ Extern ] Froms (file share/libc/string.h, line 455)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Default behavior [ Valid ] Default behavior
by Frama-C kernel. by Frama-C kernel.
...@@ -1695,19 +1695,19 @@ ...@@ -1695,19 +1695,19 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null' [ Extern ] Post-condition for 'no_allocation' 'result_null'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 465) [ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 467)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns nothing [ Extern ] Assigns nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing [ Extern ] Assigns for 'no_allocation' nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 465) [ Extern ] Froms for 'allocation' (file share/libc/string.h, line 467)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 466) [ Extern ] Froms for 'allocation' (file share/libc/string.h, line 468)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 462) [ Extern ] Froms (file share/libc/string.h, line 464)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 472) [ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 474)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation' [ Valid ] Behavior 'allocation'
by Frama-C kernel. by Frama-C kernel.
...@@ -1715,7 +1715,7 @@ ...@@ -1715,7 +1715,7 @@
by Frama-C kernel. by Frama-C kernel.
[ Valid ] Behavior 'no_allocation' [ Valid ] Behavior 'no_allocation'
by Frama-C kernel. by Frama-C kernel.
[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 461) [ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 463)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing [ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
...@@ -1730,19 +1730,19 @@ ...@@ -1730,19 +1730,19 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null' [ Extern ] Post-condition for 'no_allocation' 'result_null'
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 483) [ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 486)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns nothing [ Extern ] Assigns nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing [ Extern ] Assigns for 'no_allocation' nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 483) [ Extern ] Froms for 'allocation' (file share/libc/string.h, line 486)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 484) [ Extern ] Froms for 'allocation' (file share/libc/string.h, line 487)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 479) [ Extern ] Froms (file share/libc/string.h, line 482)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 493) [ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 496)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation' [ Valid ] Behavior 'allocation'
by Frama-C kernel. by Frama-C kernel.
...@@ -1750,7 +1750,7 @@ ...@@ -1750,7 +1750,7 @@
by Frama-C kernel. by Frama-C kernel.
[ Valid ] Behavior 'no_allocation' [ Valid ] Behavior 'no_allocation'
by Frama-C kernel. by Frama-C kernel.
[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 478) [ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 481)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing [ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
...@@ -1767,7 +1767,7 @@ ...@@ -1767,7 +1767,7 @@
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Assigns nothing [ Extern ] Assigns nothing
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/string.h, line 509) [ Extern ] Froms (file share/libc/string.h, line 512)
Unverifiable but considered Valid. Unverifiable but considered Valid.
[ Valid ] Default behavior [ Valid ] Default behavior
by Frama-C kernel. by Frama-C kernel.
......
tests/libc/oracle/fc_libc.1.res.oracle
View file @ 8a541e84
...@@ -5858,7 +5858,7 @@ char *strcpy(char *dest, char const *src) ...@@ -5858,7 +5858,7 @@ char *strcpy(char *dest, char const *src)
return dest; return dest;
} }
/*@ requires valid_string_src: valid_read_string(src); /*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1)); requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1)); requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest); ensures result_ptr: \result ≡ \old(dest);
...@@ -6145,7 +6145,8 @@ char *strdup(char const *s) ...@@ -6145,7 +6145,8 @@ char *strdup(char const *s)
return_label: return __retres; return_label: return __retres;
} }
/*@ assigns \result; /*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n), \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status); (indirect: __fc_heap_status);
......
tests/libc/oracle/netdb_c.res.oracle
View file @ 8a541e84
...@@ -243,7 +243,7 @@ ...@@ -243,7 +243,7 @@
Called from share/libc/netdb.c:147. Called from share/libc/netdb.c:147.
[eva] using specification for function strncpy [eva] using specification for function strncpy
[eva] share/libc/netdb.c:147: [eva] share/libc/netdb.c:147:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] share/libc/netdb.c:147: [eva] share/libc/netdb.c:147:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] share/libc/netdb.c:147: [eva] share/libc/netdb.c:147:
......
tests/libc/oracle/string_c.res.oracle
View file @ 8a541e84
...@@ -494,13 +494,13 @@ ...@@ -494,13 +494,13 @@
function strlen: precondition 'valid_string_s' got status valid. function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen [eva] Recording results for strlen
[eva] Done for function strlen [eva] Done for function strlen
[eva] share/libc/string.h:405: [eva] share/libc/string.h:407:
function strcat: postcondition 'sum_of_lengths' got status valid. function strcat: postcondition 'sum_of_lengths' got status valid.
[eva] share/libc/string.h:408: [eva] share/libc/string.h:410:
function strcat: postcondition 'initialization,dest' got status valid. function strcat: postcondition 'initialization,dest' got status valid.
[eva] share/libc/string.h:409: [eva] share/libc/string.h:411:
function strcat: postcondition 'dest_null_terminated' got status valid. function strcat: postcondition 'dest_null_terminated' got status valid.
[eva] share/libc/string.h:410: [eva] share/libc/string.h:412:
function strcat: postcondition 'result_ptr' got status valid. function strcat: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcat [eva] Recording results for strcat
[eva] Done for function strcat [eva] Done for function strcat
...@@ -598,7 +598,7 @@ ...@@ -598,7 +598,7 @@
[eva] computing for function strncpy <- test_strncpy <- main. [eva] computing for function strncpy <- test_strncpy <- main.
Called from tests/libc/string_c.c:154. Called from tests/libc/string_c.c:154.
[eva] tests/libc/string_c.c:154: [eva] tests/libc/string_c.c:154:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_c.c:154: [eva] tests/libc/string_c.c:154:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:154: [eva] tests/libc/string_c.c:154:
...@@ -618,7 +618,7 @@ ...@@ -618,7 +618,7 @@
[eva] computing for function strncpy <- test_strncpy <- main. [eva] computing for function strncpy <- test_strncpy <- main.
Called from tests/libc/string_c.c:157. Called from tests/libc/string_c.c:157.
[eva] tests/libc/string_c.c:157: [eva] tests/libc/string_c.c:157:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_c.c:157: [eva] tests/libc/string_c.c:157:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:157: [eva] tests/libc/string_c.c:157:
...@@ -633,7 +633,7 @@ ...@@ -633,7 +633,7 @@
[eva] computing for function strncpy <- test_strncpy <- main. [eva] computing for function strncpy <- test_strncpy <- main.
Called from tests/libc/string_c.c:159. Called from tests/libc/string_c.c:159.
[eva] tests/libc/string_c.c:159: [eva] tests/libc/string_c.c:159:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_c.c:159: [eva] tests/libc/string_c.c:159:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:159: [eva] tests/libc/string_c.c:159:
...@@ -644,7 +644,7 @@ ...@@ -644,7 +644,7 @@
[eva] computing for function strncpy <- test_strncpy <- main. [eva] computing for function strncpy <- test_strncpy <- main.
Called from tests/libc/string_c.c:161. Called from tests/libc/string_c.c:161.
[eva] tests/libc/string_c.c:161: [eva] tests/libc/string_c.c:161:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_c.c:161: [eva] tests/libc/string_c.c:161:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:161: [eva] tests/libc/string_c.c:161:
......
tests/libc/oracle/string_c_generic.res.oracle
View file @ 8a541e84
...@@ -155,7 +155,7 @@ ...@@ -155,7 +155,7 @@
[eva] computing for function strncpy <- main. [eva] computing for function strncpy <- main.
Called from tests/libc/string_c_generic.c:73. Called from tests/libc/string_c_generic.c:73.
[eva] tests/libc/string_c_generic.c:73: [eva] tests/libc/string_c_generic.c:73:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_c_generic.c:73: [eva] tests/libc/string_c_generic.c:73:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:73: [eva] tests/libc/string_c_generic.c:73:
...@@ -194,7 +194,7 @@ ...@@ -194,7 +194,7 @@
[eva] computing for function strncpy <- main. [eva] computing for function strncpy <- main.
Called from tests/libc/string_c_generic.c:78. Called from tests/libc/string_c_generic.c:78.
[eva] tests/libc/string_c_generic.c:78: [eva] tests/libc/string_c_generic.c:78:
function strncpy: precondition 'valid_string_src' got status valid. function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_c_generic.c:78: [eva] tests/libc/string_c_generic.c:78:
function strncpy: precondition 'room_nstring' got status valid. function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:78: [eva] tests/libc/string_c_generic.c:78:
...@@ -252,9 +252,9 @@ ...@@ -252,9 +252,9 @@
function strlen: postcondition 'acsl_c_equiv' got status valid. function strlen: postcondition 'acsl_c_equiv' got status valid.
[eva] Recording results for strlen [eva] Recording results for strlen
[eva] Done for function strlen [eva] Done for function strlen
[eva] share/libc/string.h:419: [eva] share/libc/string.h:421:
function strncat: postcondition 'result_ptr' got status valid. function strncat: postcondition 'result_ptr' got status valid.
[eva] share/libc/string.h:434: [eva] share/libc/string.h:436:
function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid. function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid.
[eva] Recording results for strncat [eva] Recording results for strncat
[eva] Done for function strncat [eva] Done for function strncat
......
tests/libc/oracle/string_h.res.oracle
View file @ 8a541e84
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
nondet ∈ [--..--] nondet ∈ [--..--]
[eva] computing for function test_strcmp <- main. [eva] computing for function test_strcmp <- main.
Called from tests/libc/string_h.c:112. Called from tests/libc/string_h.c:139.
[eva] computing for function strcmp <- test_strcmp <- main. [eva] computing for function strcmp <- test_strcmp <- main.
Called from tests/libc/string_h.c:5. Called from tests/libc/string_h.c:5.
[eva] using specification for function strcmp [eva] using specification for function strcmp
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
[eva] Recording results for test_strcmp [eva] Recording results for test_strcmp
[eva] Done for function test_strcmp [eva] Done for function test_strcmp
[eva] computing for function test_strcat <- main. [eva] computing for function test_strcat <- main.
Called from tests/libc/string_h.c:113. Called from tests/libc/string_h.c:140.
[eva] computing for function strcat <- test_strcat <- main. [eva] computing for function strcat <- test_strcat <- main.
Called from tests/libc/string_h.c:13. Called from tests/libc/string_h.c:13.
[eva] using specification for function strcat [eva] using specification for function strcat
...@@ -43,7 +43,7 @@ ...@@ -43,7 +43,7 @@
[eva] Recording results for test_strcat [eva] Recording results for test_strcat
[eva] Done for function test_strcat [eva] Done for function test_strcat
[eva] computing for function test_strstr <- main. [eva] computing for function test_strstr <- main.
Called from tests/libc/string_h.c:114. Called from tests/libc/string_h.c:141.
[eva] computing for function strstr <- test_strstr <- main. [eva] computing for function strstr <- test_strstr <- main.
Called from tests/libc/string_h.c:24. Called from tests/libc/string_h.c:24.
[eva] using specification for function strstr [eva] using specification for function strstr
...@@ -58,7 +58,7 @@ ...@@ -58,7 +58,7 @@
[eva] Recording results for test_strstr [eva] Recording results for test_strstr
[eva] Done for function test_strstr [eva] Done for function test_strstr
[eva] computing for function test_strncat <- main. [eva] computing for function test_strncat <- main.
Called from tests/libc/string_h.c:115. Called from tests/libc/string_h.c:142.
[eva] tests/libc/string_h.c:34: Trace partitioning superposing up to 100 states [eva] tests/libc/string_h.c:34: Trace partitioning superposing up to 100 states
[eva] computing for function strncat <- test_strncat <- main. [eva] computing for function strncat <- test_strncat <- main.
Called from tests/libc/string_h.c:36. Called from tests/libc/string_h.c:36.
...@@ -73,7 +73,7 @@ ...@@ -73,7 +73,7 @@
[eva] Recording results for test_strncat [eva] Recording results for test_strncat
[eva] Done for function test_strncat [eva] Done for function test_strncat
[eva] computing for function crashes_gcc <- main. [eva] computing for function crashes_gcc <- main.
Called from tests/libc/string_h.c:116. Called from tests/libc/string_h.c:143.
[eva] computing for function strcpy <- crashes_gcc <- main. [eva] computing for function strcpy <- crashes_gcc <- main.
Called from tests/libc/string_h.c:53. Called from tests/libc/string_h.c:53.
[eva] using specification for function strcpy [eva] using specification for function strcpy
...@@ -87,7 +87,7 @@ ...@@ -87,7 +87,7 @@
[eva] Recording results for crashes_gcc [eva] Recording results for crashes_gcc
[eva] Done for function crashes_gcc [eva] Done for function crashes_gcc
[eva] computing for function test_strtok <- main. [eva] computing for function test_strtok <- main.
Called from tests/libc/string_h.c:117. Called from tests/libc/string_h.c:144.
[eva] computing for function strtok <- test_strtok <- main. [eva] computing for function strtok <- test_strtok <- main.
Called from tests/libc/string_h.c:58. Called from tests/libc/string_h.c:58.
[eva] using specification for function strtok [eva] using specification for function strtok
...@@ -152,7 +152,7 @@ ...@@ -152,7 +152,7 @@
[eva] Recording results for test_strtok [eva] Recording results for test_strtok
[eva] Done for function test_strtok [eva] Done for function test_strtok
[eva] computing for function test_strtok_r <- main. [eva] computing for function test_strtok_r <- main.
Called from tests/libc/string_h.c:118. Called from tests/libc/string_h.c:145.
[eva] computing for function strtok_r <- test_strtok_r <- main. [eva] computing for function strtok_r <- test_strtok_r <- main.
Called from tests/libc/string_h.c:82. Called from tests/libc/string_h.c:82.
[eva] using specification for function strtok_r [eva] using specification for function strtok_r
...@@ -241,57 +241,95 @@ ...@@ -241,57 +241,95 @@
[eva] Recording results for test_strtok_r [eva] Recording results for test_strtok_r
[eva] Done for function test_strtok_r [eva] Done for function test_strtok_r
[eva] computing for function strdup <- main. [eva] computing for function strdup <- main.
Called from tests/libc/string_h.c:119. Called from tests/libc/string_h.c:146.
[eva] using specification for function strdup [eva] using specification for function strdup
[eva:libc:unsupported-spec] tests/libc/string_h.c:119: Warning: [eva:libc:unsupported-spec] tests/libc/string_h.c:146: Warning:
The specification of function 'strdup' is currently not supported by Eva. The specification of function 'strdup' is currently not supported by Eva.
Consider adding ./share/libc/string.c to the analyzed source files. Consider adding ./share/libc/string.c to the analyzed source files.
[eva] tests/libc/string_h.c:119: Warning: ignoring unsupported \allocates clause [eva] tests/libc/string_h.c:146: Warning: ignoring unsupported \allocates clause
[eva] tests/libc/string_h.c:119: [eva] tests/libc/string_h.c:146:
function strdup: precondition 'valid_string_s' got status valid. function strdup: precondition 'valid_string_s' got status valid.
[eva] Done for function strdup [eva] Done for function strdup
[eva] computing for function strndup <- main. [eva] computing for function strndup <- main.
Called from tests/libc/string_h.c:120. Called from tests/libc/string_h.c:147.
[eva] using specification for function strndup [eva] using specification for function strndup
[eva:libc:unsupported-spec] tests/libc/string_h.c:120: Warning: [eva:libc:unsupported-spec] tests/libc/string_h.c:147: Warning:
The specification of function 'strndup' is currently not supported by Eva. The specification of function 'strndup' is currently not supported by Eva.
Consider adding ./share/libc/string.c to the analyzed source files. Consider adding ./share/libc/string.c to the analyzed source files.
[eva] tests/libc/string_h.c:120: Warning: ignoring unsupported \allocates clause [eva] tests/libc/string_h.c:147: Warning: ignoring unsupported \allocates clause
[eva] tests/libc/string_h.c:147:
function strndup: precondition 'valid_string_s' got status valid.
[eva] Done for function strndup [eva] Done for function strndup
[eva] computing for function strlcpy <- main. [eva] computing for function strsignal <- main.
Called from tests/libc/string_h.c:123. Called from tests/libc/string_h.c:148.
[eva] using specification for function strsignal
[eva] Done for function strsignal
[eva] tests/libc/string_h.c:149: assertion got status valid.
[eva] computing for function test_strncpy <- main.
Called from tests/libc/string_h.c:150.
[eva] computing for function strncpy <- test_strncpy <- main.
Called from tests/libc/string_h.c:113.
[eva] using specification for function strncpy
[eva] tests/libc/string_h.c:113:
function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] tests/libc/string_h.c:113:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_h.c:113:
function strncpy: precondition 'separation' got status valid.
[eva] Done for function strncpy
[eva] computing for function strncpy <- test_strncpy <- main.
Called from tests/libc/string_h.c:118.
[eva:alarm] tests/libc/string_h.c:118: Warning:
function strncpy: precondition 'valid_nstring_src' got status invalid.
[eva] tests/libc/string_h.c:118:
function strncpy: no state left, precondition 'room_nstring' got status valid.
[eva] tests/libc/string_h.c:118:
function strncpy: no state left, precondition 'separation' got status valid.
[eva] Done for function strncpy
[eva] Recording results for test_strncpy
[eva] Done for function test_strncpy
[eva] computing for function test_strlcpy <- main.
Called from tests/libc/string_h.c:151.
[eva] computing for function strlcpy <- test_strlcpy <- main.
Called from tests/libc/string_h.c:126.
[eva] using specification for function strlcpy [eva] using specification for function strlcpy
[eva] tests/libc/string_h.c:123: [eva] tests/libc/string_h.c:126:
function strlcpy: precondition 'valid_string_src' got status valid. function strlcpy: precondition 'valid_string_src' got status valid.
[eva] tests/libc/string_h.c:123: [eva] tests/libc/string_h.c:126:
function strlcpy: precondition 'room_nstring' got status valid. function strlcpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_h.c:123: [eva] tests/libc/string_h.c:126:
function strlcpy: precondition 'separation' got status valid. function strlcpy: precondition 'separation' got status valid.
[eva] Done for function strlcpy [eva] Done for function strlcpy
[eva] computing for function strlcpy <- main. [eva] computing for function strlcpy <- test_strlcpy <- main.
Called from tests/libc/string_h.c:124. Called from tests/libc/string_h.c:127.
[eva] tests/libc/string_h.c:124: [eva] tests/libc/string_h.c:127:
function strlcpy: precondition 'valid_string_src' got status valid. function strlcpy: precondition 'valid_string_src' got status valid.
[eva] tests/libc/string_h.c:124: [eva] tests/libc/string_h.c:127:
function strlcpy: precondition 'room_nstring' got status valid. function strlcpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_h.c:124: [eva] tests/libc/string_h.c:127:
function strlcpy: precondition 'separation' got status valid. function strlcpy: precondition 'separation' got status valid.
[eva] Done for function strlcpy [eva] Done for function strlcpy
[eva] computing for function strlcat <- main. [eva] computing for function strlcat <- test_strlcpy <- main.
Called from tests/libc/string_h.c:125. Called from tests/libc/string_h.c:128.
[eva] using specification for function strlcat [eva] using specification for function strlcat
[eva:alarm] tests/libc/string_h.c:125: Warning: [eva:alarm] tests/libc/string_h.c:128: Warning:
function strlcat: precondition 'valid_string_src' got status unknown. function strlcat: precondition 'valid_string_src' got status unknown.
[eva:alarm] tests/libc/string_h.c:125: Warning: [eva:alarm] tests/libc/string_h.c:128: Warning:
function strlcat: precondition 'valid_string_dest' got status unknown. function strlcat: precondition 'valid_string_dest' got status unknown.
[eva] tests/libc/string_h.c:125: [eva] tests/libc/string_h.c:128:
function strlcat: precondition 'room_nstring' got status valid. function strlcat: precondition 'room_nstring' got status valid.
[eva] Done for function strlcat [eva] Done for function strlcat
[eva] computing for function strsignal <- main. [eva] computing for function strlcpy <- test_strlcpy <- main.
Called from tests/libc/string_h.c:126. Called from tests/libc/string_h.c:132.
[eva] using specification for function strsignal [eva:alarm] tests/libc/string_h.c:132: Warning:
[eva] Done for function strsignal function strlcpy: precondition 'valid_string_src' got status invalid.
[eva] tests/libc/string_h.c:127: assertion got status valid. [eva] tests/libc/string_h.c:132:
function strlcpy: no state left, precondition 'room_nstring' got status valid.
[eva] tests/libc/string_h.c:132:
function strlcpy: no state left, precondition 'separation' got status valid.
[eva] Done for function strlcpy
[eva] Recording results for test_strlcpy
[eva] Done for function test_strlcpy
[eva] Recording results for main [eva] Recording results for main
[eva] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
...@@ -306,11 +344,30 @@ ...@@ -306,11 +344,30 @@
[6..9] ∈ UNINITIALIZED [6..9] ∈ UNINITIALIZED
[eva:final-states] Values at end of function test_strcmp: [eva:final-states] Values at end of function test_strcmp:
res ∈ {0} res ∈ {0}
[eva:final-states] Values at end of function test_strlcpy: