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] 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                    |