From 5996b6757c926fb380f63e64d35626132d9cfa57 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 24 Jan 2022 15:57:40 +0100
Subject: [PATCH] [wp/doc] Remove some alt-ergo related driver doc
---
src/plugins/wp/doc/manual/wp_builtins.tex | 24 +++++++++++------------
1 file changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_builtins.tex b/src/plugins/wp/doc/manual/wp_builtins.tex
index c5df277c89c..4454601c8d3 100644
--- a/src/plugins/wp/doc/manual/wp_builtins.tex
+++ b/src/plugins/wp/doc/manual/wp_builtins.tex
@@ -141,7 +141,7 @@ Moreover, the following lemmas are added to complement the reference ones:
\vskip 1em
\hrule
\label{builtin-exp-log}
-\paragraph{$\builtin{exp}(x)$, $\builtin{log}(x)$ and $\builtin{log10}(x)$} are declared
+\paragraph{$\builtin{exp}(x)$, $\builtin{log}(x)$ and $\builtin{log10}(x)$} are declared
to be injective, monotonically increasing and are associated with the following simplifiers:
\[
\begin{array}{rcl@{\quad}l}
@@ -188,14 +188,14 @@ imported from \textsf{Why-3}.
\vskip 1em
\hrule
\label{builtin-trigo}
-\paragraph{$\builtin{sin}(x)$, $\builtin{cos}(x)$ and $\builtin{tan}(x)$} trigonometric
+\paragraph{$\builtin{sin}(x)$, $\builtin{cos}(x)$ and $\builtin{tan}(x)$} trigonometric
operations. Useful lemmas are already defined in the reference implementation from
\textsf{Why-3} library.
\label{builtin-arctrigo}
-\paragraph{$\builtin{asin}(x)$, $\builtin{acos}(x)$ and $\builtin{atan}(x)$} trigonometric
+\paragraph{$\builtin{asin}(x)$, $\builtin{acos}(x)$ and $\builtin{atan}(x)$} trigonometric
operations. Except definition of $\builtin{atan}$ which is available from reference,
-definition for arc-$\builtin{sin}$ and arc-$\builtin{cos}$ have been added. Moreover,
+definition for arc-$\builtin{sin}$ and arc-$\builtin{cos}$ have been added. Moreover,
all the arc-trigonometric operations are declared to be injective. In addition, the
following simplifiers are also registered:
@@ -216,7 +216,7 @@ and are actually provided by custom extensions installed in the \textsf{WP} shar
\vskip 1em
\hrule
\label{builtin-hyperbolic}
-\paragraph{$\builtin{sinh}(x)$, $\builtin{cosh}(x)$ and $\builtin{tanh}(x)$} trigonometric
+\paragraph{$\builtin{sinh}(x)$, $\builtin{cosh}(x)$ and $\builtin{tanh}(x)$} trigonometric
operations. Useful lemmas are already defined in the reference implementation from
\textsf{Why-3} library.
@@ -256,21 +256,21 @@ Since all the builtin symbols of \textsf{ACSL} are actually linked to the standa
of \textsf{Why-3}, any user theory also referring to the standard symbols can be added to the proof
environment by using option \verb+-wp-why-lib 'file...'+.
-Otherwise, a driver shall be written. For instance, the additional lemma regarding $\builtin{exp}$
-p.\pageref{builtin-hyperbolic} for \textsf{Alt-Ergo} is simply defined in the following way:
+Otherwise, a driver can be written. For instance, the additional lemma regarding $\builtin{exp}$
+p.\pageref{builtin-hyperbolic} for \textsf{Why3} is simply defined in the following way:
-\begin{logs}
+\begin{logs}
// MyExp.mlw file
- axiom exp_pos : (forall x:real. (0.0 < exp(x)))
+ axiom exp_pos : forall x:real. (0.0 < exp(x))
\end{logs}
-Of course, this piece of \textsf{Alt-Ergo} input file must be integrated after the symbol
+Of course, this piece of \textsf{Why3} input file must be integrated after the symbol
\verb+exp+ has been defined. The corresponding driver is then:
\begin{logs}
// MyExp.driver file
library exponential:
- ergo.file += "MyExp.mlw" ;
+ why3.file += "MyExp.mlw" ;
\end{logs}
Such a driver, once loaded with option \verb+-wp-driver+, instructs \textsf{Frama-C/WP} to
@@ -278,5 +278,5 @@ append your extension file to the other necessary resources for library \verb+"e
which the logic ACSL builtin \verb+\exp+ belongs to.
The file \verb+share/wp/wp.driver+ located into the shared directory of \textsf{Frama-C},
-and the associated files in sub-directories \verb+share/wp/ergo+ and \verb+share/wp/why3+ shall provide
+and the associated files in sub-directory \verb+share/wp/why3+ shall provide
all the necessary hints for extending the capabilities of \textsf{Frama-C/WP} in a similar way.
--
GitLab