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: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Sun, 13 May 2012 20:12:17 +0000
  • In-reply-to: <4FAFF570.5030309@free.fr>
  • References: <4FAFF570.5030309@free.fr>
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