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: Thu, 17 May 2012 18:27:04 +0000
  • In-reply-to: <4FB52125.1090505@free.fr>
  • References: <mailman.29.1336989688.28070.frama-c-discuss@lists.gforge.inria.fr> <4FB52125.1090505@free.fr>

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