--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on April 2010 ---
Nicholas Mc Guire wrote: > the make problem is gone for alt-ergo,z3,cvc3,simplify - Thanks ! > > good ! > from the makefile - I guess for isabelle you also would need > Isabelle -> Isabelle.output_file (fwe ^ "_why.thy") ?? > > No, because Isabelle is not available under GWhy, and the problem was introduced by a recent change in the handling of Gwhy temporary files. > and... a new one poped up (max example from tutorial): > > ... > max1.c:2:[kernel] user error: Error during annotations analysis: unbound logic variable NULL > you need option -pp-annot of frama-c. You are right, it should be said in the tutorial... Thanks for reporting! -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |