From ecd2f1f2110d1f3adc8aac0ff2195c17194cc2a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 28 Jan 2019 14:43:10 +0100
Subject: [PATCH] [WP] update doc & changelog
---
src/plugins/wp/Changelog | 2 ++
src/plugins/wp/doc/manual/wp_intro.tex | 15 +++++++++------
2 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 405600b3263..844b5b50097 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
# <Prover>: prover
###############################################################################
+- Wp [2019/01/28] New floating-point model
+
######################
Plugin WP 18.0 (Argon)
######################
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index da74357a7b9..1e3c5e076a6 100644
--- a/src/plugins/wp/doc/manual/wp_intro.tex
+++ b/src/plugins/wp/doc/manual/wp_intro.tex
@@ -340,12 +340,15 @@ For tackling this complexity, the \textsf{WP} plug-in relies on several
or \texttt{-wp-rte} will generate a warning if some annotation might be not
generated.
-\item[Float Model:] floating-point operations are \emph{defined} to be
- the mathematical ones \emph{with} a rounding operation. This is fully
- consistent with the \textsf{IEEE} semantics. Most automated provers
- are not able to discharge the generated proof obligations. Special
- support for the \textsf{Gappa} theorem prover is available through
- \textsf{Why3}.
+\item[Float Model:] floating-point values are represent in a special
+ theory with dedicated operations over \texttt{float} and \texttt{double}
+ values and conversion from and to their \texttt{real} representation \emph{via}
+ rounding, as defined by the \textsc{C/ACSL} semantics.
+
+ Although correct with respect to the \textsc{IEEE} specifications, this
+ model still provides very little support for proving properties with automated
+ provers. You may add additional properties using \emph{drivers}
+ as explained later.
\item[Real Model:] floating-point operations are \emph{transformed} on
reals, with \emph{no} rounding. This is completely unsound with
--
GitLab