Skip to content
Snippets Groups Projects
Commit 1b1693fc authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'fix/libc/no-addr-array' into 'master'

[libc] fixes bug in time.h (taking address of array instead of first elt)

See merge request frama-c/frama-c!2138
parents ae3347dc 10d01115
No related branches found
No related tags found
No related merge requests found
...@@ -105,7 +105,7 @@ extern time_t mktime(struct tm *timeptr); ...@@ -105,7 +105,7 @@ extern time_t mktime(struct tm *timeptr);
extern time_t time(time_t *timer); extern time_t time(time_t *timer);
char __fc_ctime[26]; char __fc_ctime[26];
char * const __fc_p_ctime = &__fc_ctime; char * const __fc_p_ctime = __fc_ctime;
extern char *asctime(const struct tm *timeptr); extern char *asctime(const struct tm *timeptr);
......
...@@ -5166,7 +5166,7 @@ extern time_t mktime(struct tm *timeptr); ...@@ -5166,7 +5166,7 @@ extern time_t mktime(struct tm *timeptr);
extern time_t time(time_t *timer); extern time_t time(time_t *timer);
char __fc_ctime[26]; char __fc_ctime[26];
char * const __fc_p_ctime = (char *)(& __fc_ctime); char * const __fc_p_ctime = __fc_ctime;
/*@ requires valid_timer: \valid_read(timer); /*@ requires valid_timer: \valid_read(timer);
requires initialization: init_timer: \initialized(timer); requires initialization: init_timer: \initialized(timer);
ensures result_points_to_ctime: \result ≡ __fc_p_ctime; 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