--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on April 2010 ---
On Thu, 22 Apr 2010, Julien Signoles wrote: > Claude Marche a ?crit : >> 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? > > The -pp-annot option as well as all the other general options of Frama-C > is fully documented in the Frama-C user manual. > > This particular option is described page 23 of the manual (easy to find > through the index). > yes - the problem is not finding the documentation for -pp-annot i.e. in the man page to frama-c - the problem was rather to figure out from the error message that one actually needs to preprocess the file. [-no]-pp-annot pre-process annotations. This is currently only possible when using gcc (or GNU cpp) pre-processor. The default is to not pre- process annotations. the manually equally only states what -pp-annot is for, but gives no reason why it is needed. Now this is self-explaining to anybody using these tools for some time - but not to a newbee ;) thx! hofrat