--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2014 ---
That was a pointer to the right direction. However, the option -ffreestanding did not work. With help of a C guru at my office I found another option that did the trick: -fpreprocessed <stdc-predef.h>. My complete command now reads: frama-c -cpp-extra-args="-I `frama-c -print-share-path`/libc" -cpp-extra-args="-nostdinc" -cpp-extra-args="-fpreprocessed </path/to/stdc-predef.h>" -wp -wp-rte -pp-annot constant.c So thanks again for your help. Frank On Sun, 30 Mar 2014, Pascal Cuoq wrote: > On Sun, Mar 30, 2014 at 2:50 PM, Frank Dordowsky <frank at strato.de> wrote: > > ? ? ? ? frama-c -cpp-extra-args="-nostdinc" -cpp-extra-args="-I > `frama-c -print-share-path`/libc" -pp-annot -wp -wp-rte > constant.c > > There are no more warnings now (I skipped these in my previus > posting), but unfortunately the error remains: > > [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. > > Is there still a mistake in the command? > > > There is still something strange, which is that a header from /usr/include > finds itself included when it shouldn't. Considering the name of the file, > ?stdc-predef.h?, it may be a file that is systematically included before > every pre-processed file, and that is not disabled by -nostdinc. This is > between you and your compiler, I am afraid, but googling for ?stdc-predef.h? > produces a list of results the first entry of which is a webpage containing > the line: > > As a workaround, the?stdc-predef.h?preinclude can be disabled with the use > of - ffreestanding > > This is the page the above sentence comes > from:?http://gcc.gnu.org/gcc-4.8/porting_to.html > > It seems worth a try. > > Pascal > > > Frank Dordowsky S?ntisstr. 37 81825 M?nchen E-Mail: frank at dordowsky.de