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

[Frama-c-discuss] Unknows Pragma



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
>
>