Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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