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