--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on May 2011 ---
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>