From ed2fe1ee74a6615b740019941f0f3d42d184bf01 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 28 Jun 2023 17:04:18 +0200
Subject: [PATCH] [doc] Clarified ieee 754 floating point requirement in spec

---
 doc/acas_xu.rst | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 81bef8e..cb836f4 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -125,11 +125,15 @@ our theory ``ACASXU_P1``.
 
 We will need to write down some numerical values. As of now, CAISAR allows
 writing values using floating-point arithmetic only. Why3 defines a float type
-and the relevant arithmetic operations according to the IEEE floating-point
+and the relevant arithmetic operations according to the IEEE 754 floating-point
 standard in a theory, astutely called ``ieee_float``. Specifically, we will
 import the ``Float64`` sub-theory, that defines everything we need for 64-bit
 precision floating-point numbers. We thus import it in our theory using the
 ``use`` keyword.
+This currently requires to write exact IEEE 754 floating
+point values in the specification file, which is
+understandably a setback in terms of usability, but have the
+advantage of being unambiguous on the specification.
 
 Our file looks like this so far:
 
-- 
GitLab