Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] [jessie-plugin] cannot be used on your code
  • From: damien.balima at free.fr (dams)
  • Date: Sun, 13 May 2012 19:54:56 +0200
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