Skip to content
Snippets Groups Projects
Commit fb19ba7d authored by Andre Maroneze's avatar Andre Maroneze Committed by Virgile Prevosto
Browse files

[tests] update oracles related to frama-c/frama-c!2836

parent 1b29ccd5
No related branches found
No related tags found
No related merge requests found
......@@ -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;
......
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