[doc] start moving documentation of @calls from WP to userman

doc/userman/user-acsl.tex

+\chapter{\acsl extensions}
+\label{cha:acsl-extensions}
+\section{Handling indirect calls with \texttt{calls}}
+\label{acsl:calls}
+
+In order to help plug-ins support indirect calls (i.e. calls through
+a function pointer), an \acsl extension is provided. It is introduced
+by keyword \lstinline|calls| and can be placed before
+a statement with an indirect call to give the list of
+functions that may be the target of the call. As an example,
+\begin{ccode}
+/*@ calls f1, f2, ... , fn */
+*f(args);
+\end{ccode}
+indicates that the pointer \lstinline|f| can point to any one of
+\lstinline|f1|, \lstinline|f2|, ..., \lstinline|fn|.
+
+It is in particular used by the WP plug-in (see \cite{wp} for more information).
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "userman"
+%%% End:

doc/userman/userman.tex

@@ -62,6 +62,7 @@ Baudin, Mickaël Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente
 \include{user-start}
 \include{user-plugins}
 \include{user-sources}
+\include{user-acsl}
 \include{user-analysis}
 \include{user-properties}
 \include{user-services}

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

@@ -1043,11 +1043,11 @@ weakest precondition calculus.
 \subsubsection{ACSL extension \texttt{@calls}}
 \label{acsl:calls}
 
-The handling of functions pointers is done via the ACSL code annotation
-extension \verb+@calls+. For each call to a function pointer \verb+fp+
-in the instruction or block under the annotation \verb+calls f1,\ldots,fn+,
-\verb+fp+ is required to belongs to the set \verb+f1,\ldots,fn+ and
-a case analysis is performed with the contract of each provided function.
+Frama-C provides an ACSL extension \texttt{@calls} that can be written
+before an indirect call to indicate which functions can be the target
+of the pointer (see \cite{userman} for more information). Upon encountering
+such annotation, WP will perform a case analysis with the contract of
+each provided function.
 
 For example: