Skip to content
Snippets Groups Projects
Commit 42b1074a authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] update oracle against change in Frama-C's libc

parent 4548fd43
No related branches found
No related tags found
No related merge requests found
......@@ -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:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment