--- layout: fc_discuss_archives title: Message 28 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



Hi,

I started using the WP plugin of frama-c recently and have been quite impressed
by the results.

I have been able to successfully test it on some basic examples, but I'm
now stuck with I/O. I read in the FAQ that I should specify the path to
the annotated standard headers that are provided with frama-c, so as to have
annotations for functions in the standard library.

I use WP like this:

$ frama-c -cpp-extra-args="-I`frama-c -print-path`/libc" -wp -wp-verbose 0 -wp-rte -wp-par 4 -wp-proof alt-ergo example.c -then -report

and I stumbled on the following error:

[..]/frama-c/libc/stdio.h:166:[kernel] user error: can not assign part of a formal parameter: arg in annotation.

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, but I don't see
how to check code that uses I/O functions.
Is it possible with WP? And if so, how can I do it?
Any help would be greatly appreciated.

Sincerely,

-- 
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/1063b506/attachment.pgp>