From fb19ba7d6c093a0b10fb2f3ef1e93cc85667324c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 17 Sep 2020 15:06:30 +0200
Subject: [PATCH] [tests] update oracles related to frama-c/frama-c!2836

---
 tests/stl/oracle/stl_system_error.res.oracle | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index c5d8f826..ed910e4f 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -1735,6 +1735,18 @@ time_t time(time_t *timer);
 
 char __fc_ctime[26];
 char * const __fc_p_ctime = __fc_ctime;
+/*@ requires valid_timeptr: \valid_read(timeptr);
+    requires init_timeptr: initialization: \initialized(timeptr);
+    ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
+    ensures result_valid_string: valid_read_string(__fc_p_ctime);
+    assigns __fc_ctime[0 .. 25], \result;
+    assigns __fc_ctime[0 .. 25]
+      \from (indirect: *timeptr), (indirect: __fc_time);
+    assigns \result
+      \from (indirect: *timeptr), (indirect: __fc_time), __fc_p_ctime;
+ */
+char *asctime(struct tm const *timeptr);
+
 /*@ requires valid_timer: \valid_read(timer);
     requires init_timer: initialization: \initialized(timer);
     ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
-- 
GitLab