From b2f768894bf424bc158be77f2fee5f911ce566cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Jan 2024 11:16:22 +0100
Subject: [PATCH] [wp] doc reformulations
---
src/plugins/wp/doc/manual/wp_plugin.tex | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index b54f270dac6..8c6f6ae198d 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1508,10 +1508,12 @@ To enable counter examples generation by \textsf{WP} you shall use
\verb+-wp-counter-examples+ option. Then, for each selected solver that has a
counter-examples variant, this variant will be used instead and counter-examples
will be asked to the solver in case of unknown result. Notice that you can also
-use counter-examples solvers \emph{without} asking for counter-examples, by
-using \verb+-wp-no-counter-examples+, which is the default. Notice that
-solvers variants with counter-examples support are generally a bit slower than
-their original version.
+use counter-examples solvers \emph{without} asking for counter-examples. For
+instance, with option \verb+-wp-prover cvc4-ce+, \textsf{WP} will use this
+version of the prover, even if counter examples is not active; the prover will
+not be asked to report models, unless counter examples \emph{is}
+activate. Notice that solvers variants with counter-examples support are
+generally a bit slower than their original version.
A proof obligation for which a counter-example has been generated is reported by
\textsf{WP} by the string \verb+"(Model)"+ after its proof status. For instance:
@@ -1571,8 +1573,9 @@ general syntax for the annotation is:
\]
Probes are normalized by \textsf{Qed} during simplification of proof obligations
-by \textsf{WP}. Their (simplified) term definitions are also reported when
-printing proof obligations. For instance:
+by \textsf{WP}. Their (simplified) term definitions are reported when printing
+proof obligations, and their model values are reported when printing proof
+results, when available. For instance:
\begin{shell}
# frama-c [...] -wp-status
--
GitLab