From 5984984fc9b71f1c1e5e2bd82a87a9c1f2a08616 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 13 Oct 2022 18:24:30 +0200
Subject: [PATCH] [doc] start moving documentation of @calls from WP to userman

---
 doc/userman/user-acsl.tex               | 23 +++++++++++++++++++++++
 doc/userman/userman.tex                 |  1 +
 src/plugins/wp/doc/manual/wp_plugin.tex | 10 +++++-----
 3 files changed, 29 insertions(+), 5 deletions(-)
 create mode 100644 doc/userman/user-acsl.tex

diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
new file mode 100644
index 00000000000..6dafa681fcd
--- /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 bae73751949..2a85088030b 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 7f9c9a0f557..b891cf1c4c4 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:
 
-- 
GitLab