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