From 5c5bd9d6fd9381288030bc40a8b1f17787b56c63 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 14 Jan 2022 10:41:49 +0100
Subject: [PATCH] [wp/doc] supported decreases
---
src/plugins/wp/Changelog | 7 +++++--
src/plugins/wp/doc/manual/wp_intro.tex | 11 +++++++----
src/plugins/wp/doc/manual/wp_plugin.tex | 4 ++--
3 files changed, 14 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index c43afbaba78..3bc5855e346 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,10 +24,13 @@
Plugin WP <next-release>
########################
+- WP [2022-01-10] Supported general variant measure
+- WP [2022-01-10] Supported decreases clause
- TIP [2022-01-10] New tactic Mod-Mask: rewrite bitmask into/from modulo
- TIP [2022-01-05] New tactic Clear: remove hypothesis
--* WP [2022-01-05] Fix loop invariant order
-- WP [2022-01-05] Weaken check loop invariant
+-* WP [2022-01-05] Fixed loop invariant order
+- WP [2022-01-05] Weakened loop invariant verification (in particular
+ for check loop invariant)
- TIP [2021-11-30] Extended Split tactic: can split in hypotheses, can
split conjunctions into multiple hypotheses.
- WP [2021-11-08] Removed legacy WP engine and option -wp-legacy
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index efc03f16a64..114c37f60c4 100644
--- a/src/plugins/wp/doc/manual/wp_intro.tex
+++ b/src/plugins/wp/doc/manual/wp_intro.tex
@@ -198,10 +198,13 @@ speaking, the \emph{weakest precondition} of property $Q$ through
statement $\mathit{stmt}$ should also ensure termination and execution without
runtime errors.
-The proof obligations generated by \textsf{WP} do not entail
-systematic termination, unless you systematically specify and validate
-loop variant \textsf{ACSL} annotations. Nevertheless, \texttt{exit} behaviors of a
-function are correctly handled by \textsf{WP}.
+When the \verb+terminates+ clause is specified in function contracts,
+\textsf{WP} generates proof
+obligations to make sure that all loops have loop variants and that all function
+calls terminate whenever necessary (thus requiring \verb+decreases+ clause for
+recursive functions). Furthermore, \texttt{exit} behaviors of a function are
+correctly handled by \textsf{WP}. More details about proof of termination in
+\textsf{WP} are provided in Section~\ref{ss-sec:plugin-terminates}.
Regarding runtime errors, the proof obligations generated by
\textsf{WP} assume your program never raises any of them. As
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 1a60d74bc1d..478cdf7d398 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1050,6 +1050,7 @@ a second for the call to \verb+f2+. A last goal is generated at the call
site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.
\subsubsection{Proof of \texttt{@terminates}}
+\label{ss-sec:plugin-terminates}
In ACSL, a function can be specified to terminate when some condition \verb+P+ holds
in pre-condition.
@@ -1132,8 +1133,7 @@ as specified by the options:
recursive cluster (as defined in the ACSL manual) and shall terminate, WP checks that a
\verb+decreases+ clause is available for the function. Proving that existing
recursive calls might be unreachable is delegated to the proof of the
-\verb+decreases+ clause. Note however that, currenlty, the proof of \verb+decreases+
-clauses is not supported yet.
+\verb+decreases+ clause.
\paragraph{Function pointers. } On a call via a function pointer, WP checks that
a \verb+@calls+ is specified for this function pointer. If so, WP just behaves
--
GitLab