diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d5a4550ba8159849c07a08e303f297b9fe1a6c20..23e24fa4d73ef6939753a9a7177bc6a8b73f3708 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -207,6 +207,7 @@ share/libc/__fc_define_suseconds_t.h: CEA_LGPL
share/libc/__fc_define_time_t.h: CEA_LGPL
share/libc/__fc_define_timer_t.h: CEA_LGPL
share/libc/__fc_define_timespec.h: CEA_LGPL
+share/libc/__fc_define_timeval.h: CEA_LGPL
share/libc/__fc_define_uid_and_gid.h: CEA_LGPL
share/libc/__fc_define_useconds_t.h: CEA_LGPL
share/libc/__fc_define_wchar_t.h: CEA_LGPL
diff --git a/share/libc/__fc_define_timeval.h b/share/libc/__fc_define_timeval.h
new file mode 100644
index 0000000000000000000000000000000000000000..34db8894a582b2e7a28779182505194efadaed79
--- /dev/null
+++ b/share/libc/__fc_define_timeval.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_TIMEVAL
+#define __FC_DEFINE_TIMEVAL
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+#include "__fc_define_suseconds_t.h"
+#include "__fc_define_time_t.h"
+struct timeval {
+ time_t tv_sec;
+ suseconds_t tv_usec;
+};
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/__fc_select.h b/share/libc/__fc_select.h
index 4fc0f3b0aa6e161a24d6daefa686adb5e5223392..1fad5956e876ce077f8db6bfccda7db5ddd8c7d4 100644
--- a/share/libc/__fc_select.h
+++ b/share/libc/__fc_select.h
@@ -24,13 +24,11 @@
#define __FC_SELECT__
#include "features.h"
__PUSH_FC_STDLIB
-#include "__fc_define_time_t.h"
-#include "__fc_define_suseconds_t.h"
#include "__fc_define_fd_set_t.h"
#include "__fc_define_sigset_t.h"
-
-#include "sys/time.h"
-
+#include "__fc_define_suseconds_t.h"
+#include "__fc_define_timeval.h"
+#include "__fc_define_timespec.h"
__BEGIN_DECLS
/* assigns \result \from nfds, *readfds, *writefds,*errorfds,*timeout,*sigmask;
diff --git a/share/libc/getopt.h b/share/libc/getopt.h
index ed3f45384b71e51ed761a1e0d67c7f38462eb608..380abc7f5aba56b890fa82bd197dbce6e5acead3 100644
--- a/share/libc/getopt.h
+++ b/share/libc/getopt.h
@@ -24,10 +24,9 @@
#define __FC_GETOPT_H
#include "features.h"
__PUSH_FC_STDLIB
-
+#include "unistd.h"
__BEGIN_DECLS
-#include "unistd.h"
/* GNU specific */
struct option
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index fbd3da31927d47879bb7ef0c81bf878ba4b5fbc7..db0a5b17b0b5ce5a9eaac4e983ac9bdd0eb45abd 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -24,17 +24,12 @@
#define __FC_SYS_TIME_H__
#include "../features.h"
__PUSH_FC_STDLIB
-__BEGIN_DECLS
-
-#include "../__fc_define_time_t.h"
-#include "../__fc_define_suseconds_t.h"
#include "../__fc_define_fd_set_t.h"
-#include "../__fc_define_timespec.h"
+#include "../__fc_define_suseconds_t.h"
+#include "../__fc_define_time_t.h"
+#include "../__fc_define_timeval.h"
#include "../__fc_string_axiomatic.h"
-struct timeval {
- time_t tv_sec;
- suseconds_t tv_usec;
-};
+__BEGIN_DECLS
struct timezone {
int tz_minuteswest;
diff --git a/share/libc/time.h b/share/libc/time.h
index d156b59c620e759c9709a9b8da294049b57e0476..fe6304ce88d58490ddb41494e6608c6ffed332b0 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -24,14 +24,16 @@
#define __FC_TIME_H
#include "features.h"
__PUSH_FC_STDLIB
+#include "__fc_define_clockid_t.h"
#include "__fc_define_null.h"
#include "__fc_define_size_t.h"
-#include "__fc_define_clockid_t.h"
+#include "__fc_define_time_t.h"
#include "__fc_define_timer_t.h"
+#include "__fc_define_timespec.h"
#include "__fc_string_axiomatic.h"
-
#include "errno.h"
#include "signal.h"
+
/*
* Names of the interval timers, and structure
* defining a timer setting:
@@ -47,7 +49,6 @@ __BEGIN_DECLS
typedef unsigned int clock_t;
#define __clock_t_defined
#endif
-#include "__fc_define_time_t.h"
// From POSIX.1-2008: "The value of CLOCKS_PER_SEC shall be 1 million on
// XSI-conformant systems. [...]"
#define CLOCKS_PER_SEC ((time_t)1000000)
@@ -64,8 +65,6 @@ struct tm {
int tm_isdst; // Daylight Saving Time flag
};
-#include "__fc_define_timespec.h"
-
struct itimerspec {
struct timespec it_interval;
struct timespec it_value;
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 916d67d1a3a8bd10fbebc9ecfa91aca92b56c834..5979b51c4d998f8883c3d332861a36a51cd86688 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -29,6 +29,7 @@ __PUSH_FC_STDLIB
#include "__fc_define_max_open_files.h"
#include "__fc_define_size_t.h"
#include "__fc_define_null.h"
+#include "__fc_define_seek_macros.h"
#include "__fc_define_ssize_t.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_off_t.h"
@@ -36,10 +37,8 @@ __PUSH_FC_STDLIB
#include "__fc_define_useconds_t.h"
#include "__fc_define_intptr_t.h"
#include "__fc_define_fds.h"
-#include "__fc_select.h"
-
-
#include "limits.h"
+__BEGIN_DECLS
extern volatile int Frama_C_entropy_source;
@@ -55,8 +54,6 @@ extern volatile int Frama_C_entropy_source;
#define STDOUT_FILENO 1 /* Standard output. */
#define STDERR_FILENO 2 /* Standard error output. */
-#include "__fc_define_seek_macros.h"
-
/* compatibility macros */
#ifndef __FC_NO_MONOTONIC_CLOCK
@@ -67,8 +64,6 @@ extern volatile int Frama_C_entropy_source;
#define _POSIX_MONOTONIC_CLOCK 0
#endif
-__BEGIN_DECLS
-
/* Values for the NAME argument to `pathconf' and `fpathconf'. */
enum __fc_pathconf_name
{
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index bc77198c9b7df50e50eca7e5a477ae2e1c0bac45..53b38f02cd517ecf8d921d0aefa51f5aa9693d40 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -68,9 +68,10 @@
#include "__fc_define_ssize_t.h"
#include "__fc_define_stat.h"
#include "__fc_define_suseconds_t.h"
-#include "__fc_define_timespec.h"
#include "__fc_define_time_t.h"
#include "__fc_define_timer_t.h"
+#include "__fc_define_timespec.h"
+#include "__fc_define_timeval.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_useconds_t.h"
#include "__fc_define_wchar_t.h"