--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on May 2012 ---
Hello, You need contracts for the functions listed by you. Frama-C comes only with a few standard C functions. So, you probably have to come up with your own contracts. By the way, I should have asked first what kind of properties do you want to formally verify? Enlighten us, please. Regards Jens Am 13.05.2012 um 19:57 schrieb "dams" <damien.balima at free.fr>: > Hi, > > I'm trying to do some formal verification on a simple socket unix server. The code can be open with frama-c-gui, it can do some verification with WP, but jessie doesn't. > The log say : > > [kernel] preprocessing with "gcc -C -E -I. -dD serveur_frama.c" > [jessie] Starting Jessie translation > [kernel] warning: No code for function accept, default assigns generated for default behavior > [kernel] warning: No code for function atoi, default assigns generated for default behavior > [kernel] warning: No code for function bind, default assigns generated for default behavior > [kernel] warning: No code for function bzero, default assigns generated for default behavior > [kernel] warning: No code for function close, default assigns generated for default behavior > [kernel] warning: No code for function exit, default assigns generated for default behavior > [kernel] warning: No code for function fflush, default assigns generated for default behavior > [kernel] warning: No code for function fgets, default assigns generated for default behavior > [kernel] warning: No code for function free, default assigns generated for default behavior > [kernel] warning: No code for function htonl, default assigns generated for default behavior > [kernel] warning: No code for function htons, default assigns generated for default behavior > [kernel] warning: No code for function inet_ntoa, default assigns generated for default behavior > [kernel] warning: No code for function listen, default assigns generated for default behavior > [kernel] warning: No code for function malloc, default assigns generated for default behavior > [kernel] warning: No code for function memset, default assigns generated for default behavior > [kernel] warning: No code for function perror, default assigns generated for default behavior > [kernel] warning: No code for function printf, default assigns generated for default behavior > [kernel] warning: No code for function read, default assigns generated for default behavior > [kernel] warning: No code for function select, default assigns generated for default behavior > [kernel] warning: No code for function shutdown, default assigns generated for default behavior > [kernel] warning: No code for function socket, default assigns generated for default behavior > [kernel] warning: No code for function sprintf, default assigns generated for default behavior > [kernel] warning: No code for function strcat, default assigns generated for default behavior > [kernel] warning: No code for function strcmp, default assigns generated for default behavior > [kernel] warning: No code for function strcpy, default assigns generated for default behavior > [kernel] warning: No code for function strlen, default assigns generated for default behavior > [kernel] warning: No code for function strncmp, default assigns generated for default behavior > [kernel] warning: No code for function strncpy, default assigns generated for default behavior > [kernel] warning: No code for function strtok, default assigns generated for default behavior > [kernel] warning: No code for function write, default assigns generated for default behavior > :0:[jessie] failure: cannot handle this lvalue > [jessie] warning: Unsupported feature(s). > Jessie plugin can not be used on your code. > > Is there a fatal problem with these function, witch are standard C function ? My code can compile with GCC, it works fine. > > Regards, > > Damien > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss