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



On Wed, 21 Apr 2010, Claude Marche wrote:

> 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.
>
well in the Debian env (5.0.4 gcc 4.3.2) -pp-annot seems to work fine as 
well - will switch to the clean solution never the less.


thx!
hofrat