--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how jessie and why platform work to generate a .v output?



Same mistake as before, don't call why3 directly on generated files,
because you need to put extra parameters. Use the max.makefile instead

- Claude
Le 06/11/2013 07:29, Xiao-lei Cui a ?crit :
> Following the why3 manual, as I run :
> cuix at berkhoff:~/projects/frama-c/max/max.jessie$  why3 -P alt-ergo max.mlw
> File "max.mlw", line 7, characters 0-46:
> Theory not found: jessie3theories.Jessie_memory_model
> 
> I also tried some simple input files and example shipped with source,
> the attached .why and .mlw seems working.
> 
> What I did is I upgraded frama-c-carbon/why2.29 to
> frama-c-fluorine/why3(0.81), re-installed why2(but this time it is
> why2.33 to be compatible with frama-c-fluorine).
> 
> Thanks!!
> 
> Xiaolei
> ------------------------------------------------------------------------
> From: x_cui at hotmail.com
> To: frama-c-discuss at lists.gforge.inria.fr
> Date: Tue, 5 Nov 2013 21:38:28 -0500
> Subject: Re: [Frama-c-discuss] how jessie and why platform work to
> generate a .v output?
> 
> Hello,
>   I re-configured why2 and installed it. frama-c now can recognize
> jessie plugin, however, as I tried a previous demo, why3IDE complains :
>    "Error while reading file '../max.mlw': File "max/../max.mlw", line
> 487, characters 9-36: this expression raises unlisted exception
> Return_label_exc"
>    No proof obligations are shown in the IDE. The demo max.c works fine
> with frama-c-carbon/why2 though:)
>    Thanks again.   
> 
>  $ frama-c -jessie -pp-annot max.c
> [kernel] preprocessing with "gcc -C -E -I.  -dD max.c"
> [jessie] Starting Jessie translation
> [jessie] Producing Jessie files in subdir max.jessie
> [jessie] File max.jessie/max.jc written.
> [jessie] File max.jessie/max.cloc written.
> [jessie] Calling Jessie tool in subdir max.jessie
> Generating Why function max
> Generating Why function main
> [jessie] Calling VCs generator.
> why3ide --extra-config /usr/local/lib/why/why3/why3.conf max.mlw
> [Info] Init the GTK interface... done.
> [Info] reading icons... done.
> [Info] Creating tree model... done
> [Info] found regular file 'max.mlw'
> [Info] using 'max' as directory for the project
> [Info] Opening session...
>  
> [Info] Opening session: update done
>  
> [Info] Opening session: done
> Adding file '../max.mlw'
> [Info] adding file ../max.mlw in database
> [Info] saving IDE config file
> 
> 
> 
> 
> 
> 
>> Date: Tue, 5 Nov 2013 15:47:36 +0100
>> From: Claude.Marche at inria.fr
>>
>>
>> You should install Why2 after Why3. So in your case, reconfigure why2
>> (check that frama-c support will be compiled), compile and install it.
>>
>> - Claude
>>
>> Le 05/11/2013 15:10, Xiao-lei Cui a ?crit :
>> > hello, thanks for tip!!
>> > I now upgraded frama-c from frama-c-carbon to
>> > frama-c-Fluorine-20130401. And installed why3(0.81). However, as I try
>> > out frama-c:
>> > $ frama-c -jessie file.c
>> >
>> > It complains "option -jessie is unknown".
>> > Running
>> > $ frama-c -help
>> > the -jessie option is not shown.
>> >
>> > Any ideas? :)
>> >
>> > xiaolei
>> >
>> >
>> >
>> >
>> >> Date: Tue, 5 Nov 2013 14:31:35 +0100
>> >> From: Claude.Marche at inria.fr
>> >> To: frama-c-discuss at lists.gforge.inria.fr
>> >> Subject: Re: [Frama-c-discuss] how jessie and why platform work to
>> > generate a .v output?
>> >>
>> >>
>> >> Hi,
>> >>
>> >> Le 02/11/2013 05:45, Xiao-lei Cui a ?crit :
>> >> > Hi all,
>> >> > I am trying to figure out the workflow from C source(plus
>> >> > embeddedACSL spec) to the .v file passed to proof assistant.
>> >> > I am using why2. Is the following workflow correct?
>> >> > C/ACSL -> (frama-c/jessie)
>> >> > -->filename.jc ->(jessie/why)
>> >> > -->filename.why->(why)
>> >>
>> >> more or less
>> >>
>> >> > from
>> >> >> frama-c -jessie -pp-annot max.c
>> >> > I got max.why, which is over 300lines of code.
>> >> > I then use why command to generate .v output for coq:
>> >> >> why --coq max.why
>> >> > File "max.why", line 17, characters 29-35:
>> >> > Unbound type 'tag_id'
>> >> >
>> >> > Did I miss something or some step?
>> >> > Thanks in advance.
>> >>
>> >> the "why" command should be giving an additional prelude file as input.
>> >> Indeed you should not call why directly but use
>> >>
>> >> make -f max.makefile coq
>> >>
>> >> Anyway, the support of Coq in Why2 is known to be painful for the user.
>> >> Using Coq to discharge VCs using Why3 is much much easier to do, so I
>> >> strongly recommend to use Why3 instead.
>> >>
>> >> - Claude
>> >>
>> >>
>> >>
>> >>
>> >>
>> >> --
>> >> Claude March? | tel: +33 1 72 92 59 69
>> >> INRIA Saclay - ?le-de-France |
>> >> Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
>> >> F-91405 ORSAY Cedex |
>> >>
>> >>
>> >> _______________________________________________
>> >> 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
>> >
>> >
>> > _______________________________________________
>> > 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
>> >
>>
>> --
>> Claude March? | tel: +33 1 72 92 59 69
>> INRIA Saclay - ?le-de-France |
>> Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
>> F-91405 ORSAY Cedex |
>>
>>
>> _______________________________________________
>> 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
> 
> _______________________________________________ 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
> 
> 
> _______________________________________________
> 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
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |