From d8902fc02e0036c9080d25af9aa4e7e97b5b141b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 20 Aug 2019 15:59:59 +0200
Subject: [PATCH] [doc] update reference manual wrt support of rationals
---
src/plugins/e-acsl/VERSION | 2 +-
src/plugins/e-acsl/doc/refman/binders.tex | 2 +-
.../e-acsl/doc/refman/changes_modern.tex | 7 +++++++
.../e-acsl/doc/refman/libraries_modern.tex | 5 ++---
.../e-acsl/doc/refman/speclang_modern.tex | 17 +++++++++--------
5 files changed, 20 insertions(+), 13 deletions(-)
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 0c48b6c985e..e11f7bd73d4 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-19.0
\ No newline at end of file
+19.0+dev
diff --git a/src/plugins/e-acsl/doc/refman/binders.tex b/src/plugins/e-acsl/doc/refman/binders.tex
index 53a46c97cc3..023fec69d07 100644
--- a/src/plugins/e-acsl/doc/refman/binders.tex
+++ b/src/plugins/e-acsl/doc/refman/binders.tex
@@ -9,7 +9,7 @@
logic-type-expr ::= built-in-logic-type ;
| id ; type identifier
\
- built-in-logic-type ::= "boolean" | "integer" | { "real" }
+ built-in-logic-type ::= "boolean" | "integer" | "real"
\
variable-ident ::= id
| "*" variable-ident ;
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index b610ebad7ea..ee30a79f7e0 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -125,6 +125,13 @@ in \lstinline|\\at|}
\section{Changes in \eacsl Implementation}
\subsection*{Version \eacslversion}
+
+\begin{itemize}
+\item \changeinsection{reals}{support of rational numbers and operations}
+\end{itemize}
+
+\subsection*{Version Potassium-19}
+
\begin{itemize}
\item \changeinsection{logicspec}{support of logic functions and predicates}
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/libraries_modern.tex b/src/plugins/e-acsl/doc/refman/libraries_modern.tex
index 862e5a22fe8..4e828cdd1d3 100644
--- a/src/plugins/e-acsl/doc/refman/libraries_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/libraries_modern.tex
@@ -1,6 +1,5 @@
\chapter{Libraries}
\label{chap:lib}
-\emph{Disclaimer:} this chapter is yet empty. It is left here to give an idea of
-what the final document will look and to be consistent with the \acsl reference
-manual~\cite{acsl}.
+\emph{Disclaimer:} this chapter is empty on purpose. It is left here to be
+consistent with the \acsl reference manual~\cite{acsl}.
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index baafd9b8bb8..c1482c0d65c 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -45,12 +45,6 @@ only difference between \eacsl and \acsl predicates are quantifications.
\label{fig:gram:binders}
\end{figure}
-\begin{notimplementedenv}
- Reals are not correctly supported by the \eacsl plug-in right now. Only
- floating point numbers are supported: real constants and operations are seen as
- \C floating point constants and operations.
-\end{notimplementedenv}
-
\subsection*{Quantification}
\eacsl quantification must be computable. They are limited to two limited forms.
@@ -260,10 +254,17 @@ It is not possible to define logic types introduced by the specification writer
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{\notimplemented{Real numbers} and floating point numbers}
+\subsection{Real numbers and floating point numbers}
+\label{sec:reals}
\nodiff
-\difficults{\notimplemented{Exact real numbers} and even floating point numbers}
+\difficults{Exact real numbers and even floating point numbers}
+
+\begin{notimplementedenv}
+ Real numbers beyond rationals are currently not supported by the \eacsl
+ plug-in. Only rationals (in $\mathbb{Q}$) and floating point numbers are
+ supported.
+\end{notimplementedenv}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
--
GitLab