From 42b1074a68f8380e7ea95026be8e23c1398dc14f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 4 Aug 2020 11:08:13 +0200
Subject: [PATCH] [tests] update oracle against change in Frama-C's libc
---
tests/stl/oracle/stl_system_error.res.oracle | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 94668511..c5d8f826 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -1913,6 +1913,17 @@ axiomatic nanosleep_predicates {
int clock_nanosleep(clockid_t clock_id, int flags,
struct timespec const *rqtp, struct timespec *rmtp);
+/*@ requires valid_timer: \valid_read(timer);
+ requires valid_result: \valid(result);
+ ensures
+ result_null_or_result: \result ≡ \old(result) ∨ \result ≡ \null;
+ assigns \result, *result;
+ assigns \result \from (indirect: *timer), result;
+ assigns *result \from (indirect: *timer);
+ */
+struct tm *gmtime_r(time_t const * __restrict timer,
+ struct tm * __restrict result);
+
/*@ requires valid_request: \valid_read(rqtp);
requires
initialized_request: initialization:
--
GitLab