From b12b655395aac060adb9628d62f236b0a27a0ad3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 14 Oct 2020 10:26:37 +0200
Subject: [PATCH] [wp] cross referencing in manual
---
src/plugins/wp/doc/manual/wp_logic.tex | 1 +
src/plugins/wp/doc/manual/wp_plugin.tex | 12 ++++++++----
2 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_logic.tex b/src/plugins/wp/doc/manual/wp_logic.tex
index b51bb2e7789..83218a58bcd 100644
--- a/src/plugins/wp/doc/manual/wp_logic.tex
+++ b/src/plugins/wp/doc/manual/wp_logic.tex
@@ -180,6 +180,7 @@ This optimization is not activated by default, since the non-aliasing
assumptions at call sites are sometimes irrelevant.
\section{Mixed models hypotheses}
+\label{wp-model-hypotheses}
For the previously presented \textsf{Ref} model, but also for the
\textsf{Typed}, and \textsf{Caveat} models presented later, WP lists
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 8398488c919..d72e45d025b 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -823,13 +823,17 @@ The available \textsf{WP} command-line options related to model selection are:
makes the \textsf{WP} emitting a warning on each volatile access.
\item[\tt -wp-(no)-warn-memory-model] this option (de)activate the
warnings about memory model hypotheses
- for the generated proof obligations. For each model supporting this feature, and each concerned function,
+ for the generated proof obligations, as described in Section~\ref{wp-model-hypotheses}.
+ For each model supporting this feature, and each concerned function,
an \textsf{ACSL} specification is printed on output.
Currently, only the \texttt{Caveat}, \texttt{Typed} and \texttt{Ref} memory models support
- this feature.
+ this feature. See also experimental option below.
\item[\tt -wp-(no)-check-memory-model] this \emph{experimental} option generates
- the hypotheses listed by the option \texttt{-wp-warn-memory-model} as ACSL contracts and
- asks WP to verify them. Disabled by default.
+ ACSL contracts for the selected memory model hypotheses, as described
+ in Section~\ref{wp-model-hypotheses} and listed by option
+ \texttt{-wp-warn-memory-model}.
+ Hence, the memory model hypothes are exposed to \textsf{WP} and other plugins.
+ Disabled by default.
\end{description}
\subsection{Computation Strategy}
--
GitLab