--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on March 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Error on using pp-annot



Hello,

On Sun, Mar 30, 2014 at 9:45 AM, Frank Dordowsky <frank at strato.de> wrote:

> Hello,
> I am trying to expand macro definitions within ACSL annotations using the
> pp-annot option. Unfortunately, I get an error on processing standard
> include files:
>
>          [kernel] preprocessing with "gcc -C -E -I. -I
> /usr/share/frama-c/libc -nostdinc -dD constant.c"
>          /usr/include/stdc-predef.h:1:[kernel] user error: unexpected
> token '/'
>          [kernel] user error: skipping file "constant.c" that has errors.
>          [kernel] Frama-C aborted: invalid user input.
>
> I have used the following command:
>
>   frama-c -cpp-extra-args="-I /usr/share/frama-c/libc" -pp-annot -wp
> -wp-rte
>

Generally speaking, you should always use the headers provided with Frama-C
instead of those from your system.

When using GCC or a compatible compiler such as Clang, this involves
passing the pre-processor the options -nostdinc and -I... where "..."
stands for the place where Frama-C's headers were installed. This
locationcan be obtained from Frama-C with the option -print-share-path.

All in all, it may look like:

frama-c -cpp-extra-args=-nostdinc -cpp-extra-args=`frama-c
-print-share-path`/libc .....
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140330/a3a50e97/attachment.html>