--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Usage of the WP plugin with standard lib



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>