Frama-C-discuss mailing list archives

damien.balima at free.fr (dams) · Thu, 17 May 2012 18:02:45 +0200

Hi,

Thanks for the reply. I will get step-by-step, function by function. By 
the way, I've just try a simple test, like :
//@ requires i;
int test(int i){
     int max_id = i+5;
     /*@
       @ loop invariant max_id > i;
       @ loop variant max_id-i;
       @*/
     while(i<max_id){
         i++;
     }

     return i;
}

int main(){
     int a = 1;
     int b = test(a);
     return b;
}

which is a simple test. Then I've got a recurrent  error :
frama-c -jessie test.c
[kernel] preprocessing with "gcc -C -E -I.  -dD test.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir test.jessie
[jessie] File test.jessie/test.jc written.
[jessie] File test.jessie/test.cloc written.
[jessie] Calling Jessie tool in subdir test.jessie
Generating Why function test
Generating Why function main
[jessie] Calling VCs generator.
gwhy-bin [...] why/test.why
Computation of VCs...
Computation of VCs done.
Reading GWhy configuration...
Loading .gwhyrc config file
GWhy configuration loaded...
Creating GWhy Tree view...
GWhy Tree view created...
Creating GWhy views...
Segmentation fault
make: *** [test.stat] Erreur 139
[jessie] user error: Jessie subprocess failed: make -f test.makefile gui

and using why directly :
why test.why
File "test.why", line 11, characters 27-33:
Unbound type 'tag_id'

I've got this "unbound type 'tag_id' error" even on a no specified 
simple code.
It is the Debian sid version of frama-c (version 20111001 nitrogen 
dfsg-4), with why 2.30.

It didn't seems to have a norm.ml file in the source downloaded by an 
"apt-get source frama-c" command, neither a frama-c-plugin directory or 
the line code below.

Regards,

Le 14/05/2012 12:01, frama-c-discuss-request at lists.gforge.inria.fr a 
?crit :
> Message: 1
> Date: Sun, 13 May 2012 19:54:56 +0200
> From: dams<damien.balima at free.fr>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: [Frama-c-discuss] [jessie-plugin] cannot be used on your code
> Message-ID:<4FAFF570.5030309 at free.fr>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> 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
>
>
>
> ------------------------------
>
> Message: 2
> Date: Sun, 13 May 2012 20:12:17 +0000
> From: Jens Gerlach<jens.gerlach at first.fraunhofer.de>
> To: Frama-C public discussion<frama-c-discuss at lists.gforge.inria.fr>
> Subject: Re: [Frama-c-discuss] [jessie-plugin] cannot be used on your
> 	code
> Message-ID:<7E942D31-56B3-4B7C-AE44-157150EB3C3A at first.fraunhofer.de>
> Content-Type: text/plain; charset="us-ascii"
>
> 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
>
>
> ------------------------------
>
> Message: 3
> Date: Mon, 14 May 2012 09:58:39 +0200
> From: Virgile Prevosto<virgile.prevosto at m4x.org>
> To: Frama-C public discussion<frama-c-discuss at lists.gforge.inria.fr>
> Subject: Re: [Frama-c-discuss] [jessie-plugin] cannot be used on your
> 	code
> Message-ID:
> 	<CA+yPOVhSn94Oboe+oqzMLcgZ3nvK=MrTtnWT9SjTfnKpDpttjA at mail.gmail.com>
> Content-Type: text/plain; charset=ISO-8859-1
>
> Hello,
>
> 2012/5/13 dams<damien.balima at free.fr>:
>> [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
>> :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.
> As Jens said, you probably won't be able to prove much if you don't
> provide specifications for the functions you use. Some of stdlib
> functions have a partial specification in $FRAMAC_SHARE/libc, but this
> is very incomplete and can have bugs (some of them have already been
> reported and will be fixed in Oxygen, but there's likely more, as this
> is not the most tested part of Frama-C).
> That said, the warnings about the lack of specification for functions
> without code and the fact there's a feature that Jessie does not
> understand in your code are not necessarily related.
> If you happen to compile the Jessie plug-in from sources, the
> following patch will let Frama-C print the lval that is not handled by
> the Jessie plug-in. Otherwise, there's little that can be done without
> seeing the code under analysis.
>
> --- frama-c-plugin/norm.ml	2011-10-24 17:21:06.000000000 +0200
> +++ frama-c-plugin/norm.ml.new	2012-05-14 09:54:53.038692786 +0200
> @@ -1567,7 +1567,7 @@
>       match lv with
>         | Var _, NoOffset ->  lv
>         | Var _, _ ->
> -          unsupported "cannot handle this lvalue"
> +          unsupported "cannot handle this lvalue: %a" !Ast_printer.d_lval lv;
>         | Mem e, NoOffset ->
>             begin match self#wrap_type_if_needed (typeOf e) with
>               | Some newtyp ->
>
>
>
> Best regards,