--- layout: fc_discuss_archives title: Message 44 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 can't comment on the segmentation fault but I wonder whether
you are aware that "i+5" may overflow for large values of "i".
Depending on your implementation of int you might then have "max_id < i".

Btw, "requires i" is in my opinion equivalent to "requires i != 0".
Is this what you want to express?

Jens

P.S.

If you are looking for a collection of ACSL examples you can have a look at

http://www.first.fraunhofer.de/fileadmin/FIRST/ACSL-by-Example.pdf



On 17.05.2012, at 18:02, dams wrote:

> 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,
> 
> 
> _______________________________________________
> 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