diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index cb5f7f538a9213bbca5092d962708c6c5f72fd3c..84131d8aab4d130b7889900b63bc75ec0b9bc8eb 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -316,7 +316,14 @@ extern int pthread_mutex_trylock(pthread_mutex_t *);
   ensures success_or_error: \result == 0 || \result == EPERM;
 */
 extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
-extern int pthread_mutexattr_destroy(pthread_mutexattr_t *);
+
+/*@
+  requires valid_attr: \valid(attr);
+  assigns \result, *attr \from \nothing;
+  ensures success: \result == 0;
+ */
+extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);
+
 extern int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *restrict,
                                             int *restrict);
 extern int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *restrict,
@@ -327,12 +334,26 @@ extern int pthread_mutexattr_getrobust(const pthread_mutexattr_t *restrict,
                                        int *restrict);
 extern int pthread_mutexattr_gettype(const pthread_mutexattr_t *restrict,
                                      int *restrict);
-extern int pthread_mutexattr_init(pthread_mutexattr_t *);
+
+/*@
+  requires valid_attr: \valid(attr);
+  assigns \result, *attr \from \nothing;
+  ensures success_or_error: \result == 0 || \result == ENOMEM;
+ */
+extern int pthread_mutexattr_init(pthread_mutexattr_t *attr);
+
 extern int pthread_mutexattr_setprioceiling(pthread_mutexattr_t *, int);
 extern int pthread_mutexattr_setprotocol(pthread_mutexattr_t *, int);
 extern int pthread_mutexattr_setpshared(pthread_mutexattr_t *, int);
 extern int pthread_mutexattr_setrobust(pthread_mutexattr_t *, int);
-extern int pthread_mutexattr_settype(pthread_mutexattr_t *, int);
+
+/*@
+  requires valid_attr: \valid(attr);
+  assigns \result, *attr \from indirect:type;
+  ensures success_or_error: \result == 0 || \result == EINVAL;
+ */
+extern int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type);
+
 extern int pthread_once(pthread_once_t *, void (*)(void));
 extern int pthread_rwlock_destroy(pthread_rwlock_t *);
 extern int pthread_rwlock_init(pthread_rwlock_t *restrict,
diff --git a/share/libc/sys/ioctl.h b/share/libc/sys/ioctl.h
index b9d5f00202a975829f706745e185bdd26dbe4de0..91453478272e1eb297ad7982588723bec1dd14c8 100644
--- a/share/libc/sys/ioctl.h
+++ b/share/libc/sys/ioctl.h
@@ -116,5 +116,9 @@
 #define SIOCPROTOPRIVATE 0x89E0 /* to 89EF */
 
 
+// Some definitions from ioctls.h
+
+#define FIONREAD 0x541B
+
 
 #endif
diff --git a/share/libc/time.h b/share/libc/time.h
index 741476f6f125ca319c21010d627ab0ebaa925a61..b44aafbe4c1cddc1ab494816d33458e3a9c36f1c 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -258,8 +258,18 @@ extern int clock_nanosleep(clockid_t clock_id, int flags,
 extern int clock_settime(clockid_t, const struct timespec *);
 extern char *ctime_r(const time_t *timep, char *buf);
 extern struct tm *getdate(const char *string);
+
+/*@
+  requires valid_timer: \valid_read(timer);
+  requires valid_result: \valid(result);
+  assigns \result \from indirect:*timer, result;
+  assigns *result \from indirect:*timer;
+  ensures result_null_or_result:
+    \result == result || \result == \null;
+*/
 extern struct tm *gmtime_r(const time_t *restrict timer,
                            struct tm *restrict result);
+
 extern struct tm *localtime_r(const time_t *restrict timep,
                               struct tm *restrict result);
 
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e3ca27e4863a5c853bf6c387842e38e4363e8e51..8ab5e9661ecca1d0174745e86ae07b5cc0421de0 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
    unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
    wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call); 
   
-  Undefined functions (407)
+  Undefined functions (411)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -105,64 +105,65 @@
    getpwnam (0 call); getpwuid (0 call); getresgid (0 call);
    getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
    getsid (0 call); getsockname (0 call); getsockopt (0 call);
-   gettimeofday (0 call); getuid (0 call); gmtime (0 call); htonl (0 call);
-   htons (0 call); iconv (0 call); iconv_close (0 call); iconv_open (0 call);
-   inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
-   inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
-   kill (0 call); killpg (0 call); labs (0 call); lcong48 (0 call);
-   ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
-   localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
-   log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
-   logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
-   lseek (0 call); lstat (0 call); makedev (0 call); malloc (7 calls);
-   mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
-   mkfifo (0 call); mknod (0 call); mkstemp (0 call); mktime (0 call);
-   mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
-   nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
-   open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
-   pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
-   poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+   gettimeofday (0 call); getuid (0 call); gmtime (0 call); gmtime_r (0 call);
+   htonl (0 call); htons (0 call); iconv (0 call); iconv_close (0 call);
+   iconv_open (0 call); inet_addr (2 calls); inet_ntoa (0 call);
+   inet_ntop (0 call); inet_pton (0 call); isascii (0 call); isatty (0 call);
+   jrand48 (0 call); kill (0 call); killpg (0 call); labs (0 call);
+   lcong48 (0 call); ldiv (0 call); listen (0 call); llabs (0 call);
+   lldiv (0 call); localtime (0 call); log (0 call); log10 (0 call);
+   log10f (0 call); log10l (0 call); log2 (0 call); log2f (0 call);
+   log2l (0 call); logf (0 call); logl (0 call); longjmp (0 call);
+   lrand48 (0 call); lseek (0 call); lstat (0 call); makedev (0 call);
+   malloc (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+   mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
+   mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
+   nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
+   ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
+   openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
+   pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
    pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
    pthread_cond_init (0 call); pthread_cond_wait (0 call);
    pthread_create (0 call); pthread_join (0 call);
    pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
-   pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
-   putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
-   puts (0 call); qsort (0 call); quick_exit (0 call); raise (0 call);
-   rand (0 call); random (0 call); read (0 call); readdir (0 call);
-   readv (0 call); realloc (3 calls); recv (0 call); recvmsg (0 call);
-   remove (0 call); rename (0 call); rewind (0 call); round (0 call);
-   roundf (0 call); roundl (0 call); seed48 (0 call); select (0 call);
-   send (0 call); setbuf (0 call); setegid (0 call); seteuid (0 call);
-   setgid (0 call); sethostname (0 call); setitimer (0 call); setjmp (0 call);
-   setlogmask (0 call); setpgid (0 call); setpriority (0 call);
-   setregid (0 call); setresgid (0 call); setresuid (0 call);
-   setreuid (0 call); setrlimit (0 call); setsid (0 call); setsockopt (0 call);
-   settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
-   sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
-   sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
-   siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
-   sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
-   sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
-   srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
-   strcasestr (0 call); strchrnul (0 call); strcoll (0 call); strcspn (0 call);
-   strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
-   strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
-   strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
-   strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
-   strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
-   syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
-   tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
-   tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
-   ttyname (0 call); tzset (0 call); umask (0 call); uname (0 call);
-   ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
-   vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
-   vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
-   waitpid (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
-   wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
-   wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
-   wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
-   write (0 call); 
+   pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call);
+   pthread_mutexattr_destroy (0 call); pthread_mutexattr_init (0 call);
+   pthread_mutexattr_settype (0 call); putc (0 call); putc_unlocked (0 call);
+   putchar (0 call); putchar_unlocked (0 call); puts (0 call); qsort (0 call);
+   quick_exit (0 call); raise (0 call); rand (0 call); random (0 call);
+   read (0 call); readdir (0 call); readv (0 call); realloc (3 calls);
+   recv (0 call); recvmsg (0 call); remove (0 call); rename (0 call);
+   rewind (0 call); round (0 call); roundf (0 call); roundl (0 call);
+   seed48 (0 call); select (0 call); send (0 call); setbuf (0 call);
+   setegid (0 call); seteuid (0 call); setgid (0 call); sethostname (0 call);
+   setitimer (0 call); setjmp (0 call); setlogmask (0 call); setpgid (0 call);
+   setpriority (0 call); setregid (0 call); setresgid (0 call);
+   setresuid (0 call); setreuid (0 call); setrlimit (0 call); setsid (0 call);
+   setsockopt (0 call); settimeofday (0 call); setuid (0 call);
+   setvbuf (0 call); shutdown (0 call); sigaction (0 call); sigaddset (0 call);
+   sigdelset (0 call); sigemptyset (0 call); sigfillset (0 call);
+   sigismember (0 call); siglongjmp (0 call); signal (0 call);
+   sigprocmask (0 call); sin (0 call); sinf (0 call); sinl (0 call);
+   socket (0 call); socketpair (0 call); sqrt (0 call); sqrtf (0 call);
+   sqrtl (0 call); srand (0 call); srand48 (0 call); srandom (0 call);
+   stat (0 call); stpcpy (0 call); strcasestr (0 call); strchrnul (0 call);
+   strcoll (0 call); strcspn (0 call); strftime (0 call); strlcat (0 call);
+   strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call); strsep (0 call);
+   strspn (0 call); strtod (0 call); strtof (0 call); strtoimax (0 call);
+   strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
+   strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
+   sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
+   tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
+   times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
+   truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
+   umask (0 call); uname (0 call); ungetc (0 call); unlink (0 call);
+   usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
+   vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
+   vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
+   wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+   wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+   wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+   wmemcmp (0 call); wmemmove (0 call); write (0 call); 
   
   'Extern' global variables (16)
   ==============================
@@ -185,7 +186,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 489
+  Function = 493
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 70a3baea5cd3d9cb5d0a3884f8a27b5b2437c965..29a563fb2eb5ca45b840bb5c4c7bfa51574fd7ed 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6402,6 +6402,17 @@ axiomatic nanosleep_predicates {
 extern 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);
+ */
+extern struct tm *gmtime_r(time_t const * __restrict timer,
+                           struct tm * __restrict result);
+
 /*@ requires valid_request: \valid_read(rqtp);
     requires
       initialization: initialized_request:
@@ -7777,6 +7788,30 @@ extern int pthread_mutex_lock(pthread_mutex_t *mutex);
  */
 extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
+/*@ requires valid_attr: \valid(attr);
+    ensures success: \result ≡ 0;
+    assigns \result, *attr;
+    assigns \result \from \nothing;
+    assigns *attr \from \nothing;
+ */
+extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);
+
+/*@ requires valid_attr: \valid(attr);
+    ensures success_or_error: \result ≡ 0 ∨ \result ≡ 12;
+    assigns \result, *attr;
+    assigns \result \from \nothing;
+    assigns *attr \from \nothing;
+ */
+extern int pthread_mutexattr_init(pthread_mutexattr_t *attr);
+
+/*@ requires valid_attr: \valid(attr);
+    ensures success_or_error: \result ≡ 0 ∨ \result ≡ 22;
+    assigns \result, *attr;
+    assigns \result \from (indirect: type);
+    assigns *attr \from (indirect: type);
+ */
+extern int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type);
+
 extern char __fc_getpwuid_pw_name[64];
 
 extern char __fc_getpwuid_pw_passwd[64];
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index 7e8f729d1beae0a1300355d51b3f1c84f7826b6c..8262e54c5d111ef4e74fc10fcda75398e437ee47 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -118,11 +118,121 @@
   Called from tests/libc/time_h.c:43.
 [eva] Done for function ctime
 [eva:alarm] tests/libc/time_h.c:44: Warning: assertion got status unknown.
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:48.
+[eva] using specification for function Frama_C_interval
+[eva] tests/libc/time_h.c:48: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:48.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:49.
+[eva] tests/libc/time_h.c:49: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:49.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:50.
+[eva] tests/libc/time_h.c:50: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:50.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:51.
+[eva] tests/libc/time_h.c:51: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:51.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:52.
+[eva] tests/libc/time_h.c:52: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:52.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:53.
+[eva] tests/libc/time_h.c:53: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:53.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:54.
+[eva] tests/libc/time_h.c:54: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:54.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:55.
+[eva] tests/libc/time_h.c:55: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:55.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:56.
+[eva] tests/libc/time_h.c:56: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/libc/time_h.c:56.
+[eva] Done for function Frama_C_interval
+[eva] computing for function mktime <- main.
+  Called from tests/libc/time_h.c:58.
+[eva] using specification for function mktime
+[eva] tests/libc/time_h.c:58: 
+  function mktime: precondition 'valid_timeptr' got status valid.
+[eva] Done for function mktime
+[eva] computing for function mktime <- main.
+  Called from tests/libc/time_h.c:58.
+[eva] Done for function mktime
+[eva] computing for function gmtime <- main.
+  Called from tests/libc/time_h.c:60.
+[eva] using specification for function gmtime
+[eva] tests/libc/time_h.c:60: 
+  function gmtime: precondition 'valid_timer' got status valid.
+[eva] Done for function gmtime
+[eva] computing for function gmtime <- main.
+  Called from tests/libc/time_h.c:60.
+[eva] Done for function gmtime
+[eva] computing for function gmtime_r <- main.
+  Called from tests/libc/time_h.c:62.
+[eva] using specification for function gmtime_r
+[eva] tests/libc/time_h.c:62: 
+  function gmtime_r: precondition 'valid_timer' got status valid.
+[eva] tests/libc/time_h.c:62: 
+  function gmtime_r: precondition 'valid_result' got status valid.
+[eva] Done for function gmtime_r
+[eva] computing for function gmtime_r <- main.
+  Called from tests/libc/time_h.c:62.
+[eva] Done for function gmtime_r
+[eva] computing for function gmtime_r <- main.
+  Called from tests/libc/time_h.c:62.
+[eva] Done for function gmtime_r
+[eva] computing for function gmtime_r <- main.
+  Called from tests/libc/time_h.c:62.
+[eva] Done for function gmtime_r
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   __fc_ctime[0..25] ∈ [--..--]
+  __fc_time_tm ∈ [--..--]
+  Frama_C_entropy_source ∈ [--..--]
   req.tv_sec ∈ [--..--]
      .tv_nsec ∈ [0..999999999]
   rem ∈ [--..--] or UNINITIALIZED
@@ -131,4 +241,8 @@
       .tv_nsec ∈ [0..999999999] or UNINITIALIZED
   tt ∈ {42}
   time_str ∈ {{ &__fc_ctime[0] }}
+  mytime ∈ [--..--]
+  t ∈ [--..--]
+  res_time ∈ {{ NULL ; &mytime2 }} or UNINITIALIZED
+  mytime2 ∈ [--..--] or UNINITIALIZED
   __retres ∈ {0; 1; 2}
diff --git a/tests/libc/time_h.c b/tests/libc/time_h.c
index 0ce0180a8c7a2892d0da7f2dafafa7c3fd04bc8b..c56c8ef3b96cdefead7c20068c10df481f78ba28 100644
--- a/tests/libc/time_h.c
+++ b/tests/libc/time_h.c
@@ -3,7 +3,7 @@
  */
 
 #include <time.h>
-
+#include "__fc_builtin.h"
 
 
 int main() {
@@ -42,5 +42,24 @@ int main() {
   time_t tt = 42;
   char *time_str = ctime(&tt);
   //@ assert valid_string(time_str);
+
+  struct tm mytime =
+    {
+     .tm_sec = Frama_C_interval(0,60), // 60: for leap seconds
+     .tm_min = Frama_C_interval(0,59),
+     .tm_hour = Frama_C_interval(0,23),
+     .tm_mday = Frama_C_interval(1,31),
+     .tm_mon = Frama_C_interval(0,11),
+     .tm_year = Frama_C_interval(0,177), // arbitrary value
+     .tm_wday = Frama_C_interval(0,6),
+     .tm_yday = Frama_C_interval(0,365),
+     .tm_isdst = Frama_C_interval(0,1)
+    };
+  time_t t = mktime(&mytime);
+  struct tm *res_time;
+  res_time = gmtime(&t);
+  struct tm mytime2;
+  res_time = gmtime_r(&t, &mytime2);
+
   return 0;
 }