--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2013 ---
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 |