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