[wp/doc] Document terminates support

src/plugins/wp/Changelog

@@ -27,9 +27,9 @@ Plugin WP <next-release>
 - WP          [2021-10-25] Removes -wp-overflows option (unsound)
 - WP          [2021-06-11] Adds an experimental support of "terminates" clauses.
                            Adds the options -wp-declaration-terminate and
-                          -wp-frama-c-stdlib to claims that external functions
+                           -wp-frama-c-stdlib to claim that external functions
                            terminates.
-                           Adds -wp-declarations-terminate option to claims that
+                           Adds -wp-definitions-terminate option to claim that
                            defined function terminates.
                            Adds -wp-variant-with-terminates to verify loop
                            variants under the termination hypothesis.

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -986,7 +986,7 @@ weakest precondition calculus.
   \texttt{terminates \textbackslash{}false}, any loop variant proof is trivial)
   (default is: \texttt{no}).
 \item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
-  thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
+  thanks to the dedicated code annotation \verb+@calls f1,...,fn+ (default is: \texttt{yes}).
 \end{description}
 
 \subsubsection{ACSL extension \texttt{@calls}}
@@ -1018,6 +1018,100 @@ These annotations split post-conditions to the dynamic call into two sub-goals:
 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}}
+
+In ACSL, a function can be specified to terminate some condition \verb+P+ holds
+in precondition.
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+/*@ terminates P ; */
+void function(void){
+  ...
+}
+\end{lstlisting}
+
+If terminates verification is active, WP collects all function calls and loops
+and generate different VCs.
+
+\paragraph{Loop variants.} When a loop has a variant, no particular verification
+is generated for termination. However, if \verb+-wp-variant-with-terminates+ is
+active, the variant is verified only if \verb+P+ holds at this program point.
+Basically, "the variant has to hold only if the function has to terminate". For
+example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i >= 0 ;
+void positive(int i){
+  /*@ loop invariant \at(i, Pre) >= 0 ==> 0 <= i <= \at(i, Pre) ;
+      loop assigns i ;
+      loop variant i ; // verified when i >= 0 at pre
+  */
+  while(i) --i;
+}
+\end{lstlisting}
+
+Note that it means that when one specifies \verb+terminates \false+ any loop
+variant trivially holds.
+
+When a loop does not have a variant, WP checks that the loop is unreachable
+when \verb+P+ holds in precondition, which means "a loop is allowed not
+terminating when the function does not have to". For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i >= 0 ;
+void function(int i){
+  if(i < 0){
+    // note i >= 0 && i < 0 ==> \false
+    while(1);
+  }
+}
+\end{lstlisting}
+
+\paragraph{Function call.} When a function \verb+f+ that terminates when
+\verb+P+, calls a function \verb+g+ that terminates when \verb+Q+, WP tries to
+prove that \verb+P@pre ==> Q@call-point+, "when \verb+f+ terminates, we must
+call \verb+g+ in a way that guarantees that it also terminates". Note that it
+means that if the function under verification must terminate, any call to a
+non terminating function must be unreachable. For example:
+
+\begin{lstlisting}[language=c, alsolanguage=acsl]
+//@ terminates i <= 0 ;
+void f(int i) ;
+
+//@ terminates i >  0 ;
+void g(int i) ;
+
+/*@ requires i <= 0 ;
+    terminates \true ; */
+void caller(int i){
+  f(i); // succeeds
+  g(i); // fails, thus global termination is not proved
+}
+\end{lstlisting}
+
+When a called function does not have a terminates specification, WP assumes one
+as specified by the options:
+
+\begin{itemize}
+\item \verb+-wp-frama-c-stdlib-terminate+,
+\item \verb+-wp-declarations-terminate+,
+\item \verb+-wp-definitions-terminate+.
+\end{itemize}
+
+\paragraph{(Mutually) recursive function.} When a function is in a recursive
+cluster (as defined in the ACSL manual) and must 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 such a clause
+is not supported.
+
+\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 behave
+as explained before for function calls. If this specification is not available,
+WP considers that the pointed function might call the function under
+verification and thus that it is part of a recursive cluster and must provide
+a \verb+decreases+ clause.
+
 \subsection{Smoke Tests}
 
 During modular deductive verification, inconsistencies in function requirements