From 4eeb5855fca5d874bbabc79bbfbd5f515131c1bb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 1 Feb 2019 15:51:12 +0100
Subject: [PATCH] [Libc] fix some minor issues
---
share/libc/malloc.h | 2 +-
share/libc/memory.h | 2 +-
share/libc/pthread.h | 4 ++--
share/libc/pwd.h | 5 +----
share/libc/semaphore.h | 2 +-
share/libc/time.h | 2 +-
share/libc/unistd.h | 4 ++--
share/libc/utmpx.h | 2 +-
.../variadic/tests/known/oracle/printf.res.oracle | 1 +
.../variadic/tests/known/oracle/swprintf.res.oracle | 1 +
.../variadic/tests/known/oracle/wchar.res.oracle | 1 +
tests/libc/oracle/fc_libc.0.res.oracle | 12 ++++++------
tests/libc/oracle/fc_libc.1.res.oracle | 8 ++------
13 files changed, 21 insertions(+), 25 deletions(-)
diff --git a/share/libc/malloc.h b/share/libc/malloc.h
index 3508e681088..89992c10aea 100644
--- a/share/libc/malloc.h
+++ b/share/libc/malloc.h
@@ -21,4 +21,4 @@
/**************************************************************************/
// This file is not in the C standard; it exists for compatibility purposes
-#include <stdlib.h>
+#include "stdlib.h"
diff --git a/share/libc/memory.h b/share/libc/memory.h
index 4c1227c6134..767739595b4 100644
--- a/share/libc/memory.h
+++ b/share/libc/memory.h
@@ -21,4 +21,4 @@
/**************************************************************************/
// This file is not in the C standard; it exists for compatibility purposes
-#include <string.h>
+#include "string.h"
diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index d55ece32dee..ac9f78bc234 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -366,8 +366,8 @@ extern void pthread_testcancel(void);
// From POSIX: "Inclusion of the <pthread.h> header shall make symbols defined
// in the headers <sched.h> and <time.h> visible."
-#include <sched.h>
-#include <time.h>
+// (sched.h has already been included)
+#include "time.h"
__POP_FC_STDLIB
#endif
diff --git a/share/libc/pwd.h b/share/libc/pwd.h
index c93e3126bec..7e12b710fbb 100644
--- a/share/libc/pwd.h
+++ b/share/libc/pwd.h
@@ -25,6 +25,7 @@
#include "features.h"
__PUSH_FC_STDLIB
+#include "__fc_builtin.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_string_axiomatic.h"
@@ -45,16 +46,12 @@ struct passwd {
extern char __fc_getpwuid_pw_name[64];
extern char __fc_getpwuid_pw_passwd[64];
-extern uid_t __fc_getpwuid_pw_uid;
-extern gid_t __fc_getpwuid_pw_gid;
extern char __fc_getpwuid_pw_dir[64];
extern char __fc_getpwuid_pw_shell[64];
struct passwd __fc_pwd =
{.pw_name = __fc_getpwuid_pw_name,
.pw_passwd = __fc_getpwuid_pw_passwd,
- .pw_uid = __fc_getpwuid_pw_uid,
- .pw_gid = __fc_getpwuid_pw_gid,
.pw_dir = __fc_getpwuid_pw_dir,
.pw_shell = __fc_getpwuid_pw_shell};
diff --git a/share/libc/semaphore.h b/share/libc/semaphore.h
index 264a85bfeda..765cd52cb54 100644
--- a/share/libc/semaphore.h
+++ b/share/libc/semaphore.h
@@ -26,7 +26,7 @@
#define __FC_SEMAPHORE
#include "features.h"
__PUSH_FC_STDLIB
-#include <time.h>
+#include "time.h"
__BEGIN_DECLS
diff --git a/share/libc/time.h b/share/libc/time.h
index ffe74960d94..60e5031571f 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -31,7 +31,7 @@ __PUSH_FC_STDLIB
#include "__fc_string_axiomatic.h"
#include "errno.h"
-
+#include "signal.h"
/*
* Names of the interval timers, and structure
* defining a timer setting:
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 3e790d21269..019c35bdad2 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -36,8 +36,8 @@ __PUSH_FC_STDLIB
#include "__fc_define_intptr_t.h"
#include "__fc_select.h"
-#include <getopt.h>
-#include <limits.h>
+#include "getopt.h"
+#include "limits.h"
extern volatile int Frama_C_entropy_source;
diff --git a/share/libc/utmpx.h b/share/libc/utmpx.h
index cc1c85dc142..8e38de8057f 100644
--- a/share/libc/utmpx.h
+++ b/share/libc/utmpx.h
@@ -26,7 +26,7 @@
__PUSH_FC_STDLIB
#include "__fc_define_pid_t.h"
-#include <sys/time.h>
+#include "sys/time.h"
__BEGIN_DECLS
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 6468d9e5be5..d3eac0b8fd4 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -155,6 +155,7 @@
/* Generated by Frama-C */
#include "errno.h"
#include "inttypes.h"
+#include "signal.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdint.h"
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 304d4dc1977..84ee5740088 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -54,6 +54,7 @@
__retres ∈ {0}
/* Generated by Frama-C */
#include "errno.h"
+#include "signal.h"
#include "stdarg.h"
#include "stdio.h"
#include "time.h"
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 0f8d049bfce..6d0225a7730 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -83,6 +83,7 @@
S___fc_stdout[0..1] ∈ [--..--]
/* Generated by Frama-C */
#include "errno.h"
+#include "signal.h"
#include "stdarg.h"
#include "stdio.h"
#include "time.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index eab1d99264c..ba81dc3d603 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -156,12 +156,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 (15)
==============================
- __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_gid;
- __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell;
- __fc_getpwuid_pw_uid; __fc_hostname; __fc_mblen_state; __fc_mbtowc_state;
- __fc_ttyname; __fc_wctomb_state; optarg; opterr; optopt; tzname
+ __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
+ __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_hostname;
+ __fc_mblen_state; __fc_mbtowc_state; __fc_ttyname; __fc_wctomb_state;
+ optarg; opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -171,7 +171,7 @@
==============
Sloc = 1083
Decision point = 204
- Global variables = 68
+ Global variables = 66
If = 195
Loop = 43
Goto = 89
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index a0d63cf77b1..c0bb6e199f8 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7050,10 +7050,6 @@ extern char __fc_getpwuid_pw_name[64];
extern char __fc_getpwuid_pw_passwd[64];
-extern uid_t __fc_getpwuid_pw_uid;
-
-extern gid_t __fc_getpwuid_pw_gid;
-
extern char __fc_getpwuid_pw_dir[64];
extern char __fc_getpwuid_pw_shell[64];
@@ -7061,8 +7057,8 @@ extern char __fc_getpwuid_pw_shell[64];
struct passwd __fc_pwd =
{.pw_name = __fc_getpwuid_pw_name,
.pw_passwd = __fc_getpwuid_pw_passwd,
- .pw_uid = __fc_getpwuid_pw_uid,
- .pw_gid = __fc_getpwuid_pw_gid,
+ .pw_uid = 0U,
+ .pw_gid = 0U,
.pw_gecos = (char *)0,
.pw_dir = __fc_getpwuid_pw_dir,
.pw_shell = __fc_getpwuid_pw_shell};
--
GitLab