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] Frama-c-discuss Digest, Vol 40, Issue 3

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 40, Issue 3
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 14 Sep 2011 16:57:50 +0200
  • In-reply-to: <CAL2=XacWtXKNvKLDRhxrCS0yPGjMWHSoMNVMj+8cDFQsWyUSNQ@mail.gmail.com>
  • References: <mailman.61.1315994505.11897.frama-c-discuss@lists.gforge.inria.fr> <CAL2=XacWtXKNvKLDRhxrCS0yPGjMWHSoMNVMj+8cDFQsWyUSNQ@mail.gmail.com>
Le 14/09/2011 16:18, haihao shen a ?crit :
> Thanks Pascal and Julien.
> Some of research work showed that macro may hidden some bugs, so
> sometimes, we still need to do static analysis based on the purely
> source code I think.

Macros may hidden bugs to developers but, as far I know, inlining macros 
(as preprocessing does) does not remove bugs: if you use a correct 
preprocessor and next a correct static analysis tool on the resulting 
file, you do find bugs introduced by misused macros. The major drawback 
of this approach is that the exact origin of the bug may be more 
difficult to identify for the end-user. That is one reason why you 
suggestion would be useful.

But, if the Frama-C team chooses to implement a new C preprocessor from 
scratch, it would take a huge amount of time used to reinvent the wheel 
instead of writing new static analysers which is our primary goal. Also 
it would introduce a new large and complex piece of code in Frama-C 
which could contain critical bugs impacting each end-user. That is two 
reasons why the Frama-C team chooses to not implement such a preprocessor.

Fortunatly, Frama-C is an open source and extensible platform: anyone is 
free to implement itself such a preprocessor and plug in to Frama-C. The 
Frama-C team could even provide some helps through this mailing list. 
Maybe someone reading this message would like to contribute this way :-).

--
Julien