Merge branch 'doc/wp/supported-decreases' into 'master'

[wp/doc] supported decreases/generalized measures

See merge request frama-c/frama-c!3531

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

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

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