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] gcc+cpp+Frama-C et les const

  • Subject: [Frama-c-discuss] gcc+cpp+Frama-C et les const
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Thu, 30 Apr 2009 23:37:39 +0200
  • References: <49FA1559.4090801@dassault-aviation.fr>
> 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.