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

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