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



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
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131105/94442c7e/attachment.html>