[libc] improve spec of strrchr

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);
 

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" }}

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);