--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unknows Pragma



> Use frama-c with the option:
> -cpp-command "gcc -C -E -I. - < ?%1 | gr > %2"

Having eaten my own dogfood[1], I found that

-cpp-command "gcc -C -E -I. %1 | gr > %2"

gives much better results. With this syntax, gcc still
sends the pre-processed file to its standard output,
but since the name of the file is known, inserted in
the pre-processed file, and taken advantage of by
Frama-C, you get messages such as:

[value] computing for function printf <-sizeof_enum1.
        Called from tests/misc/enum2.c:25.

instead of:

[value] computing for function printf <-sizeof_enum1.
        Called from <stdin>:25.

Pascal

[1] http://en.wikipedia.org/wiki/Eating_your_own_dog_food