diff --git a/share/libc/string.h b/share/libc/string.h
index 8125585d09b04a6d307b4e5b17344cda1ef6ce34..d021f5a873f05884e6529b23552252a86c65b170 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -88,6 +88,24 @@ extern int memcmp (const void *s1, const void *s2, size_t n);
 extern void *memchr(const void *s, int c, size_t n);
 
 // Non-POSIX; GNU extension
+// Note: these specifications are simplified w.r.t memchr's; in particular,
+// since we start searching from the end of the string, we assume the entire
+// string is valid, initialized, non-escaping, etc.
+/*@
+  requires valid: valid_read_or_empty(s, n);
+  requires initialization: \initialized(((unsigned char*)s)+(0 .. n - 1));
+  requires danglingness: non_escaping(s, n);
+  assigns \result \from s, indirect:c, indirect:((unsigned char*)s)[0..n-1];
+  behavior found:
+    assumes char_found: memchr((char*)s,c,n);
+    ensures result_same_base: \base_addr(\result) == \base_addr(s);
+    ensures result_points_to_same_base: \subset(\result, s+(0 .. n));
+  behavior not_found:
+    assumes char_not_found: !memchr((char*)s,c,n);
+    ensures result_null: \result == \null;
+  complete behaviors;
+  disjoint behaviors;
+*/
 extern void *memrchr(const void *s, int c, size_t n);
 
 // Copy memory
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 86e86ce330f9298a749647abbd18eae41ff32308..62c225c8140534ab341e6530a4dfee59ae1f1ef6 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -13,7 +13,7 @@
   function strcmp: precondition 'valid_string_s1' got status valid.
 [eva] string_h.c:5: 
   function strcmp: precondition 'valid_string_s2' got status valid.
-[eva] FRAMAC_SHARE/libc/string.h:156: 
+[eva] FRAMAC_SHARE/libc/string.h:174: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
 [eva] Done for function strcmp
 [eva:alarm] string_h.c:6: Warning: assertion got status unknown.
@@ -51,7 +51,7 @@
   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:245: 
+[eva] FRAMAC_SHARE/libc/string.h:263: 
   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.
@@ -342,7 +342,7 @@
 [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: 
+[eva] FRAMAC_SHARE/libc/string.h:199: 
   cannot evaluate ACSL term, unsupported logic var p
 [eva] computing for function strchrnul <- main.
   Called from string_h.c:164.
@@ -367,11 +367,42 @@
   function mempcpy: precondition 'valid_src' got status valid.
 [eva] string_h.c:169: 
   function mempcpy: precondition 'separation' got status valid.
-[eva] FRAMAC_SHARE/libc/string.h:114: 
+[eva] FRAMAC_SHARE/libc/string.h:132: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
 [kernel] string_h.c:169: Warning: using size of 'void'
 [eva] Done for function mempcpy
 [eva:alarm] string_h.c:170: Warning: assertion 'imprecise' got status unknown.
+[eva] string_h.c:172: Call to builtin strlen
+[eva] string_h.c:172: 
+  function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function memrchr <- main.
+  Called from string_h.c:172.
+[eva] using specification for function memrchr
+[eva] string_h.c:172: function memrchr: precondition 'valid' got status valid.
+[eva] string_h.c:172: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_h.c:172: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:100: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+[eva] FRAMAC_SHARE/libc/string.h:104: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+[kernel] string_h.c:172: Warning: using size of 'void'
+[eva] Done for function memrchr
+[eva:alarm] string_h.c:173: Warning: check got status unknown.
+[eva] string_h.c:174: Call to builtin strlen
+[eva] string_h.c:174: 
+  function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function memrchr <- main.
+  Called from string_h.c:174.
+[eva] string_h.c:174: function memrchr: precondition 'valid' got status valid.
+[eva] string_h.c:174: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_h.c:174: 
+  function memrchr: precondition 'danglingness' got status valid.
+[kernel] string_h.c:174: Warning: using size of 'void'
+[eva] Done for function memrchr
+[eva:alarm] string_h.c:175: Warning: check got status unknown.
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -449,4 +480,5 @@
   pdest[0..8] ∈ [--..--] or UNINITIALIZED
        [9] ∈ UNINITIALIZED
   pend ∈ {{ &pdest[9] }}
+  rchr ∈ {{ NULL ; "haystack" + [--..--] }}
   __retres ∈ {0}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 84e8f2469560ba477d4d8884ff86c68ccf8283ff..d51e38c9c28fa26aa147cecf4a7ce431c104054d 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -168,5 +168,11 @@ int main(int argc, char **argv)
   char pdest[10];
   char *pend = mempcpy(pdest, "gnu-only function", 9);
   //@ assert imprecise: pend == pdest + 9 && *pend == '\0';
+
+  char *rchr = memrchr(c, 'a', strlen(c));
+  //@ check imprecise: rchr == c + strlen("haysta");
+  rchr = memrchr(c, 'n', strlen(c));
+  //@ check imprecise: rchr == \null;
+
   return 0;
 }