diff --git a/share/libc/strings.h b/share/libc/strings.h
index f1091001fc4b1bf80ad01cf123ceba53cda6431e..6b6e42dd4a04bc6f7e626dc1acf7a4995a2acc53 100644
--- a/share/libc/strings.h
+++ b/share/libc/strings.h
@@ -35,6 +35,7 @@ extern void   bcopy(const void *, void *, size_t);
 
 /*@ requires valid_memory_area: \valid (((char*) s)+(0 .. n-1));
   assigns ((char*) s)[0 .. n-1] \from \nothing;
+  ensures s_initialized:initialization:\initialized(((char*) s)+(0 .. n-1));
   ensures zero_initialized: \subset(((char*) s)[0 .. n-1], {0}); */
 extern void   bzero(void *s, size_t n);
 extern int    ffs(int);
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 286bbe329a045436cc10b60d93aa8aa30853ca7f..056a7d23f9316f95d9dada935a0a42ab3796252d 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1690,6 +1690,8 @@
 --- Properties of Function 'bzero'
 --------------------------------------------------------------------------------
 
+[ Extern  ] Post-condition 's_initialized,initialization'
+            Unverifiable but considered Valid.
 [ Extern  ] Post-condition 'zero_initialized'
             Unverifiable but considered Valid.
 [ Extern  ] Assigns (file share/libc/strings.h, line 37)
@@ -1705,7 +1707,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/strings.h, line 47)
+[ Extern  ] Froms (file share/libc/strings.h, line 48)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -1716,7 +1718,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/strings.h, line 54)
+[ Extern  ] Froms (file share/libc/strings.h, line 55)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -2133,8 +2135,8 @@
 --- Status Report Summary
 --------------------------------------------------------------------------------
    156 Completely validated
-   215 Considered valid
+   216 Considered valid
     29 To be validated
      4 Alarms emitted
-   404 Total
+   405 Total
 --------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 388b254dc2a9885eae3ae4b6709ec8d78e129fab..22d7faf5fa0a2634869377cc070cda4f06758896 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4041,6 +4041,9 @@ char *strdup(char const *s);
 char *strndup(char const *s, size_t n);
 
 /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1));
+    ensures
+      s_initialized: initialization:
+        \initialized((char *)\old(s) + (0 .. \old(n) - 1));
     ensures
       zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0});
     assigns *((char *)s + (0 .. n - 1));
diff --git a/tests/libc/oracle/strings_h.res.oracle b/tests/libc/oracle/strings_h.res.oracle
index d675e204e1f114ab718cf914d67dda5be9c77ef5..5545c5be19e053286fcb4acc33a16cad2d023eef 100644
--- a/tests/libc/oracle/strings_h.res.oracle
+++ b/tests/libc/oracle/strings_h.res.oracle
@@ -55,6 +55,13 @@
 [eva] tests/libc/strings_h.c:15: 
   function strncasecmp: precondition 'valid_string_s2' got status valid.
 [eva] Done for function strncasecmp
+[eva] computing for function bzero <- main.
+  Called from tests/libc/strings_h.c:18.
+[eva] using specification for function bzero
+[eva] tests/libc/strings_h.c:18: 
+  function bzero: precondition 'valid_memory_area' got status valid.
+[eva] Done for function bzero
+[eva] tests/libc/strings_h.c:19: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -70,3 +77,4 @@
   r3 ∈ [--..--]
   r4 ∈ [--..--]
   r5 ∈ [--..--]
+  s4[0..9] ∈ {0}
diff --git a/tests/libc/strings_h.c b/tests/libc/strings_h.c
index a1af1541ec7eae739b614e1f8cb309af73632c7b..587b961e6ef5517cf3ec3b2fd254d10c6e9dd243 100644
--- a/tests/libc/strings_h.c
+++ b/tests/libc/strings_h.c
@@ -13,4 +13,8 @@ void main() {
   int r4 = strncasecmp(s1, s, 3);
   if (nondet) strncasecmp(s1, s, 4);
   int r5 = strncasecmp(s1, s2, 0);
+
+  char s4[10];
+  bzero(s4, 10);
+  //@ assert s4[9] == s4[8] == 0;
 }