Your system headers contain non-standard syntax extensions that are not supported by Frama-C. This is normal, as the headers are often provided as part of a complete package with the compiler, so the headers and the compiler only need to work together, not to work with all the other programs that take C source code as input.
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
location can be obtained from Frama-C with the option -print-share-path
.
All in all, on a Unix system, it may look like:
frama-c -cpp-extra-args=-nostdinc -cpp-extra-args=-I`frama-c -print-share-path`/libc .....
Doing the same thing with Windows and MinGW follows the same idea but sometimes involves extra trouble due to the perpetual ambiguity between \
and /
as directory separators.
Recently, Frank Dordowsky has been having trouble with using a very new GCC version to pre-process C files for Frama-C. That was only when using -pp-annot
, but in any case, the solution was to switch to Clang as pre-processor.