--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] gcc+cpp+Frama-C et les const



> gcc rejects but Frama-C accepts
>
>const int x=4;
>void f1()
>{const int *p;
>p = &x;
>*p = x + 1;
>}
>
>gcc warns but Frama-C accepts:
>const int x=4;
>void f1()
>{int *p;
>p = &x;
>*p = x + 1;
>}

That's right.

There are already a lot of great tools for checking this.

Frama-C won't replace your favorite lint checker, it'll add to it.
Put Frama-C right next to your lint checker and use them together.

Pascal

PS: Or, if there is no available program that checks exactly
the syntactic rules that you want, you can implement them
as a custom Frama-C plug-in, too.