From bbddbb19f54498a9cf4b9d99958722a162eccaf8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 5 Jun 2020 09:34:35 +0200
Subject: [PATCH] [Libc] avoid GCC warnings in C stubs
---
share/libc/glob.c | 2 +-
share/libc/locale.c | 8 ++++++--
share/libc/netdb.c | 2 +-
share/libc/netdb.h | 2 +-
share/libc/stdlib.c | 2 +-
share/libc/string.c | 4 ++++
6 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/share/libc/glob.c b/share/libc/glob.c
index b4b55cda11a..5eff2df86de 100644
--- a/share/libc/glob.c
+++ b/share/libc/glob.c
@@ -71,7 +71,7 @@ int glob(const char *pattern, int flags,
for (size_t i = 0; i < reserve_offs; i++) pglob->gl_pathv[i] = 0;
for (size_t i = 0; i < pglob->gl_pathc; i++) {
- pglob->gl_pathv[reserve_offs + prev_len + i] = "glob result";
+ pglob->gl_pathv[reserve_offs + prev_len + i] = (char*)"glob result";
}
pglob->gl_pathv[prev_len + reserve_offs + pglob->gl_pathc] = 0; // terminator
if (Frama_C_nondet(0, 1)) { // simulate "no error"
diff --git a/share/libc/locale.c b/share/libc/locale.c
index 0b3dc103fce..7a21928517b 100644
--- a/share/libc/locale.c
+++ b/share/libc/locale.c
@@ -23,11 +23,15 @@
#include "locale.h"
#include "limits.h"
__PUSH_FC_STDLIB
-struct lconv __C_locale = {".","","","","","","","","","",CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX};
+struct lconv __C_locale = {(char*)".",(char*)"",(char*)"",(char*)"",(char*)"",
+ (char*)"",(char*)"",(char*)"",(char*)"",(char*)"",
+ CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,
+ CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,
+ CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX};
struct lconv *__frama_c_locale=&__C_locale;
-char*__frama_c_locale_names[512]={"C"};
+char*__frama_c_locale_names[512]={(char*)"C"};
char *setlocale(int category, const char *locale) {
if (*locale == 'C')
{ __frama_c_locale = &__C_locale;
diff --git a/share/libc/netdb.c b/share/libc/netdb.c
index 182d8d7e8dd..493d1fc84ae 100644
--- a/share/libc/netdb.c
+++ b/share/libc/netdb.c
@@ -69,7 +69,7 @@ int getaddrinfo(
ai -> ai_protocol = Frama_C_interval(0,IPPROTO_MAX);
ai -> ai_addrlen = sizeof(*sa) ;
ai -> ai_addr = sa ;
- ai -> ai_canonname = "dummy" ;
+ ai -> ai_canonname = (char*)"dummy" ;
ai -> ai_next = NULL;
*res = ai;
return 0;
diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index 68f12a1ccf8..a0e7fbe8ec4 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -121,7 +121,7 @@ extern void endservent(void);
*/
extern void freeaddrinfo(struct addrinfo * addrinfo);
-char *__fc_gai_strerror = "<error message reported by gai_strerror>";
+char *__fc_gai_strerror = (char*)"<error message reported by gai_strerror>";
/*@
assigns \result \from indirect:errcode, __fc_gai_strerror;
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index 9874c18211f..e473fe89afb 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -111,7 +111,7 @@ char *getenv(const char *name)
int putenv(char *string)
{
- char *separator = strchr(string, '=');
+ char *separator __attribute__((unused)) = strchr(string, '=');
//@ assert string_contains_separator: separator != \null;
//@ assert name_is_not_empty: separator != string;
diff --git a/share/libc/string.c b/share/libc/string.c
index 998ca167775..7fef5b93a06 100644
--- a/share/libc/string.c
+++ b/share/libc/string.c
@@ -272,7 +272,9 @@ char *strstr(const char *haystack, const char *needle)
}
char __fc_strerror[64];
+#ifdef __FRAMAC__
static int __fc_strerror_init;
+#endif
char *strerror(int errnum)
{
@@ -318,7 +320,9 @@ char *strndup(const char *s, size_t n)
}
char __fc_strsignal[64];
+#ifdef __FRAMAC__
static int __fc_strsignal_init;
+#endif
char *strsignal(int signum)
{
--
GitLab