diff --git a/share/libc/string.h b/share/libc/string.h
index 6f265a44d012653bdfd2dfbf0b4e6405e3e81331..577f35be8e00ab415db3769659bece22017e3f30 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -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:
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 9deb0bc5e01c04aaea0bbf5178f55316e8f09166..8e73401933cf18244067ab5c84f7b50c269d724f 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -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.
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index ed172048f4c391e586f81f1d78820d16d0d48d97..dec8b3a4cc8155162a1e2336cb10f2045e874691 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -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);
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 93b9bdbbe40ccc606dcc5036e9f45a7a50c22751..7245bc0aa8f2903a460e474cf1ab66f61ba3d344 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -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:
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 01a4e906ea181e9a16394341b6a59aff9005809a..f07006ab7b9f349145414cf225baf363499be4b9 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -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:
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index 23daf7cb9257fd1bdee878600fe317860cfafaaa..41ee7f4cbff2f2b095c96af0332fb3ca82e2c204 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -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
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 55c5afe6dad117fc0beb325fa0f45052db727460..89300398e63a10d546dfe9bf14577b28a251225e 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -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}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 27065864dd54811732a6107eecaeca8386c9422f..0b264a615662d7fe36471bf30fbcea0f87dd90d7 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -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;
}