--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on December 2013 ---
Hi all, I just started with the wp plugin. I was trying out the -wp-prover options, as listed in its help manual: -wp-prover <dp,...> Submit proof obligations to external prover(s): - 'none' to skip provers Directly supported provers: - 'alt-ergo' (default) - 'altgr-ergo' (gui) - 'coq', 'coqide' (see also -wp-script) - 'why3:<dp>' or '<dp>' (why3 prover, see -wp-detect) - 'why3ide' (why3 gui) I'd like to try the last two options. the demo file, max.c, is attached. When I use why3ide option, I got the following output: ----------------------------------------------------------------------------- $ frama-c -wp -pp-annot -wp-prover why3ide max.c [kernel] preprocessing with "gcc -C -E -I. -dD src/max.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] Goal typed_max_post : trivial [wp] Goal typed_max_post_2 : trivial [wp] Goal typed_max_assert : trivial ------------------------------------------------------------------------------ why3IDE did not show up. It seems that all VCs are proved already, right? is there a way to display the why3IDE interface using wp? Thanks! cheers xiao-lei -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131209/d4b145cb/attachment-0001.html> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: max.c URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131209/d4b145cb/attachment-0001.c>