[libc] refine spec of strftime

share/libc/time.h

@@ -159,9 +159,8 @@ extern struct tm *localtime(const time_t *timer);
   assigns s[0 .. max-1] \from indirect:max, indirect:format[0..], indirect:*tm;
   assigns \result \from indirect:max, indirect:format[0..], indirect:*tm;
   ensures result_bounded: \result < max;
-  ensures result_valid_string: valid_string(s);
-  ensures result_length: s[\result] == 0;
-  ensures max: s[max-1] == 0;
+  ensures result_valid_string: \result > 0 ==> valid_string(s);
+  ensures result_length: \result > 0 ==> s[\result] == 0;
  */
 extern size_t strftime(char * restrict s,
                        size_t max,

tests/libc/oracle/fc_libc.1.res.oracle

@@ -5116,9 +5116,8 @@ extern struct tm *localtime(time_t const *timer);
     requires valid_format: valid_read_string(format);
     requires valid_tm: \valid_read(tm);
     ensures result_bounded: \result < \old(max);
-    ensures result_valid_string: valid_string(\old(s));
-    ensures result_length: *(\old(s) + \result) ≡ 0;
-    ensures max: *(\old(s) + (\old(max) - 1)) ≡ 0;
+    ensures result_valid_string: \result > 0 ⇒ valid_string(\old(s));
+    ensures result_length: \result > 0 ⇒ *(\old(s) + \result) ≡ 0;
     assigns *(s + (0 .. max - 1)), \result;
     assigns *(s + (0 .. max - 1))
       \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);