From 9b8dc476d16245abc4624ed84d8866d847397063 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 16 Sep 2019 16:09:24 +0200
Subject: [PATCH] [WP/Doc] Removes unexisting options
---
src/plugins/wp/doc/manual/wp_plugin.tex | 42 +++----------------------
1 file changed, 5 insertions(+), 37 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 10c1a2f55dc..5431caaf077 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -839,14 +839,6 @@ The available \textsf{WP} command-line options related to model selection are:
in \textsf{ACSL} contracts to ensure type-checking but are related to identity-casts
from the code. The option is \texttt{off} by default.
-\item[\tt -wp-bool-range] experimental support for \verb+_Bool+ range. This option assumes
- there is no \emph{trap representations}
- in considering valid the related assertions generated by \texttt{-wp-rte} (those tagged with \texttt{bool\_value:}).
- Hence, integer values with boolean type are
- either equal to \verb+0+ or \verb+1+. Actually, the only way to forge other values
- is \emph{via} union types and heterogeneous pointer casts, which is currently not allowed
- in the memory models of \textsf{WP}.
-
\item[\tt -wp-literals] exports the contents of string literals
to provers (default: \texttt{no}).
\item[\tt -wp-extern-arrays] gives an arbitrary large size to arrays
@@ -861,6 +853,7 @@ The available \textsf{WP} command-line options related to model selection are:
\texttt{ref}: & the variable is a constant pointer and is modeled by the \texttt{Ref}.\\
\texttt{context}: & the variable is initially non-aliased and uses a fresh global in \texttt{Typed}.\\
\end{tabular}
+\item[\tt -wp-(no)-alias-init] Use initializers for aliasing propagation (default is: yes).
\item[\tt -wp-(no)-volatile] this option (de)activate the correct handling of
volatile access. By default, accessing a volatile l-value returns an undefined
value, and writing to a volatile l-value is modeled like an \textsf{ACSL} assigns clause.
@@ -1029,7 +1022,7 @@ Support for \textsf{Why-3 IDE} is no longer provided.
Default is \verb+5s+.
\item[\tt -wp-steps <$n$>] sets the maximal number of prover
steps. This can be used as a machine-independent alternative to timeout.
-\item[\tt -wp-why-opt='options,...'] provides additional options to the
+\item[\tt -wp-why3-opt='options,...'] provides additional options to the
\verb+why3+ command.
\item[\tt -wp-why3='<cmd>'] overrides the path to the \verb+why3+ command.
\end{description}
@@ -1102,27 +1095,6 @@ procedures. This support is provided for \textsf{Alt-Ergo},
\item[\tt -wp-share <dir>] modifies the default directory where
resources are found. This option can be useful for running a modified or
patched distribution of \textsf{WP}.
-% \item[\tt -wp-include <dir,\ldots,++sharedir>] (\textbf{deprecated} use driver instead) sets the directories where external
-% libraries and driver files are looked for.
-% The current directory (implicitly added to that list) is always looked up
-% first.
-% Relative directory names are relative to the current directory except
-% for names prefixed by the characters \texttt{++}.
-% In such a name, the directory is relative to the main \texttt{FRAMAC\_SHARE}
-% directory.
-% \item[\tt -wp-alt-ergo-lib <f,\ldots>] (\textbf{deprecated} use altergo.file
-% in driver instead) looks for \textsf{Alt-Ergo}
-% library files \verb+"f.mlw"+ and inlines them into the proof
-% obligation files for \textsf{Alt-Ergo}.
-% \item[\tt -wp-coq-lib <f,\ldots>] (\textbf{deprecated} use coq.file
-% in driver instead) looks for \textsf{Coq} files
-% \verb+"f.v"+ or \verb+"f.vo"+. If
-% \verb+"f.vo"+ is not found, then \textsf{WP} copies \verb+"f.v"+
-% into its working directory (see option
-% \texttt{-wp-out}) and compiles it locally.
-% \item[\tt -wp-why-lib <f,\ldots>] (\textbf{deprecated} use why3.file in driver instead) looks for \textsf{Why3} library file
-% \verb+"f.why"+ and opens the library \verb+"f.F"+ for the proving the
-% goals.
\end{description}
\subsection{Linking \textsf{ACSL} Symbols to External Libraries}
@@ -1136,8 +1108,7 @@ if any, are not exported by \textsf{WP}s.
External linkage is specified in \emph{driver files}. It is possible
to load one or several drivers with the following \textsf{WP} plug-in option:
\begin{description}
-\item[\tt -wp-driver <file,\ldots>] load specified driver files,
- replacing deprecated features from section~\ref{prooflibs}.
+\item[\tt -wp-driver <file,\ldots>] load specified driver files.
\end{description}
@@ -1280,11 +1251,8 @@ interactively or incrementally, it is often the case where most proof obligation
from one \textsf{WP} execution to the other. To reduce this costs, a cache of prover results can be used
and stored in your session.
-The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo}
-and \textsf{Coq} provers -- although proof scripts works with both.
-There are different ways of using the cache, depending on your precise needs.
-
-The \textsf{WP} options to control session and cache are \verb+-wp-session+ and \verb+-wp-cache+, as documented below:
+The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers. There are different ways of using the cache, depending on your precise needs.
+The main option to control cache usage is \verb+-wp-cache+, documented below:
\begin{description}
\item[\tt -wp-session <dir>] select the directory where cached results and proof scripts
--
GitLab