Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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