[libc] refactor and fix definitions

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

share/libc/__fc_define_timeval.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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;

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

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;

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;

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
   {

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"