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