From c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30 Mon Sep 17 00:00:00 2001 From: varobert Date: Tue, 3 Jul 2012 09:15:24 +0000 Subject: checklink: adaptation to the new floats git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Asm_printers.ml | 6 +++--- checklink/Check.ml | 9 +++++---- checklink/Library.ml | 3 +++ 3 files changed, 11 insertions(+), 7 deletions(-) (limited to 'checklink') 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"; -- cgit v1.2.3