--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on May 2012 ---
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