From 5647b9dda2c50cc9d0b13c0cc621c9654934e627 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 15 Jan 2020 18:39:24 +0100
Subject: [PATCH] [Libc] fix issue with undefined extern; restore GCC test with
linking
---
headers/header_spec.txt | 1 +
share/libc/__fc_runtime.c | 1 +
share/libc/unistd.c | 28 ++++++++++++++++++++++++++
tests/libc/oracle/fc_libc.0.res.oracle | 7 ++++---
tests/libc/oracle/fc_libc.1.res.oracle | 3 +--
tests/libc/runtime.c | 2 +-
6 files changed, 36 insertions(+), 6 deletions(-)
create mode 100644 share/libc/unistd.c
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 9abea47270c..ad7a910447d 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -296,6 +296,7 @@ share/libc/termios.h: CEA_LGPL
share/libc/tgmath.h: CEA_LGPL
share/libc/time.c: CEA_LGPL
share/libc/time.h: CEA_LGPL
+share/libc/unistd.c: CEA_LGPL
share/libc/unistd.h: CEA_LGPL
share/libc/utime.h: CEA_LGPL
share/libc/utmpx.h: CEA_LGPL
diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c
index b51db45b40c..b9c5c980d79 100644
--- a/share/libc/__fc_runtime.c
+++ b/share/libc/__fc_runtime.c
@@ -35,4 +35,5 @@
#include "stdio.c"
#include "stdlib.c"
#include "string.c"
+#include "unistd.c"
#include "wchar.c"
diff --git a/share/libc/unistd.c b/share/libc/unistd.c
new file mode 100644
index 00000000000..4e499e0f502
--- /dev/null
+++ b/share/libc/unistd.c
@@ -0,0 +1,28 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2019 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#include "unistd.h"
+#include "__fc_builtin.h"
+__PUSH_FC_STDLIB
+
+volatile char __fc_ttyname[TTY_NAME_MAX];
+__POP_FC_STDLIB
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 8554a5a2d79..4dec6771dc9 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -157,12 +157,12 @@
wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
wmemmove (0 call); write (0 call);
- 'Extern' global variables (17)
+ 'Extern' global variables (16)
==============================
__fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
__fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_hostname; __fc_locale;
- __fc_locale_names; __fc_mblen_state; __fc_mbtowc_state; __fc_ttyname;
- __fc_wctomb_state; optarg; opterr; optopt; tzname
+ __fc_locale_names; __fc_mblen_state; __fc_mbtowc_state; __fc_wctomb_state;
+ optarg; opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -242,6 +242,7 @@
#include "syslog.h"
#include "termios.h"
#include "time.h"
+#include "unistd.c"
#include "unistd.h"
#include "wchar.c"
#include "wchar.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index ed172048f4c..45e5eb7daef 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1742,8 +1742,7 @@ extern void sync(void);
assigns \result \from (indirect: name); */
extern long sysconf(int name);
-extern char volatile __fc_ttyname[32];
-
+char volatile __fc_ttyname[32];
char volatile *__fc_p_ttyname = __fc_ttyname;
/*@ requires valid_fildes: 0 ≤ fildes < 1024;
ensures
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index 260c3a09259..69ea8ad3649 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,6 +1,6 @@
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
- CMD: gcc -fsyntax-only -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99
+ CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
OPT:
*/
--
GitLab