diff options
author | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-03 09:15:24 +0000 |
---|---|---|
committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-03 09:15:24 +0000 |
commit | c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30 (patch) | |
tree | 765798824239f826f5cd008eecf1fdb0ea6820f6 /checklink/Check.ml | |
parent | 3de3ecc23d8ab5d6d45451075467dd70981f1061 (diff) | |
download | compcert-c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30.tar.gz compcert-c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30.zip |
checklink: adaptation to the new floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Check.ml')
-rw-r--r-- | checklink/Check.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml index 8e2b1033..840c2334 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 |