From 4877f89c46c35ba84fc6163330f7d53251889243 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 8 Feb 2022 19:28:08 +0100
Subject: [PATCH] [libc] refine spec of strftime
---
share/libc/time.h | 5 ++---
tests/libc/oracle/fc_libc.1.res.oracle | 5 ++---
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/share/libc/time.h b/share/libc/time.h
index bfc3f053de3..a0958995d76 100644
--- a/share/libc/time.h
+++ b/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,
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 9ef75177e38..9e2fa656c31 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/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);
--
GitLab