[Kernel] Updating the documentation of Typed_float.

src/libraries/floating_point/floating_point.c

@@ -88,7 +88,10 @@ value frama_c_get_round_mode(value _) {
 }
 
 // Floating-point formats supported by Frama-C. Must be synchronized with
-// the ['f format] type of the [Floating_point] module.
+// the ['f format] type of the [Floating_point] module, in the sens that it
+// must contain at least one value for each constructor of ['f format], and
+// those values have to be in the same order. For now, there is also a [Long]
+// value, which is not yet used, but will probably be in the future.
 typedef enum { Single, Double, Long } precision;
 
 // Convert the Frama-C format into a precision.

src/libraries/floating_point/typed_float.mli

@@ -25,21 +25,14 @@
     The goal of this module is to provide a representation of floating-point
     numbers that statically encode the format of the represented number. As
     for now, the numbers are represented using the OCaml [float] type (which
-    are in the [binary64] format) and thus, all operations for the [Long]
-    format (or [binary80]) are unsound as they are performed using the
-    [binary64] format instead of [binary80] for x86 architectures.
+    are in the [binary64] format) and thus, the [Long] format (or [binary80])
+    is not yet supported.
 
-    This is TEMPORARY, and does not break anything in Frama-C as the historical
-    way of handling the [Long] format was to use the OCaml [float] type. Future
-    improvements of this module WILL INCLUDE a correct way to perform
-    computations in the [Long] format.
+    The main feature of this module currently used by Frama-C is the [parse]
+    function, which returns a witness that specifies the format one would like
+    to use and the one actually used to encode the parsed floating point number.
 
-    The format is nevertheless presents because Frama-C still needs to be able
-    to differentiate between the two formats. In particular, the parsing
-    process must be able to infer the correct format to store the
-    corresponding [fkind], and the logic must know the correct [fkind] to emit
-    relevant warnings that partially alleviate the incorrectness resulting
-    from Frama-C encoding of [Long] numbers. *)
+    @since Frama-C+dev *)
 
 
 
@@ -137,6 +130,9 @@ type 'f parsed_float =
   ; format  : 'f format
   }
 
+(** A witness encoding the floating-point format represented by the string,
+    and the format actually used to parse it. For now, Long format is not
+    supported by this module, and is thus approximated using double precision. *)
 type ('format, 'encoded_as) parsed_format =
   | Single_supported : (single, single) parsed_format
   | Double_supported : (double, double) parsed_format