--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"



Hello David,

2013/9/12 David <abiao.yang at gmail.com>:
> I was wondering whether i could pre-process c file by include frama-c
> library without -nostdinc flag, i.e. using frama-c share library along with
> including system headers by the following command :
> gcc -C -E -I/usr/local/share/frama-c/libc -I. test.c

I don't think so. For me this is complicated (a system header might
use another system header the defines a symbol identical to one in
Frama-C's header, even if at first sight both first level included
files are different) and risky (you might think that a symbol is
defined by a system header while in fact it is defined by a Frama-C
one, or vice versa).

It is probably better to use only Frama-C headers, maybe augmented by
copied/pasted and annotated version of system ones if Frama-C headers
are lacking some features.

Best regards,
david