diff --git a/share/libc/string.h b/share/libc/string.h
index 566b296162caca8aebbd4466043550e300659bab..6f265a44d012653bdfd2dfbf0b4e6405e3e81331 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -457,7 +457,8 @@ extern size_t strxfrm (char *restrict dest,
 
 // Allocate strings
 
-/*@ allocates \result;
+/*@ requires valid_string_s: valid_read_string(s);
+  @ allocates \result;
   @ assigns \result \from indirect:s[0..strlen(s)], indirect:__fc_heap_status;
   @ behavior allocation:
   @   assumes can_allocate: is_allocable(strlen(s));
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index fffd2495d1d6ab651db22788f76adb4ca2104a70..630d2219ba4794e3763ba8e70b88cedb13ad48b3 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1691,19 +1691,19 @@
             Unverifiable but considered Valid.
 [ Extern  ] Post-condition for 'no_allocation' 'result_null'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'allocation' (file share/libc/string.h, line 464)
+[ Extern  ] Assigns for 'allocation' (file share/libc/string.h, line 465)
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'no_allocation' nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'allocation' (file share/libc/string.h, line 464)
-            Unverifiable but considered Valid.
 [ Extern  ] Froms for 'allocation' (file share/libc/string.h, line 465)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/string.h, line 461)
+[ Extern  ] Froms for 'allocation' (file share/libc/string.h, line 466)
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/string.h, line 462)
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'no_allocation' (file share/libc/string.h, line 471)
+[ Extern  ] Froms for 'no_allocation' (file share/libc/string.h, line 472)
             Unverifiable but considered Valid.
 [  Valid  ] Behavior 'allocation'
             by Frama-C kernel.
@@ -1711,7 +1711,7 @@
             by Frama-C kernel.
 [  Valid  ] Behavior 'no_allocation'
             by Frama-C kernel.
-[ Extern  ] Frees/Allocates nothing/(file share/libc/string.h, line 460) 
+[ Extern  ] Frees/Allocates nothing/(file share/libc/string.h, line 461) 
             Unverifiable but considered Valid.
 [ Extern  ] Frees/Allocates for 'no_allocation' nothing/nothing 
             Unverifiable but considered Valid.
@@ -1726,19 +1726,19 @@
             Unverifiable but considered Valid.
 [ Extern  ] Post-condition for 'no_allocation' 'result_null'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'allocation' (file share/libc/string.h, line 482)
+[ Extern  ] Assigns for 'allocation' (file share/libc/string.h, line 483)
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'no_allocation' nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'allocation' (file share/libc/string.h, line 482)
-            Unverifiable but considered Valid.
 [ Extern  ] Froms for 'allocation' (file share/libc/string.h, line 483)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/string.h, line 478)
+[ Extern  ] Froms for 'allocation' (file share/libc/string.h, line 484)
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/string.h, line 479)
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'no_allocation' (file share/libc/string.h, line 492)
+[ Extern  ] Froms for 'no_allocation' (file share/libc/string.h, line 493)
             Unverifiable but considered Valid.
 [  Valid  ] Behavior 'allocation'
             by Frama-C kernel.
@@ -1746,7 +1746,7 @@
             by Frama-C kernel.
 [  Valid  ] Behavior 'no_allocation'
             by Frama-C kernel.
-[ Extern  ] Frees/Allocates nothing/(file share/libc/string.h, line 477) 
+[ Extern  ] Frees/Allocates nothing/(file share/libc/string.h, line 478) 
             Unverifiable but considered Valid.
 [ Extern  ] Frees/Allocates for 'no_allocation' nothing/nothing 
             Unverifiable but considered Valid.
@@ -1763,7 +1763,7 @@
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/string.h, line 508)
+[ Extern  ] Froms (file share/libc/string.h, line 509)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 975738524955a48580234e00fc2ff1533bcafb21..062a50bfd139232b9eb40071fd09447bdb2a61a9 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5557,7 +5557,8 @@ char *strerror(int errnum)
   return __retres;
 }
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))),
             (indirect: __fc_heap_status);
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 66a8414bd903b0993bdbd8dba5989da6b0294e31..75780c1ba4a10561b67f6deb39440fddbcfbf8cb 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -247,6 +247,8 @@
   The specification of function 'strdup' is currently not supported by Eva.
   Consider adding ./share/libc/string.c to the analyzed source files.
 [eva] tests/libc/string_h.c:119: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/string_h.c:119: 
+  function strdup: precondition 'valid_string_s' got status valid.
 [eva] Done for function strdup
 [eva] computing for function strndup <- main.
   Called from tests/libc/string_h.c:120.