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: pini at ethernium.org (Pierre-Nicolas Clauss)
  • Date: Tue, 24 May 2011 16:49:10 +0200
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>