diff --git a/share/libc/glob.c b/share/libc/glob.c index b4b55cda11a3ad9d9538da387aebb78926345d06..5eff2df86de7f9fd058f710691574e9354edb088 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 0b3dc103fce5463b9c65b9522fdb8eb7b2d0d6c4..7a21928517b84c8fac08f455c6fcb7520835abd6 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 182d8d7e8dd2734bd10eacc23cd9f95b4dd8c758..493d1fc84ae2450e5a5a17fe1a15da3983c0aa2e 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 68f12a1ccf8e929e753b86f9223ed49031911545..a0e7fbe8ec4872d3ced20961cdcdba5f01c093f5 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 9874c18211f312864165db98c7e9ac3adef3e402..e473fe89afb026b9a81774ef8121ac3ef6f43d3d 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 998ca167775c63aeb536528f925d71204e8637e2..7fef5b93a060aeaa0c66cd03227833b92065541f 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) {