diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6dafa681fcd42e4ca6f3091ef20bf617af091759
--- /dev/null
+++ b/doc/userman/user-acsl.tex
@@ -0,0 +1,23 @@
+\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:
diff --git a/doc/userman/userman.tex b/doc/userman/userman.tex
index bae73751949358cd1ed3de20751658cbbde76b83..2a85088030b6064d1c025c47a3c0b8390fb55213 100644
--- a/doc/userman/userman.tex
+++ b/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}
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 7f9c9a0f55790cea8ea4b6d303b3d45816d869ec..b891cf1c4c41f52f30f129764c8719be7f9bb454 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/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: