From c145059a48397a1563e01c7371eb48e3e5dbf952 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 27 May 2021 12:48:37 +0200
Subject: [PATCH] [wp/doc] Document new Overflow behavior
---
src/plugins/wp/doc/manual/wp_plugin.tex | 22 ++++++++++++++--------
1 file changed, 14 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 950ec5f52de..d3bfd7913e6 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -487,19 +487,25 @@ $G(n) \equiv P(n)\Longrightarrow\,Q(n)$:
\end{array}} \]
\paragraph{Overflow} Integer Conversions \\
-This tactic rewrites machine integer conversions by identity,
-providing the converted value is in available range. The tactic applies on expression
-with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer name,
-\emph{eg.} \texttt{to\_uint32}.
+This tactic split machine integer conversions into three cases: value in integer
+range, lower than range and upper than range. The tactic applies on expression
+with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer
+name, \emph{eg.} \texttt{to\_uint32}.
\[\TACTIC{\Delta\models G}{%
\begin{array}[t]{rcl}
-\Delta\phantom{)} &\models & a \leq e \leq b \\
-\sigma(\Delta) & \models & \sigma(G)
+\sigma_{id}(\Delta) & \models & low \leq e \leq up \Rightarrow \sigma_{id}(G) \\
+\sigma_{+}(\Delta) & \models & low < e \Rightarrow \sigma_{+}(G) \\
+\sigma_{-}(\Delta) & \models & e < up \Rightarrow \sigma_{-}(G)
\end{array}
}\]
-where $\sigma = [ \mathtt{to\_iota}(e) \mapsto e ]$ and $[a..b]$ is the range
-of the \texttt{iota} integer domain.
+where
+\begin{itemize}
+ \item $[low..up]$ is the range of the \texttt{iota} integer domain,
+ \item $\sigma_{id} = [ \mathtt{to\_iota}(e) \mapsto e ]$,
+ \item $\sigma_{+} = [ \mathtt{to\_iota}(e) \mapsto \mathtt{overflow}(e) ]$,
+ \item $\sigma_{-} = [ \mathtt{to\_iota}(e) \mapsto \mathtt{overflow}(e) ]$.
+\end{itemize}
\paragraph{Range} Enumerate a range of values for an integer term\\
The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $e<a$ and $e>b$:
--
GitLab