Skip to content

GitLab

F
frama-c
Commit 53c35ea8 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files
Options

Merge branch 'fix/andre/libc-strncpy-spec' into 'master' 

[Libc] fix spec of strncpy

Closes #767

See merge request frama-c/frama-c!2477
parents 434a309e 8a541e84
Show whitespace changes
Inline Side-by-side
Showing with 178 additions and 99 deletions
share/libc/string.h
View file @ 53c35ea8
......@@ -354,7 +354,7 @@ extern char *strerror(int errnum);
extern char *strcpy(char *restrict dest, const char *restrict src);
/*@
@ 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 separation:
@ \separated(dest+(0..n-1), src+(0..n-1));
......@@ -372,7 +372,9 @@ extern char *strcpy(char *restrict dest, const char *restrict src);
extern char *strncpy(char *restrict dest,
const char *restrict src, size_t n);
/*@ // Non-POSIX, but often present
/*@ // Non-POSIX, but often present; note that, unlike strncpy, this has no
@ // "official specification" other than manpages. They state that src is
@ // a *string*, therefore its precondition is stricter than that of strncpy.
@ requires valid_string_src: valid_read_string(src);
@ requires room_nstring: \valid(dest+(0..n-1));
@ requires separation:
......@@ -475,7 +477,8 @@ extern size_t strxfrm (char *restrict dest,
@*/
extern char *strdup (const char *s);
/*@ allocates \result;
/*@ requires valid_string_s: valid_read_string(s);
@ allocates \result;
@ assigns \result \from indirect:s[0..strlen(s)], indirect:n,
@ indirect:__fc_heap_status;
@ behavior allocation:
......
tests/builtins/oracle/memcpy.res.oracle
View file @ 53c35ea8
......@@ -1575,11 +1575,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'bounded_result'
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.
[ Extern ] Froms (file share/libc/string.h, line 380)
[ Extern ] Froms (file share/libc/string.h, line 382)
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.
[ Valid ] Default behavior
by Frama-C kernel.
......@@ -1592,11 +1592,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'points_to_end'
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.
[ Extern ] Froms (file share/libc/string.h, line 392)
[ Extern ] Froms (file share/libc/string.h, line 394)
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.
[ Valid ] Default behavior
by Frama-C kernel.
......@@ -1613,11 +1613,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr'
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.
[ Extern ] Froms (file share/libc/string.h, line 403)
[ Extern ] Froms (file share/libc/string.h, line 405)
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.
[ Valid ] Default behavior
by Frama-C kernel.
......@@ -1632,24 +1632,24 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'partial' 'sum_of_bounded_lengths'
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.
[ Extern ] Assigns (file share/libc/string.h, line 417)
[ Extern ] Assigns (file share/libc/string.h, line 419)
Unverifiable but considered Valid.
[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 431)
Unverifiable but considered Valid.
[ Extern ] Froms for 'complete' (file share/libc/string.h, line 423)
[ 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 425)
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.
[ Extern ] Froms (file share/libc/string.h, line 418)
[ Extern ] Froms (file share/libc/string.h, line 419)
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.
[ Extern ] Froms for 'partial' (file share/libc/string.h, line 433)
Unverifiable but considered Valid.
[ Extern ] Froms for 'partial' (file share/libc/string.h, line 435)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete'
by Frama-C kernel.
[ Valid ] Default behavior
......@@ -1663,11 +1663,11 @@
[ Extern ] Post-condition 'bounded_result'
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.
[ Extern ] Froms (file share/libc/string.h, line 443)
[ Extern ] Froms (file share/libc/string.h, line 445)
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.
[ Valid ] Default behavior
by Frama-C kernel.
......@@ -1676,11 +1676,11 @@
--- 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.
[ Extern ] Froms (file share/libc/string.h, line 452)
[ Extern ] Froms (file share/libc/string.h, line 454)
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.
[ Valid ] Default behavior
by Frama-C kernel.
......@@ -1695,19 +1695,19 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null'
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.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing
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.
[ 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.
[ Extern ] Froms (file share/libc/string.h, line 462)
[ Extern ] Froms (file share/libc/string.h, line 464)
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.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
......@@ -1715,7 +1715,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
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.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
......@@ -1730,19 +1730,19 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null'
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.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing
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.
[ 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.
[ Extern ] Froms (file share/libc/string.h, line 479)
[ Extern ] Froms (file share/libc/string.h, line 482)
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.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
......@@ -1750,7 +1750,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
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.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
......@@ -1767,7 +1767,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
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.
[ Valid ] Default behavior
by Frama-C kernel.
......
tests/libc/oracle/fc_libc.1.res.oracle
View file @ 53c35ea8
......@@ -5858,7 +5858,7 @@ char *strcpy(char *dest, char const *src)
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 separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
......@@ -6145,7 +6145,8 @@ char *strdup(char const *s)
return_label: return __retres;
}
/*@ assigns \result;
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
......
tests/libc/oracle/netdb_c.res.oracle
View file @ 53c35ea8
......@@ -243,7 +243,7 @@
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.
function strncpy: precondition 'valid_nstring_src' got status valid.
[eva] share/libc/netdb.c:147:
function strncpy: precondition 'room_nstring' got status valid.
[eva] share/libc/netdb.c:147:
......
tests/libc/oracle/string_c.res.oracle
View file @ 53c35ea8
......@@ -494,13 +494,13 @@
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for 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.
[eva] share/libc/string.h:408:
[eva] share/libc/string.h:410:
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.
[eva] share/libc/string.h:410:
[eva] share/libc/string.h:412:
function strcat: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcat
[eva] Done for function strcat
......@@ -598,7 +598,7 @@
[eva] computing for function strncpy <- test_strncpy <- main.
Called from 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:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:154:
......@@ -618,7 +618,7 @@
[eva] computing for function strncpy <- test_strncpy <- main.
Called from 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:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:157:
......@@ -633,7 +633,7 @@
[eva] computing for function strncpy <- test_strncpy <- main.
Called from 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:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:159:
......@@ -644,7 +644,7 @@
[eva] computing for function strncpy <- test_strncpy <- main.
Called from 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:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:161:
......
tests/libc/oracle/string_c_generic.res.oracle
View file @ 53c35ea8
......@@ -155,7 +155,7 @@
[eva] computing for function strncpy <- main.
Called from 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:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:73:
......@@ -194,7 +194,7 @@
[eva] computing for function strncpy <- main.
Called from 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:
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:78:
......@@ -252,9 +252,9 @@
function strlen: postcondition 'acsl_c_equiv' got status valid.
[eva] Recording results for 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.
[eva] share/libc/string.h:434:
[eva] share/libc/string.h:436:
function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid.
[eva] Recording results for strncat
[eva] Done for function strncat
......
tests/libc/oracle/string_h.res.oracle
View file @ 53c35ea8
......@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[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.
Called from tests/libc/string_h.c:5.
[eva] using specification for function strcmp
......@@ -20,7 +20,7 @@
[eva] Recording results for test_strcmp
[eva] Done for function test_strcmp
[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.
Called from tests/libc/string_h.c:13.
[eva] using specification for function strcat
......@@ -43,7 +43,7 @@
[eva] Recording results for test_strcat
[eva] Done for function test_strcat
[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.
Called from tests/libc/string_h.c:24.
[eva] using specification for function strstr
......@@ -58,7 +58,7 @@
[eva] Recording results for test_strstr
[eva] Done for function test_strstr
[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] computing for function strncat <- test_strncat <- main.
Called from tests/libc/string_h.c:36.
......@@ -73,7 +73,7 @@
[eva] Recording results for test_strncat
[eva] Done for function test_strncat
[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.
Called from tests/libc/string_h.c:53.
[eva] using specification for function strcpy
......@@ -87,7 +87,7 @@
[eva] Recording results for crashes_gcc
[eva] Done for function crashes_gcc
[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.
Called from tests/libc/string_h.c:58.
[eva] using specification for function strtok
......@@ -152,7 +152,7 @@
[eva] Recording results for test_strtok
[eva] Done for function test_strtok
[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.
Called from tests/libc/string_h.c:82.
[eva] using specification for function strtok_r
......@@ -241,57 +241,95 @@
[eva] Recording results for test_strtok_r
[eva] Done for function test_strtok_r
[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: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.
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:119:
[eva] tests/libc/string_h.c:146: Warning: ignoring unsupported \allocates clause
[eva] tests/libc/string_h.c:146:
function strdup: precondition 'valid_string_s' got status valid.
[eva] Done for function strdup
[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: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.
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] computing for function strlcpy <- main.
Called from tests/libc/string_h.c:123.
[eva] computing for function strsignal <- main.
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] tests/libc/string_h.c:123:
[eva] tests/libc/string_h.c:126:
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.
[eva] tests/libc/string_h.c:123:
[eva] tests/libc/string_h.c:126:
function strlcpy: precondition 'separation' got status valid.
[eva] Done for function strlcpy
[eva] computing for function strlcpy <- main.
Called from tests/libc/string_h.c:124.
[eva] tests/libc/string_h.c:124:
[eva] computing for function strlcpy <- test_strlcpy <- main.
Called from tests/libc/string_h.c:127.
[eva] tests/libc/string_h.c:127:
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.
[eva] tests/libc/string_h.c:124:
[eva] tests/libc/string_h.c:127:
function strlcpy: precondition 'separation' got status valid.
[eva] Done for function strlcpy
[eva] computing for function strlcat <- main.
Called from tests/libc/string_h.c:125.
[eva] computing for function strlcat <- test_strlcpy <- main.
Called from tests/libc/string_h.c:128.
[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.
[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.
[eva] tests/libc/string_h.c:125:
[eva] tests/libc/string_h.c:128:
function strlcat: precondition 'room_nstring' got status valid.
[eva] Done for function strlcat
[eva] computing for function strsignal <- main.
Called from tests/libc/string_h.c:126.
[eva] using specification for function strsignal
[eva] Done for function strsignal
[eva] tests/libc/string_h.c:127: assertion got status valid.
[eva] computing for function strlcpy <- test_strlcpy <- main.
Called from tests/libc/string_h.c:132.
[eva:alarm] tests/libc/string_h.c:132: Warning:
function strlcpy: precondition 'valid_string_src' got status invalid.
[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] done for function main
[eva] ====== VALUES COMPUTED ======
......@@ -306,11 +344,30 @@
[6..9] ∈ UNINITIALIZED
[eva:final-states] Values at end of function test_strcmp:
res ∈ {0}
[eva:final-states] Values at end of function test_strlcpy:
buf[0..15] ∈ [--..--]
buf2[0..5] ∈ [--..--]
[6..31] ∈ [--..--] or UNINITIALIZED
r1 ∈ {18}
r2 ∈ {5}
r3 ∈ [--..--]
src[0] ∈ {97}
[1] ∈ {98}
[2] ∈ {99}
dst[0..2] ∈ UNINITIALIZED
[eva:final-states] Values at end of function test_strncat:
data[0] ∈ [--..--]
[1..99] ∈ [--..--] or UNINITIALIZED
source[0..98] ∈ {90}
[99] ∈ {0}
[eva:final-states] Values at end of function test_strncpy:
src[0] ∈ {97}
[1] ∈ {98}
[2] ∈ {99}
dst[0..2] ∈ [--..--]
src2[0] ∈ {97}
[1] ∈ {98}
[2] ∈ UNINITIALIZED
[eva:final-states] Values at end of function test_strstr:
s ∈ {{ "aba" ; "bab" }}
needle ∈ {{ "a" ; "b" }}
......@@ -337,11 +394,5 @@
__fc_strtok_ptr ∈ {{ "constant!" + [0..--] }}
a ∈ [--..--]
b ∈ [--..--]
buf[0..15] ∈ [--..--]
buf2[0..5] ∈ [--..--]
[6..31] ∈ [--..--] or UNINITIALIZED
r1 ∈ {18}
r2 ∈ {5}
r3 ∈ [--..--]
strsig ∈ {{ &__fc_strsignal[0] }}
__retres ∈ {0}
tests/libc/string_h.c
View file @ 53c35ea8
......@@ -107,6 +107,33 @@ void test_strtok_r() {
}
}
void test_strncpy() {
char src[] = { 'a', 'b', 'c' };
char dst[3];
strncpy(dst,src,3);
char src2[3];
src2[0] = 'a';
src2[1] = 'b';
if (nondet) {
strncpy(dst,src2,3);
//@ assert unreachable: \false;
}
}
void test_strlcpy() {
char buf[16];
char buf2[32];
size_t r1 = strlcpy(buf, "longer than buffer", 16);
size_t r2 = strlcpy(buf2, "short", 16);
size_t r3 = strlcat(buf2, buf, 32);
char src[] = { 'a', 'b', 'c' };
char dst[3];
if (nondet) {
strlcpy(dst,src,3);
//@ assert unreachable: \false;
}
}
int main(int argc, char **argv)
{
test_strcmp();
......@@ -118,12 +145,9 @@ int main(int argc, char **argv)
test_strtok_r();
char *a = strdup("bla"); // unsound; specification currently unsupported
char *b = strndup("bla", 2); // unsound; specification currently unsupported
char buf[16];
char buf2[32];
size_t r1 = strlcpy(buf, "longer than buffer", 16);
size_t r2 = strlcpy(buf2, "short", 16);
size_t r3 = strlcat(buf2, buf, 32);
char *strsig = strsignal(1);
//@ assert valid_read_string(strsig);
test_strncpy();
test_strlcpy();
return 0;
}
Markdown is supported
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