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: pini at ethernium.org (Pierre-Nicolas Clauss)
  • Date: Tue, 24 May 2011 17:15:40 +0200
  • In-reply-to: <BANLkTi=avqkC4xy1wiVX6_c=Q_mihVc1LA@mail.gmail.com>
  • References: <20110524144910.GA8848@Nimbus> <BANLkTi=avqkC4xy1wiVX6_c=Q_mihVc1LA@mail.gmail.com>
Le Tuesday 24 May 2011 ? 17:07:21 (+0200), Pascal Cuoq a ?crit :
> Variadic functions are outside the scope of what Frama-C
> handles well, and this time I am saying "Frama-C" because
> since no plug-in tries very hard to do something with them
> there probably are issues in the front-end itself related to
> variadic functions.
> 
> If the function is used only once, give it a non-variadic prototype
> and specification. If it is used several times with varying
> prototypes, declare and use a different function per prototype.
> You will have to specify each of these functions, and, if you wish
> to continue being able to compile and execute the program,
> to implement it with a direct call to the variadic function.
> These functions should remain outside the scope of the
> verification.

Ok, I'll go for this. As for now, I have very little code that is
impacted, so I got define a special macro (through -cpp-extra-args) that
would use specialized prototypes instead of including the standard header
file (with #ifdef/#else/#endif).

I sometimes use the same kind of tricks when running doxygen over twisted
code.

> I should point out that the substitution standard headers
> provided with Frama-C have received very little testing, as you
> have noticed already.

Ok, I'll have a look at the provided annotations to write my own prototypes
for the functions of the standard lib that I use.

Thanks for your help.


Cheers,

-- 
Pierre-Nicolas Clauss
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110524/c54b49c9/attachment.pgp>