--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2010 ---
Hi Thank you, now it woks better. But now I stumbled on a other problem How can we make it working with this? extern volatile PORTABSTR _PORTAB @(REG_BASE + 0x00000000); :) Is it possible? best regards, Patrik On 2.6.2010 17:27, Pascal Cuoq wrote: >> 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > >