From 0b5b85945bbaec593f15015f90d3e37c862160f5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 4 Mar 2024 17:17:44 +0100
Subject: [PATCH] [libc] improve spec of strrchr
---
share/libc/string.h | 4 +-
tests/libc/oracle/string_h.res.oracle | 88 ++++++++++++++++-----------
tests/libc/string_h.c | 9 +++
3 files changed, 66 insertions(+), 35 deletions(-)
diff --git a/share/libc/string.h b/share/libc/string.h
index b775d0533d6..8125585d09b 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -195,7 +195,7 @@ extern char *strchr(const char *s, int c);
extern char *strchrnul(const char *s, int c);
/*@ 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 == c;
@@ -207,6 +207,8 @@ extern char *strchrnul(const char *s, int c);
@ behavior default:
@ ensures result_null_or_same_base:
@ \result == \null || \base_addr(\result) == \base_addr(s);
+ @ ensures result_null_or_points_to_same:
+ @ \result == \null || \subset(\result, s + (0 .. strlen(s)));
@*/
extern char *strrchr(const char *s, int c);
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index b30641505aa..86e86ce330f 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 string_h.c:139.
+ Called from string_h.c:147.
[eva] computing for function strcmp <- test_strcmp <- main.
Called from 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 string_h.c:140.
+ Called from string_h.c:148.
[eva] computing for function strcat <- test_strcat <- main.
Called from 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 string_h.c:141.
+ Called from string_h.c:149.
[eva] computing for function strstr <- test_strstr <- main.
Called from string_h.c:24.
[eva] using specification for function strstr
@@ -51,14 +51,14 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] string_h.c:24:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] FRAMAC_SHARE/libc/string.h:243:
+[eva] FRAMAC_SHARE/libc/string.h:245:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] Done for function strstr
[eva:alarm] string_h.c:25: Warning: assertion got status unknown.
[eva] Recording results for test_strstr
[eva] Done for function test_strstr
[eva] computing for function test_strncat <- main.
- Called from string_h.c:142.
+ Called from string_h.c:150.
[eva] string_h.c:34: Trace partitioning superposing up to 100 states
[eva] computing for function strncat <- test_strncat <- main.
Called from 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 string_h.c:143.
+ Called from string_h.c:151.
[eva] computing for function strcpy <- crashes_gcc <- main.
Called from 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 string_h.c:144.
+ Called from string_h.c:152.
[eva] computing for function strtok <- test_strtok <- main.
Called from string_h.c:58.
[eva] using specification for function strtok
@@ -148,7 +148,7 @@
[eva] Recording results for test_strtok
[eva] Done for function test_strtok
[eva] computing for function test_strtok_r <- main.
- Called from string_h.c:145.
+ Called from string_h.c:153.
[eva] computing for function strtok_r <- test_strtok_r <- main.
Called from string_h.c:82.
[eva] using specification for function strtok_r
@@ -233,32 +233,32 @@
[eva] Recording results for test_strtok_r
[eva] Done for function test_strtok_r
[eva] computing for function strdup <- main.
- Called from string_h.c:146.
+ Called from string_h.c:154.
[eva] using specification for function strdup
-[eva:libc:unsupported-spec] string_h.c:146: Warning:
+[eva:libc:unsupported-spec] string_h.c:154: Warning:
The specification of function 'strdup' is currently not supported by Eva.
Consider adding 'FRAMAC_SHARE/libc/string.c' to the analyzed source files.
-[eva] string_h.c:146: Warning: ignoring unsupported allocates clause
-[eva] string_h.c:146:
+[eva] string_h.c:154: Warning: ignoring unsupported allocates clause
+[eva] string_h.c:154:
function strdup: precondition 'valid_string_s' got status valid.
[eva] Done for function strdup
[eva] computing for function strndup <- main.
- Called from string_h.c:147.
+ Called from string_h.c:155.
[eva] using specification for function strndup
-[eva:libc:unsupported-spec] string_h.c:147: Warning:
+[eva:libc:unsupported-spec] string_h.c:155: Warning:
The specification of function 'strndup' is currently not supported by Eva.
Consider adding 'FRAMAC_SHARE/libc/string.c' to the analyzed source files.
-[eva] string_h.c:147: Warning: ignoring unsupported allocates clause
-[eva] string_h.c:147:
+[eva] string_h.c:155: Warning: ignoring unsupported allocates clause
+[eva] string_h.c:155:
function strndup: precondition 'valid_string_s' got status valid.
[eva] Done for function strndup
[eva] computing for function strsignal <- main.
- Called from string_h.c:148.
+ Called from string_h.c:156.
[eva] using specification for function strsignal
[eva] Done for function strsignal
-[eva] string_h.c:149: assertion got status valid.
+[eva] string_h.c:157: assertion got status valid.
[eva] computing for function test_strncpy <- main.
- Called from string_h.c:150.
+ Called from string_h.c:158.
[eva] computing for function strncpy <- test_strncpy <- main.
Called from string_h.c:113.
[eva] using specification for function strncpy
@@ -281,7 +281,7 @@
[eva] Recording results for test_strncpy
[eva] Done for function test_strncpy
[eva] computing for function test_strlcpy <- main.
- Called from string_h.c:151.
+ Called from string_h.c:159.
[eva] computing for function strlcpy <- test_strlcpy <- main.
Called from string_h.c:126.
[eva] using specification for function strlcpy
@@ -322,39 +322,56 @@
[eva] Done for function strlcpy
[eva] Recording results for test_strlcpy
[eva] Done for function test_strlcpy
-[eva] string_h.c:154: Call to builtin strchr
-[eva] string_h.c:154:
+[eva] computing for function test_strrchr <- main.
+ Called from string_h.c:160.
+[eva] computing for function strrchr <- test_strrchr <- main.
+ Called from string_h.c:139.
+[eva] using specification for function strrchr
+[eva] string_h.c:139:
+ function strrchr: precondition 'valid_string_s' got status valid.
+[eva] Done for function strrchr
+[eva:alarm] string_h.c:140: Warning: check got status unknown.
+[eva] computing for function strrchr <- test_strrchr <- main.
+ Called from string_h.c:141.
+[eva] string_h.c:141:
+ function strrchr: precondition 'valid_string_s' got status valid.
+[eva] Done for function strrchr
+[eva] string_h.c:142: check got status valid.
+[eva] Recording results for test_strrchr
+[eva] Done for function test_strrchr
+[eva] string_h.c:163: Call to builtin strchr
+[eva] string_h.c:163:
function strchr: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:181:
cannot evaluate ACSL term, unsupported logic var p
[eva] computing for function strchrnul <- main.
- Called from string_h.c:155.
+ Called from string_h.c:164.
[eva] using specification for function strchrnul
-[eva] string_h.c:155:
+[eva] string_h.c:164:
function strchrnul: precondition 'valid_string_s' got status valid.
[eva] Done for function strchrnul
-[eva] string_h.c:157: Call to builtin strchr
-[eva] string_h.c:157:
+[eva] string_h.c:166: Call to builtin strchr
+[eva] string_h.c:166:
function strchr: precondition 'valid_string_s' got status valid.
[eva] computing for function strchrnul <- main.
- Called from string_h.c:158.
-[eva] string_h.c:158:
+ Called from string_h.c:167.
+[eva] string_h.c:167:
function strchrnul: precondition 'valid_string_s' got status valid.
[eva] Done for function strchrnul
[eva] computing for function mempcpy <- main.
- Called from string_h.c:160.
+ Called from string_h.c:169.
[eva] using specification for function mempcpy
-[eva] string_h.c:160:
+[eva] string_h.c:169:
function mempcpy: precondition 'valid_dest' got status valid.
-[eva] string_h.c:160:
+[eva] string_h.c:169:
function mempcpy: precondition 'valid_src' got status valid.
-[eva] string_h.c:160:
+[eva] string_h.c:169:
function mempcpy: precondition 'separation' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:114:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[kernel] string_h.c:160: Warning: using size of 'void'
+[kernel] string_h.c:169: Warning: using size of 'void'
[eva] Done for function mempcpy
-[eva:alarm] string_h.c:161: Warning: assertion 'imprecise' got status unknown.
+[eva:alarm] string_h.c:170: Warning: assertion 'imprecise' got status unknown.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -393,6 +410,9 @@
src2[0] ∈ {97}
[1] ∈ {98}
[2] ∈ UNINITIALIZED
+[eva:final-states] Values at end of function test_strrchr:
+ s1 ∈ {{ "not a palyndrome" }}
+ p ∈ {0}
[eva:final-states] Values at end of function test_strstr:
s ∈ {{ "aba" ; "bab" }}
needle ∈ {{ "a" ; "b" }}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 1cdf89a28bc..84e8f246956 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -134,6 +134,14 @@ void test_strlcpy() {
}
}
+void test_strrchr() {
+ const char *s1 = "not a palyndrome";
+ const char *p = strrchr(s1, 'o');
+ //@ check p == s1 + strlen(s1) - 2;
+ p = strrchr(s1, 'Z');
+ //@ check p == \null;
+}
+
int main(int argc, char **argv)
{
test_strcmp();
@@ -149,6 +157,7 @@ int main(int argc, char **argv)
//@ assert valid_read_string(strsig);
test_strncpy();
test_strlcpy();
+ test_strrchr();
char *c = "haystack";
char d = nondet ? 'y' : 'k';
char *chr1 = strchr(c, d);
--
GitLab