Commit 0f66137b authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp/doc] Document model hypotheses

parent 381b38d4
......@@ -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")
......
......@@ -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.
......@@ -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}.
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment