diff --git a/share/libc/string.c b/share/libc/string.c index 99e54e162ad796fc903922f4068d0556d1996e82..fc5a78937200d259df42f5b344fa923428738dc4 100644 --- a/share/libc/string.c +++ b/share/libc/string.c @@ -271,9 +271,19 @@ char *strstr(const char *haystack, const char *needle) return NULL; } +char __fc_strerror[64]; +static int __fc_strerror_init; + char *strerror(int errnum) { - return "strerror message by Frama-C"; +#ifdef __FRAMAC__ + if (!__fc_strerror_init) { + Frama_C_make_unknown(__fc_strerror, 63); + __fc_strerror[63] = 0; + __fc_strerror_init = 1; + } +#endif + return __fc_strerror; } /* Warning: read considerations about malloc() in Frama-C */ @@ -307,4 +317,19 @@ char *strndup(const char *s, size_t n) return p; } +char __fc_strsignal[64]; +static int __fc_strsignal_init; + +char *strsignal(int signum) +{ +#ifdef __FRAMAC__ + if (!__fc_strsignal_init) { + Frama_C_make_unknown(__fc_strsignal, 63); + __fc_strsignal[63] = 0; + __fc_strsignal_init = 1; + } +#endif + return __fc_strsignal; +} + __POP_FC_STDLIB