[Libc] add requires to strdup

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

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.

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

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.