--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on November 2013 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131105/26a2f5b5/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: max.mlw Type: application/octet-stream Size: 20494 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131105/26a2f5b5/attachment-0001.obj> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: max.c URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131105/26a2f5b5/attachment-0001.c>