Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
F
frama-c
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
14
Issues
14
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
pub
frama-c
Commits
5647b9dd
Commit
5647b9dd
authored
Jan 15, 2020
by
Andre Maroneze
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
[Libc] fix issue with undefined extern; restore GCC test with linking
parent
fcbcb538
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
36 additions
and
6 deletions
+36
-6
headers/header_spec.txt
headers/header_spec.txt
+1
-0
share/libc/__fc_runtime.c
share/libc/__fc_runtime.c
+1
-0
share/libc/unistd.c
share/libc/unistd.c
+28
-0
tests/libc/oracle/fc_libc.0.res.oracle
tests/libc/oracle/fc_libc.0.res.oracle
+4
-3
tests/libc/oracle/fc_libc.1.res.oracle
tests/libc/oracle/fc_libc.1.res.oracle
+1
-2
tests/libc/runtime.c
tests/libc/runtime.c
+1
-1
No files found.
headers/header_spec.txt
View file @
5647b9dd
...
...
@@ -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
...
...
share/libc/__fc_runtime.c
View file @
5647b9dd
...
...
@@ -35,4 +35,5 @@
#include "stdio.c"
#include "stdlib.c"
#include "string.c"
#include "unistd.c"
#include "wchar.c"
share/libc/unistd.c
0 → 100644
View file @
5647b9dd
/**************************************************************************/
/* */
/* 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
tests/libc/oracle/fc_libc.0.res.oracle
View file @
5647b9dd
...
...
@@ -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 (1
7
)
'Extern' global variables (1
6
)
==============================
__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_
ttynam
e;
__fc_wctomb_state;
optarg; opterr; optopt; tzname
__fc_locale_names; __fc_mblen_state; __fc_mbtowc_state; __fc_
wctomb_stat
e;
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"
...
...
tests/libc/oracle/fc_libc.1.res.oracle
View file @
5647b9dd
...
...
@@ -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
...
...
tests/libc/runtime.c
View file @
5647b9dd
/* 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:
*/
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment