--- layout: fc_discuss_archives title: Message 23 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?



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                    |