--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on April 2010 ---
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