From 104fb6a5ab7f068ee9100fda02f32cd8d4e92804 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 4 May 2021 15:44:02 +0200
Subject: [PATCH] [libc] refactor and fix definitions
---
headers/header_spec.txt | 1 +
share/libc/__fc_define_timeval.h | 36 ++++++++++++++++++++++++++++++++
share/libc/__fc_select.h | 8 +++----
share/libc/getopt.h | 3 +--
share/libc/sys/time.h | 13 ++++--------
share/libc/time.h | 9 ++++----
share/libc/unistd.h | 9 ++------
tests/libc/fc_libc.c | 3 ++-
8 files changed, 53 insertions(+), 29 deletions(-)
create mode 100644 share/libc/__fc_define_timeval.h
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d5a4550ba81..23e24fa4d73 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 00000000000..34db8894a58
--- /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 4fc0f3b0aa6..1fad5956e87 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 ed3f45384b7..380abc7f5ab 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 fbd3da31927..db0a5b17b0b 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 d156b59c620..fe6304ce88d 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 916d67d1a3a..5979b51c4d9 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 bc77198c9b7..53b38f02cd5 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"
--
GitLab