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