--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on May 2012 ---
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