diff --git a/share/libc/features.h b/share/libc/features.h
index 0aa904e48573e3535006b3fac1112abc9bf27426..77ea2e2cac68158bb7c727efe0098ab9ef547fdc 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 84a397167bba58916fa050901842843fa26715e5..54eda346537cd771aed962413bc6adb65504a8b8 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 f0e37fef4d6d1b36d513e07ea8beedac43e7df6a..2666ef3298b503a17ead4ca3f0b97904298ee98a 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 37749792bb6187579df6a8e994f804b9bfd99e7f..acf3cfd95fab5e5803d8aef76950b9b7dcd122db 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 98735a9afbaabfd7ad65bda2459c2a1b60231e9a..688c2885483ab84cac47bdaae2a7ad9d8582bb08 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 fa5202ebf4aa0bc12b3cc3e015cbc771fdc5ee45..39b1c43044e73259b624ef6a348669f8a123279f 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 ce3c8be4b5029c0c74d8d54edff859949934a7ae..fbd3da31927d47879bb7ef0c81bf878ba4b5fbc7 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 e2d7c4000014cbc12ae389de90f07b8601f6cb16..a8c71c4da66bfde812e77250d56ab9b6192509b8 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 d9ada05d4207950e6c8b590c366c45354ebea8d0..7268da8856d2fa7c9e31f8aa80193f48014b612e 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"