Merge branch 'doc/wp/remove-native-coq-alt-ergo' into 'master'

[WP/Doc] Removes native support of Alt-Ergo/Coq

See merge request frama-c/frama-c!2380

src/plugins/wp/doc/manual/wp_builtins.tex

@@ -31,10 +31,6 @@ The \textsf{ACSL} built-ins supported by \textsf{Frama-C/WP} are listed in Figur
 In the table, the reference implementation of the function is given in terms of the \textsf{Why-3}
 standard library\footnote{Available online \texttt{http://why3.lri.fr/stdlib}},
 from which all the properties are automatically imported and communicated to the provers.
-For the natively supported provers \textsf{Alt-Ergo} and \textsf{Coq}, those properties are also available, even 
-if \textsf{Why-3} is not installed on your machine. They are statically installed by \textsf{Frama-C} in the 
-shared directory of \textsf{WP}%
-\footnote{Usually \texttt{/usr/local/share/frama-c/wp} ; otherwise \texttt{`frama-c -print-share-path`/wp}}.
 
 \begin{figure}[htbp]
 \begin{center}

src/plugins/wp/doc/manual/wp_intro.tex

@@ -25,7 +25,7 @@ heterogeneous casts, are involved. Moreover, \textsf{Jessie}
 operates by compiling the \textsf{C} program to \textsf{Why}, a
 solution that prevents the user from combining \textit{weakest
   precondition calculus} with other techniques, such as the
-\textsf{Value} analysis plug-in.
+\textsf{Eva} analysis plug-in.
 
 The \textsf{WP} plug-in has been designed with cooperation in
 mind. That is, you may use \textsf{WP} for proving some annotations of
@@ -39,9 +39,10 @@ the \textsf{WP} plug-in, the \emph{Weakest Precondition} calculus and
 \emph{Memory Models}. Then, Chapter~\ref{wp-plugin} details how to use
 and tune the plug-in within the \textsf{Frama-C}
 platform. Chapter~\ref{wp-models} provides a description for the
-included memory models. Finally, we present in
-Chapter~\ref{wp-simplifier} the simplifier module and the efficient weakest
-precondition engine implemented in the \textsf{WP} plug-in.
+included memory models. We present in Chapter~\ref{wp-simplifier} the
+simplifier module and the efficient weakest precondition engine implemented
+in the \textsf{WP} plug-in. Finally, in Chapter~\ref{wp-builtins}, we
+provide additional information on the supported ACSL built-in symbols.
 
 \clearpage
 
@@ -51,12 +52,14 @@ precondition engine implemented in the \textsf{WP} plug-in.
 %-----------------------------------------------------------------------------
 
 The \textsf{WP} plug-in is distributed with the \textsf{Frama-C}
-platform. However, you should install at least one external prover in
+platform. However, it also requires the \textsf{Why-3} platform and
+you should install at least one external prover in
 order to fulfill proof obligations. An easy choice is to install the
-\textsf{Alt-Ergo} theorem prover developed at
-\textsc{inria}\footnote{\textsf{Alt-Ergo}:
-  \url{http://alt-ergo.lri.fr}}.  See section~\ref{wp-install-provers}
-for installing other provers.
+\textsf{Alt-Ergo} theorem prover originally developed at
+\textsc{inria} and now by \textsc{OcamlPro}\footnote{\textsf{Alt-Ergo}:
+  \url{https://alt-ergo.ocamlpro.com/}}. When using the \textsf{Opam} package
+  manager, these tools are automatically installed with \textsf{Frama-C}.
+See the documentation of \textsf{Why-3} to install other provers.
 
 
 %-----------------------------------------------------------------------------
@@ -94,7 +97,7 @@ should be valid.
 By default, the \textsf{WP} plug-in does not generate any proof obligation
 for verifying the absence of runtime errors in your code. Absence of runtime errors
 can be proved with other techniques, for instance by running
-the \textsf{Value} plug-in, or by generating all the necessary annotations
+the \textsf{Eva} plug-in, or by generating all the necessary annotations
 with the \textsf{RTE} plug-in.
 
 The simple contract for the \texttt{swap} function above is not strong enough to
@@ -196,8 +199,8 @@ Regarding runtime errors, the proof obligations generated by
 \textsf{WP} assume your program never raises any of them. As
 illustrated in the short tutorial example of
 section~\ref{wp-tutorial}, you should enforce the absence of runtime
-errors on your own, for instance by running the \emph{value analysis}
-plug-in or the \emph{rte generation} one and proving the generated assertions.
+errors on your own, for instance by running the \textsf{Eva}
+plug-in or the \textsf{RTE} one and proving the generated assertions.
 
 %-----------------------------------------------------------------------------
 \section{Memory Models}
@@ -294,11 +297,11 @@ Chapter~\ref{wp-models} is dedicated to a more detailed description of
 memory models, and how the \textsf{WP} plug-in uses and \emph{combines}
 them to generate efficient proof obligations.
 
-\paragraph{Remark.}
-The original \texttt{Store} and \texttt{Runtime} memory models are no
-longer available since \textsf{WP} version \verb+0.7+ (Fluorine); the \texttt{Typed} model
-replaces the \texttt{Store} one; the \texttt{Runtime} model will be entirely
-re-implemented as \texttt{Bytes} model in some future release.
+% \paragraph{Remark.}
+% The original \texttt{Store} and \texttt{Runtime} memory models are no
+% longer available since \textsf{WP} version \verb+0.7+ (Fluorine); the \texttt{Typed} model
+% replaces the \texttt{Store} one; the \texttt{Runtime} model will be entirely
+% re-implemented as \texttt{Bytes} model in some future release.
 
 \clearpage
 \section{Arithmetic Models}
@@ -361,5 +364,5 @@ For tackling this complexity, the \textsf{WP} plug-in relies on several
 \paragraph{Remark:} with all models, there are conditions to meet for WP
 proofs to be correct. Depending on the model used and the kernel options, those conditions
 may change. WP do not generate proof obligations for runtime errors on its own. Instead, it can
-discharge the annotations generated by the Value analysis plug-in, or by the RTE plug-in.
+discharge the annotations generated by the \textsf{Eva} analysis plug-in, or by the \textsf{RTE} plug-in.
 Consider also using \textsf{-wp-rte} option.