From 0f66137b726c8615e1c267f76a5b7cf4c72e8048 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 12 Oct 2020 16:39:44 +0200
Subject: [PATCH] [wp/doc] Document model hypotheses
---
src/plugins/wp/Changelog | 4 +--
src/plugins/wp/doc/manual/wp_caveat.tex | 2 +-
src/plugins/wp/doc/manual/wp_logic.tex | 45 +++++++++++++++++++++++++
src/plugins/wp/doc/manual/wp_plugin.tex | 3 ++
4 files changed, 51 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 74f06206e05..44868a143cb 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -34,8 +34,8 @@ Plugin WP <next-release>
- WP [2020-09-21] Added support for Why3 Coq interactive prover
- WP [2020-09-21] New option -wp-interactive <mode>
- WP [2020-09-21] New option -wp-interactive-timeout <seconds>
-- WP [2020-09-17] New experimental option: -wp-check-model-hypotheses
- Generates requires in contracts for model hypotheses
+- WP [2020-09-17] New experimental option: -wp-check-memory-model
+ Insert function contracts for model hypotheses
- WP [2020-09-17] Hypotheses: assigned memory locations
- WP [2020-09-11] Support for generalized @check ACSL annotations
- WP [2020-07-06] Removed debug keys "no-xxx-info" (subsumed by "shell")
diff --git a/src/plugins/wp/doc/manual/wp_caveat.tex b/src/plugins/wp/doc/manual/wp_caveat.tex
index 9223f9d67df..6e7afa77c06 100644
--- a/src/plugins/wp/doc/manual/wp_caveat.tex
+++ b/src/plugins/wp/doc/manual/wp_caveat.tex
@@ -34,5 +34,5 @@ the user \emph{must} check by manual code review that no aliases are
introduced \emph{via} pointers passed to formal parameters at call sites.
However, \textsf{WP} warns about the implicit separation hypotheses required by
-the memory model \textit{via} the \texttt{-wp-warn-separation} option, set
+the memory model \textit{via} the \texttt{-wp-warn-memory-model} option, set
by default.
diff --git a/src/plugins/wp/doc/manual/wp_logic.tex b/src/plugins/wp/doc/manual/wp_logic.tex
index fb061182052..b51bb2e7789 100644
--- a/src/plugins/wp/doc/manual/wp_logic.tex
+++ b/src/plugins/wp/doc/manual/wp_logic.tex
@@ -178,3 +178,48 @@ detected variables are then assigned to the Hoare memory model.
This optimization is not activated by default, since the non-aliasing
assumptions at call sites are sometimes irrelevant.
+
+\section{Mixed models hypotheses}
+
+For the previously presented \textsf{Ref} model, but also for the
+\textsf{Typed}, and \textsf{Caveat} models presented later, WP lists
+the separation and validity hypotheses associated to the choice that
+it make of dispatching each pointer and variable either to the
+\lstinline{Hoare} or to the model $\cal{M}$ used for the heap.
+
+Thus, in addition to user-defined function \lstinline{requires}, WP
+also states as \lstinline{requires} that:
+
+\begin{itemize}
+\item \lstinline{Hoare} variables are separated from each other,
+\item \lstinline{Hoare} variables are separated from the locations in $\cal{M}$,
+\item references are valid memory locations,
+\item locations assigned via a pointer are separated from \lstinline{Hoare}
+ variables whose address is not taken by the function (including via
+ its contract).
+\end{itemize}
+
+Furthermore, the function must ensure that:
+
+\begin{itemize}
+\item locations assigned via a pointer (including returned value when
+ it is a pointer) are separated from \lstinline{Hoare} variables whose address
+ is not taken by the function (including via its contract),
+\item pointers assigned by the function (including returned value when
+ it is a pointer) are separated from function parameters and \lstinline{Hoare}
+ variables whose address is not taken by the function (including via
+ its contract).
+\end{itemize}
+
+In order to precisely generate these hypotheses, WP needs precise
+\lstinline{assigns} specification. In particular each function under
+verification and all its callees needs an \lstinline{assigns} specification.
+Furthermore, if the function assigns or returns a pointer, WP needs
+a correct \lstinline{\from} specification. If the specification is
+incomplete, a warning \lstinline{wp:pedantic-assigns} is triggered.
+Note that WP does not verify that the \lstinline{\from} is correct.
+
+The hypotheses are displayed when the option
+\lstinline{-wp-warn-memory-model} is enable (it is enabled by default).
+They can be verified by WP using the experimental option
+\lstinline{-wp-check-memory-model}.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index baabcb0c126..8398488c919 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -827,6 +827,9 @@ The available \textsf{WP} command-line options related to model selection are:
an \textsf{ACSL} specification is printed on output.
Currently, only the \texttt{Caveat}, \texttt{Typed} and \texttt{Ref} memory models support
this feature.
+\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.
\end{description}
\subsection{Computation Strategy}
--
GitLab