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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 24 May 2011 17:07:21 +0200
  • In-reply-to: <20110524144910.GA8848@Nimbus>
  • References: <20110524144910.GA8848@Nimbus>
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