--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to include standard header (e.g. string.h) in Frama-C Sodium?



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;
}