Commit 4eab981c authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/andre/libc-strchrnul' into 'master'

[Libc] add spec for GNU function strchrnul and improve strchr

See merge request frama-c/frama-c!2365
parents d991ac9c 618f21ce
......@@ -155,7 +155,7 @@ extern int strncmp (const char *s1, const char *s2, size_t n);
extern int strcoll (const char *s1, const char *s2);
/*@ requires valid_string_s: valid_read_string(s);
@ assigns \result \from s, s[0..],c;
@ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
@ behavior found:
@ assumes char_found: strchr(s,c);
@ ensures result_char: *\result == (char)c;
......@@ -172,6 +172,12 @@ extern int strcoll (const char *s1, const char *s2);
@*/
extern char *strchr(const char *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
@ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
@ ensures result_same_base: \subset(\result, s+(0..strlen(s)));
@*/
extern char *strchrnul(const char *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
@ assigns \result \from s, s[0..],c;
@ behavior found:
......
This diff is collapsed.
......@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 2 (out of 112)
Syntactically reachable functions = 2 (out of 113)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
......
......@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
Undefined functions (394)
Undefined functions (395)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
......@@ -142,23 +142,23 @@
sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
strcasestr (0 call); strcoll (0 call); strcspn (0 call); strftime (0 call);
strlcat (0 call); strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call);
strsep (0 call); strspn (0 call); strtod (0 call); strtof (0 call);
strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
system (0 call); tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call);
time (0 call); times (0 call); tmpfile (0 call); tmpnam (0 call);
trunc (0 call); truncf (0 call); truncl (0 call); ttyname (0 call);
tzset (0 call); umask (0 call); ungetc (0 call); unlink (0 call);
usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
wmemcmp (0 call); wmemmove (0 call); write (0 call);
strcasestr (0 call); strchrnul (0 call); strcoll (0 call); strcspn (0 call);
strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
ttyname (0 call); tzset (0 call); umask (0 call); ungetc (0 call);
unlink (0 call); usleep (0 call); utimes (0 call); vfprintf (0 call);
vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call);
vsprintf (0 call); vsyslog (0 call); wait (0 call); waitpid (0 call);
wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call);
'Extern' global variables (16)
==============================
......@@ -181,7 +181,7 @@
Goto = 89
Assignment = 438
Exit point = 82
Function = 476
Function = 477
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
......
......@@ -3999,6 +3999,15 @@ extern int strcoll(char const *s1, char const *s2);
char *strchr(char const *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
ensures
result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
assigns \result;
assigns \result
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
*/
extern char *strchrnul(char const *s, int c);
char *strrchr(char const *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
......@@ -5919,7 +5928,8 @@ char *strncpy(char *dest, char const *src, size_t n)
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
assigns \result
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≡ \true;
......
......@@ -21,6 +21,7 @@
\return(memmove) == 0 (auto)
\return(memset) == 0 (auto)
\return(strchr) == 0 (auto)
\return(strchrnul) == 0 (auto)
\return(strrchr) == 0 (auto)
\return(strpbrk) == 0 (auto)
\return(strstr) == 0 (auto)
......@@ -248,7 +249,7 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] share/libc/netdb.c:147:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:367:
[eva] share/libc/string.h:373:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strncpy
[eva] Recording results for gethostbyname
......
......@@ -105,7 +105,7 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/stdlib_c_env.c:15:
function strcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:351:
[eva] share/libc/string.h:357:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strcpy
[eva] computing for function getenv <- main.
......
......@@ -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:407:
[eva] share/libc/string.h:413:
function strcat: postcondition 'sum_of_lengths' got status valid.
[eva] share/libc/string.h:410:
[eva] share/libc/string.h:416:
function strcat: postcondition 'initialization,dest' got status valid.
[eva] share/libc/string.h:411:
[eva] share/libc/string.h:417:
function strcat: postcondition 'dest_null_terminated' got status valid.
[eva] share/libc/string.h:412:
[eva] share/libc/string.h:418:
function strcat: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcat
[eva] Done for function strcat
......@@ -559,11 +559,11 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/string_c.c:142:
function strcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:351:
[eva] share/libc/string.h:357:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva:alarm] share/libc/string.h:351: Warning:
[eva:alarm] share/libc/string.h:357: Warning:
function strcpy: postcondition 'equal_contents' got status unknown.
[eva] share/libc/string.h:352:
[eva] share/libc/string.h:358:
function strcpy: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcpy
[eva] Done for function strcpy
......@@ -603,13 +603,13 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:154:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:363:
[eva] share/libc/string.h:369:
function strncpy: postcondition 'result_ptr' got status valid.
[eva] share/libc/string.h:364:
[eva] share/libc/string.h:370:
function strncpy: postcondition 'initialization' got status valid.
[eva] share/libc/string.h:367:
[eva] share/libc/string.h:373:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva:alarm] share/libc/string.h:367: Warning:
[eva:alarm] share/libc/string.h:373: Warning:
function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
......@@ -623,9 +623,9 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:157:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:370:
[eva] share/libc/string.h:376:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva:alarm] share/libc/string.h:370: Warning:
[eva:alarm] share/libc/string.h:376: Warning:
function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
......@@ -712,13 +712,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:179:
[eva] share/libc/string.h:185:
function strrchr, behavior found: postcondition 'result_char' got status valid.
[eva] share/libc/string.h:180:
[eva] share/libc/string.h:186:
function strrchr, behavior found: postcondition 'result_same_base' got status valid.
[eva] share/libc/string.h:181:
function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva] share/libc/string.h:187:
function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva] share/libc/string.h:193:
function strrchr, behavior default: postcondition 'result_null_or_same_base' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
......@@ -728,7 +728,7 @@
[eva] tests/libc/string_c.c:216:
function strrchr: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.c:237: Reusing old results for call to strlen
[eva] share/libc/string.h:184:
[eva] share/libc/string.h:190:
function strrchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
......@@ -883,9 +883,9 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c.c:261:
function strstr: precondition 'valid_string_needle' got status valid.
[eva] share/libc/string.h:221:
[eva] share/libc/string.h:227:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva:alarm] share/libc/string.h:219: Warning:
[eva:alarm] share/libc/string.h:225: Warning:
function strstr: postcondition 'result_null_or_in_haystack' got status unknown.
[eva] Recording results for strstr
[eva] Done for function strstr
......@@ -905,7 +905,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c.c:265:
function strstr: precondition 'valid_string_needle' got status valid.
[eva] share/libc/string.h:219:
[eva] share/libc/string.h:225:
function strstr: postcondition 'result_null_or_in_haystack' got status valid.
[eva] Recording results for strstr
[eva] Done for function strstr
......
......@@ -12,11 +12,11 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/string_c_generic.c:56:
function strcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:351:
[eva] share/libc/string.h:357:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva:alarm] share/libc/string.h:351: Warning:
[eva:alarm] share/libc/string.h:357: Warning:
function strcpy: postcondition 'equal_contents' got status unknown.
[eva] share/libc/string.h:352:
[eva] share/libc/string.h:358:
function strcpy: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcpy
[eva] Done for function strcpy
......@@ -161,13 +161,13 @@
[eva] tests/libc/string_c_generic.c:73:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.c:220: starting to merge loop iterations
[eva] share/libc/string.h:363:
[eva] share/libc/string.h:369:
function strncpy: postcondition 'result_ptr' got status valid.
[eva] share/libc/string.h:364:
[eva] share/libc/string.h:370:
function strncpy: postcondition 'initialization' got status valid.
[eva] share/libc/string.h:367:
[eva] share/libc/string.h:373:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva:alarm] share/libc/string.h:367: Warning:
[eva:alarm] share/libc/string.h:373: Warning:
function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
......@@ -199,9 +199,9 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:78:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:370:
[eva] share/libc/string.h:376:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva:alarm] share/libc/string.h:370: Warning:
[eva:alarm] share/libc/string.h:376: Warning:
function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
......@@ -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:421:
[eva] share/libc/string.h:427:
function strncat: postcondition 'result_ptr' got status valid.
[eva] share/libc/string.h:436:
[eva] share/libc/string.h:442:
function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid.
[eva] Recording results for strncat
[eva] Done for function strncat
......@@ -312,13 +312,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:179:
[eva] share/libc/string.h:185:
function strrchr, behavior found: postcondition 'result_char' got status valid.
[eva] share/libc/string.h:180:
[eva] share/libc/string.h:186:
function strrchr, behavior found: postcondition 'result_same_base' got status valid.
[eva] share/libc/string.h:181:
function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva] share/libc/string.h:187:
function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva] share/libc/string.h:193:
function strrchr, behavior default: postcondition 'result_null_or_same_base' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
......@@ -328,7 +328,7 @@
function strrchr: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.c:237: Reusing old results for call to strlen
[eva] share/libc/string.c:237: starting to merge loop iterations
[eva] share/libc/string.h:184:
[eva] share/libc/string.h:190:
function strrchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
......
......@@ -10,7 +10,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c_strstr.c:52:
function strstr: precondition 'valid_string_needle' got status valid.
[eva] share/libc/string.h:219:
[eva] share/libc/string.h:225:
function strstr: postcondition 'result_null_or_in_haystack' got status valid.
[eva] Recording results for strstr
[eva] Done for function strstr
......@@ -101,9 +101,9 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c_strstr.c:64:
function strstr: precondition 'valid_string_needle' got status valid.
[eva] share/libc/string.h:221:
[eva] share/libc/string.h:227:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva:alarm] share/libc/string.h:219: Warning:
[eva:alarm] share/libc/string.h:225: Warning:
function strstr: postcondition 'result_null_or_in_haystack' got status unknown.
[eva] Recording results for strstr
[eva] Done for function strstr
......
......@@ -51,7 +51,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_h.c:24:
function strstr: precondition 'valid_string_needle' got status valid.
[eva] share/libc/string.h:221:
[eva] share/libc/string.h:227:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] Done for function strstr
[eva:alarm] tests/libc/string_h.c:25: Warning: assertion got status unknown.
......@@ -330,6 +330,23 @@
[eva] Done for function strlcpy
[eva] Recording results for test_strlcpy
[eva] Done for function test_strlcpy
[eva] tests/libc/string_h.c:154: Call to builtin strchr
[eva] tests/libc/string_h.c:154:
function strchr: precondition 'valid_string_s' got status valid.
[eva] computing for function strchrnul <- main.
Called from tests/libc/string_h.c:155.
[eva] using specification for function strchrnul
[eva] tests/libc/string_h.c:155:
function strchrnul: precondition 'valid_string_s' got status valid.
[eva] Done for function strchrnul
[eva] tests/libc/string_h.c:157: Call to builtin strchr
[eva] tests/libc/string_h.c:157:
function strchr: precondition 'valid_string_s' got status valid.
[eva] computing for function strchrnul <- main.
Called from tests/libc/string_h.c:158.
[eva] tests/libc/string_h.c:158:
function strchrnul: precondition 'valid_string_s' got status valid.
[eva] Done for function strchrnul
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
......@@ -395,4 +412,10 @@
a ∈ [--..--]
b ∈ [--..--]
strsig ∈ {{ &__fc_strsignal[0] }}
c ∈ {{ "haystack" }}
d ∈ {97; 110}
chr1 ∈ {{ "haystack" + {2; 7} }}
nul1 ∈ {{ "haystack" + [0..8] }}
chr2 ∈ {{ NULL ; "haystack" + {1} }}
nul2 ∈ {{ "haystack" + [0..8] }}
__retres ∈ {0}
......@@ -149,5 +149,12 @@ int main(int argc, char **argv)
//@ assert valid_read_string(strsig);
test_strncpy();
test_strlcpy();
char *c = "haystack";
char d = nondet ? 'y' : 'k';
char *chr1 = strchr(c, d);
char *nul1 = strchrnul(c, d);
d = nondet ? 'a' : 'n';
char *chr2 = strchr(c, d);
char *nul2 = strchrnul(c, d);
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