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?

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                    |