--- layout: fc_discuss_archives title: Message 49 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



Claude Marche wrote:
>> 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...
>
I should have said more: first the -pp-annot option is not recommended 
since it is not guaranteed to work in any environment, I think it 
requires gcc to be the preprocessor. I guess there is something about 
that in the FAQ?

But anyway, ACSL provides a safe way to avoid any problems: \null 
denotes the null pointer. This is definitely the recommended way, and I 
will update the tutorial accordingly.

- Claude


-- 
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                    |