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] Usage of the WP plugin with standard lib

  • Subject: [Frama-c-discuss] Usage of the WP plugin with standard lib
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 24 May 2011 17:30:23 +0200
  • In-reply-to: <BANLkTi=avqkC4xy1wiVX6_c=Q_mihVc1LA@mail.gmail.com>
  • References: <20110524144910.GA8848@Nimbus> <BANLkTi=avqkC4xy1wiVX6_c=Q_mihVc1LA@mail.gmail.com>
Hello Pascal,

2011/5/24 Pascal Cuoq <pascal.cuoq at gmail.com>:
> I should point out that the substitution standard headers
> provided with Frama-C have received very little testing, as you
> have noticed already.

I am probably not the first one to fall in that trap. As others, I
assumed headers provided in libc/ directory of Frama-C could be used
without any further question.

I have no issue that is not the case, however a prominent
LIBC_VALIDITY.txt file or similar telling which headers are safe for
use with Frama-C (if any) would be useful.

Best regards,
david