From 45321ce1c5bef8dfa0650b7af80d24dea022075f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 21 Jun 2021 18:56:22 +0200
Subject: [PATCH] [Libc] avoid issue with linking of extern declarations
---
share/libc/features.h | 7 +++++++
share/libc/libgen.h | 4 ++--
share/libc/pwd.h | 8 ++++----
share/libc/signal.h | 2 +-
share/libc/stdlib.h | 2 +-
share/libc/string.h | 4 ++--
share/libc/sys/time.h | 6 +++---
share/libc/unistd.h | 2 +-
src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c | 1 +
9 files changed, 22 insertions(+), 14 deletions(-)
diff --git a/share/libc/features.h b/share/libc/features.h
index 0aa904e4857..77ea2e2cac6 100644
--- a/share/libc/features.h
+++ b/share/libc/features.h
@@ -115,5 +115,12 @@
#define __USE_ISOC99 1
+// When linking code including Frama-C's libc, we avoid adding 'extern'
+// to some variable declarations. In this case, __FC_EXTERN is defined to
+// the empty string. Otherwise, define it to 'extern'.
+#ifndef __FC_EXTERN
+#define __FC_EXTERN extern
+#endif
+
/* end __FC_FEATURES_H */
#endif
diff --git a/share/libc/libgen.h b/share/libc/libgen.h
index 84a397167bb..54eda346537 100644
--- a/share/libc/libgen.h
+++ b/share/libc/libgen.h
@@ -28,7 +28,7 @@
__PUSH_FC_STDLIB
__BEGIN_DECLS
-extern char __fc_basename[__FC_PATH_MAX];
+__FC_EXTERN char __fc_basename[__FC_PATH_MAX];
char *__fc_p_basename = __fc_basename;
/*@ // missing: assigns path[0 ..], __fc_p_basename[0 ..] \from 'filesystem';
@@ -40,7 +40,7 @@ char *__fc_p_basename = __fc_basename;
*/
extern char *basename(char *path);
-extern char __fc_dirname[__FC_PATH_MAX];
+__FC_EXTERN char __fc_dirname[__FC_PATH_MAX];
char *__fc_p_dirname = __fc_dirname;
/*@ // missing: assigns path[0 ..], __fc_p_dirname[0 ..] \from 'filesystem';
diff --git a/share/libc/pwd.h b/share/libc/pwd.h
index f0e37fef4d6..2666ef3298b 100644
--- a/share/libc/pwd.h
+++ b/share/libc/pwd.h
@@ -44,10 +44,10 @@ struct passwd {
char *pw_shell;
};
-extern char __fc_getpwuid_pw_name[64];
-extern char __fc_getpwuid_pw_passwd[64];
-extern char __fc_getpwuid_pw_dir[64];
-extern char __fc_getpwuid_pw_shell[64];
+__FC_EXTERN char __fc_getpwuid_pw_name[64];
+__FC_EXTERN char __fc_getpwuid_pw_passwd[64];
+__FC_EXTERN char __fc_getpwuid_pw_dir[64];
+__FC_EXTERN char __fc_getpwuid_pw_shell[64];
struct passwd __fc_pwd =
{.pw_name = __fc_getpwuid_pw_name,
diff --git a/share/libc/signal.h b/share/libc/signal.h
index 37749792bb6..acf3cfd95fa 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -201,7 +201,7 @@ extern int sigdelset(sigset_t *set, int signum);
*/
extern int sigismember(const sigset_t *set, int signum);
-extern struct sigaction __fc_sigaction[SIGRTMAX+1];
+__FC_EXTERN struct sigaction __fc_sigaction[SIGRTMAX+1];
struct sigaction *__fc_p_sigaction = __fc_sigaction;
/*@ // missing: errno may be set to EINVAL when trying to set some signals
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 98735a9afba..688c2885483 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -286,7 +286,7 @@ extern void srandom(unsigned int seed);
// used to check if some *48() functions have called the seed initializer
int __fc_random48_init;
-extern unsigned short __fc_random48_counter[3];
+__FC_EXTERN unsigned short __fc_random48_counter[3];
unsigned short *__fc_p_random48_counter = __fc_random48_counter;
/*@
diff --git a/share/libc/string.h b/share/libc/string.h
index fa5202ebf4a..39b1c43044e 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -336,7 +336,7 @@ extern char *strtok_r(char *restrict s, const char *restrict delim, char **restr
@*/
extern char *strsep (char **stringp, const char *delim);
-extern char __fc_strerror[64];
+__FC_EXTERN char __fc_strerror[64];
char * const __fc_p_strerror = __fc_strerror;
// Note: postcondition "result_nul_terminated" is only a temporary patch,
@@ -514,7 +514,7 @@ extern char *stpncpy(char *restrict dest, const char *restrict src, size_t n);
//extern char *strerror_l(int errnum, locale_t locale);
extern int strerror_r(int errnum, char *strerrbuf, size_t buflen);
-extern char __fc_strsignal[64];
+__FC_EXTERN char __fc_strsignal[64];
char * const __fc_p_strsignal = __fc_strsignal;
/*@ //missing: requires valid_signal(signum);
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index ce3c8be4b50..fbd3da31927 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -99,8 +99,9 @@ extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
*/
extern int settimeofday(const struct timeval *tv, const struct timezone *tz);
-#if (defined _POSIX_C_SOURCE && (_POSIX_C_SOURCE) >= 200112L) || \
- (defined _XOPEN_SOURCE && (_XOPEN_SOURCE) >= 600)
+// Note: definitions related to itimerval are obsolescent in POSIX and may be
+// removed in future versions. Strictly conforming applications should not use
+// them.
#define ITIMER_REAL 0
#define ITIMER_VIRTUAL 1
#define ITIMER_PROF 2
@@ -199,7 +200,6 @@ extern int getitimer(int which, struct itimerval *curr_value);
extern int setitimer (int which,
const struct itimerval *restrict new_value,
struct itimerval *restrict old_value);
-#endif
// Non-POSIX, non-C99 functions (present in Linux and most BSDs)
extern void timeradd(struct timeval *a, struct timeval *b,
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index e2d7c400001..a8c71c4da66 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -1104,7 +1104,7 @@ extern pid_t tcgetpgrp(int);
extern int tcsetpgrp(int, pid_t);
extern int truncate(const char *, off_t);
-extern volatile char __fc_ttyname[TTY_NAME_MAX];
+__FC_EXTERN volatile char __fc_ttyname[TTY_NAME_MAX];
volatile char *__fc_p_ttyname = __fc_ttyname;
/*@
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
index d9ada05d420..7268da8856d 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
@@ -7,6 +7,7 @@
#include "string.h"
#include "sys/select.h"
#include "sys/time.h"
+#include "sys/types.h"
#include "sys/wait.h"
#include "time.h"
#include "unistd.h"
--
GitLab