--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.24 install question



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                    |