--- layout: fc_discuss_archives title: Message 32 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



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