diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index e9f59a74ee0e97911167a3e9e9a36fdab8a88d0d..22f01d33bcbc41b5f582bc656c644ae690c1766d 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -1149,7 +1149,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -1173,6 +1174,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 834f4bcf8a79c2e6d52f102aaf2f9e2142e5c0c9..8abe1c09911ce688e26892493a5a685c3a956c3b 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -878,7 +878,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -902,6 +903,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index a28010d7e27effbda991b8f2c095611f7242d2a8..8b5a0ab04c6a5d659f56680f94d76c4c127c7a77 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -881,7 +881,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -905,6 +906,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index d44adcdeb8760e12577b77f48f021a5f2da4d8dc..f02c0bd03c4b796656a145f02225a68a0bad2460 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -878,7 +878,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -902,6 +903,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index e979a9ec076c5182da39013b9e638b269e0aa032..f1e95a07590b74b4708ff4e257b1255dbef49da4 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -859,7 +859,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -883,6 +884,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index b3e59ee2b9729d1cd4d1f358df3f382c961ffae5..0e7e54f8d710f5ae1d26272488fba474a2d60fff 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -860,7 +860,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -884,6 +885,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_system_error.err.oracle b/tests/stl/oracle/stl_system_error.err.oracle
index 9712de6c53dd066847788a0481c40a1c6e9681f1..d8af1fa6cec602697f8e4d46fac4b82aea189b0c 100644
--- a/tests/stl/oracle/stl_system_error.err.oracle
+++ b/tests/stl/oracle/stl_system_error.err.oracle
@@ -1,4 +1,4 @@
-FRAMAC_SHARE/libc/signal.h:223:28: Expecting ';' after requires clause
+FRAMAC_SHARE/libc/signal.h:227:28: Expecting ';' after requires clause
 FRAMAC_SHARE/libc/wchar.h:55:5: No suitable candidate found for function valid_read_or_empty.
 FRAMAC_SHARE/libc/wchar.h:69:74: No suitable candidate found for function valid_read_or_empty.
 FRAMAC_SHARE/libc/wchar.h:80:73: No suitable candidate found for function valid_or_empty.
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index b2169e75f552185ed7999a4793d0fba91cfb80c5..94668511d81445cf260807140ddf0ad6b439ad73 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -734,7 +734,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -758,6 +759,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index a5b1a5d1c657001d913339045c5d73dfda0f3023..1b39f2c24e97433eb4c33a2a82c92112c405c6b5 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -569,7 +569,8 @@ int strcoll(char const *s1, char const *s2);
 
 /*@ 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) ≢ (0 ≢ 0);
@@ -593,6 +594,15 @@ 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);
+ */
+char *strchrnul(char const *s, int c);
+
 /*@ requires valid_string_s: valid_read_string(s);
     assigns \result;
     assigns \result \from s, *(s + (0 ..)), c;