--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [jessie-plugin] cannot be used on your code



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