--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on March 2014 ---
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>