checklink: adaptation to the new floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 11 insertions, 7 deletions

diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index 9f6a540..094d51d 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -186,7 +186,7 @@ let string_of_instruction = function
 | Plhax     (i0, i1, i2)        -> "Plhax(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plhz      (i0, c1, i2)        -> "Plhz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plhzx     (i0, i1, i2)        -> "Plhzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
-| Plfi      (f0, f1)            -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_float f1 ^ ")"
+| Plfi      (f0, f1)            -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat f1 ^ ")"
 | Plwz      (i0, c1, i2)        -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plwzx     (i0, i1, i2)        -> "Plwzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pmfcrbit  (i0, c1)            -> "Pmfcrbit(" ^ string_of_ireg i0 ^ ", " ^ string_of_crbit c1 ^ ")"
@@ -232,8 +232,8 @@ let string_of_init_data = function
 | Init_int8(i)    -> "Init_int8("    ^ string_of_int (z_int_lax i)  ^ ")"
 | Init_int16(i)   -> "Init_int16("   ^ string_of_int (z_int_lax i)  ^ ")"
 | Init_int32(i)   -> "Init_int32("   ^ string_of_int32i (z_int32 i) ^ ")"
-| Init_float32(f) -> "Init_float32(" ^ string_of_float f            ^ ")"
-| Init_float64(f) -> "Init_float64(" ^ string_of_float f            ^ ")"
+| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat f           ^ ")"
+| Init_float64(f) -> "Init_float64(" ^ string_of_ffloat f           ^ ")"
 | Init_space(z)   -> "Init_space("   ^ string_of_int (z_int z)      ^ ")"
 | Init_addrof(ident, ofs) ->
     "Init_addrof(" ^ string_of_pos ident ^ ", " ^ string_of_int32i (z_int32 ofs) ^ ")"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 8e2b103..840c233 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -5,6 +5,7 @@ open BinInt
 open BinPos
 open Bitstring_utils
 open C2C
+open Camlcoq
 open ELF_parsers
 open ELF_printers
 open ELF_types
@@ -335,8 +336,8 @@ let match_int32s a b: checker =
   ) a b
 (** We compare floats by their bit representation, so that 0.0 and -0.0 are
     different. *)
-let match_floats (a: float) (b: float): checker =
-  let a = Int64.bits_of_float a in
+let match_floats (a: Floats.float) (b: float): checker =
+  let a = Int64.bits_of_float (camlfloat_of_coqfloat a) in
   let b = Int64.bits_of_float b in
   check_eq (
     Printf.sprintf "match_floats %s %s" (string_of_int64 a) (string_of_int64 b)
@@ -2642,7 +2643,7 @@ let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework)
         | Init_float32(f) -> (
           bitmatch bs with
           | { j : 32 : int; bs : -1 : bitstring } ->
-              if f = Int32.float_of_bits j
+              if camlfloat_of_coqfloat f = Int32.float_of_bits j
               then compare_data_aux l bs (s + 4) sfw
               else ERR("Wrong float32")
           | { _ } -> error
@@ -2650,7 +2651,7 @@ let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework)
         | Init_float64(f) -> (
           bitmatch bs with
           | { j : 64 : int; bs : -1 : bitstring } ->
-              if f = Int64.float_of_bits j
+              if camlfloat_of_coqfloat f = Int64.float_of_bits j
               then compare_data_aux l bs (s + 8) sfw
               else ERR("Wrong float64")
           | { _ } -> error
diff --git a/checklink/Library.ml b/checklink/Library.ml
index b6f48ae..e6f1e2c 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -1,5 +1,6 @@
 open BinInt
 open BinPos
+open Camlcoq
 
 type bitstring = Bitstring.bitstring
 
@@ -112,6 +113,8 @@ let z_int_lax z = Safe32.to_int (z_int32_lax z)
 
 (* Some more printers *)
 
+let string_of_ffloat f = string_of_float (camlfloat_of_coqfloat f)
+
 let string_of_array string_of_elt sep a =
   let b = Buffer.create 1024 in
   Buffer.add_string b "[\n";