--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2015 ---
Hello, I have attached C code, including <string.h> and calling strcpy(). I would like to prove this kind of code using WP. I use the following command line: frama-c -frama-c-stdlib -wp -wp-rte string_use.c However, I get following warnings: """ [wp] warning: No definition for 'memchr' interpreted as reads nothing [wp] warning: No definition for 'strlen' interpreted as reads nothing [wp] warning: No definition for 'memset' interpreted as reads nothing [wp] warning: No definition for 'strchr' interpreted as reads nothing [wp] warning: No definition for 'strcmp' interpreted as reads nothing [wp] warning: No definition for 'strncmp' interpreted as reads nothing [wp] warning: No definition for 'wcscmp' interpreted as reads nothing [wp] warning: No definition for 'wcslen' interpreted as reads nothing [wp] warning: No definition for 'wcsncmp' interpreted as reads nothing """ How should I call Frama-C Sodium to avoid those warnings? From my understanding of §5.1 of User manual, -frama-c-stdlib should be enough. In FRAMAC_SHARE/libc/string.h (including __fc_string_axiomatic.h), all the needed function contracts are defined (e.g. memchr()). Best regards, david -------------- next part -------------- #include <string.h> int main(void) { char *s = "abc"; char t[4]; strcpy(t, s); return 0; }