--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2011 ---
Hello, > where stdio.h:166 is the following: > > 166 ?/*@ assigns arg \from format[..], *stream; */ > 167 ?int vfscanf(FILE * restrict stream, > 168 ? ? ? const char * restrict format, > 169 ? ? ? va_list arg); > > The error message seems consistent with the annotation, 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. > but I don't see > how to check code that uses I/O functions. > Is it possible with WP? 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. I had to do something similar in a different context and I think the example speaks for itself although it's for a different plug-in: I should point out that the substitution standard headers provided with Frama-C have received very little testing, as you have noticed already. Pascal