Revised encoding/decoding of floats

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

1 files changed, 0 insertions, 51 deletions

diff --git a/common/Memdataaux.ml b/common/Memdataaux.ml
index 3a39428..0ec7523 100644
--- a/common/Memdataaux.ml
+++ b/common/Memdataaux.ml
@@ -10,59 +10,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open Camlcoq
-open Integers
-open AST
-
 let big_endian =
   match Configuration.arch with
   | "powerpc" -> true
   | "arm" -> false
   | _ -> assert false
-
-let encode_float chunk f =
-  match chunk with
-  | Mint8unsigned | Mint8signed ->
-      [Byte.zero]
-  | Mint16unsigned | Mint16signed ->
-      [Byte.zero; Byte.zero]
-  | Mint32 ->
-      [Byte.zero; Byte.zero; Byte.zero; Byte.zero]
-  | Mfloat32 ->
-      let bits = Int32.bits_of_float f in
-      let byte n =
-        coqint_of_camlint
-          (Int32.logand (Int32.shift_right_logical bits n) 0xFFl) in
-      if big_endian then
-        [byte 24; byte 16; byte 8; byte 0]
-      else
-        [byte 0; byte 8; byte 16; byte 24]
-  | Mfloat64 ->
-      let bits = Int64.bits_of_float f in
-      let byte n =
-        coqint_of_camlint
-          (Int64.to_int32
-            (Int64.logand (Int64.shift_right_logical bits n) 0xFFL)) in
-      if big_endian then
-        [byte 56; byte 48; byte 40; byte 32; byte 24; byte 16; byte 8; byte 0]
-      else
-        [byte 0; byte 8; byte 16; byte 24; byte 32; byte 40; byte 48; byte 56]
-
-let decode_float chunk bytes =
-  match chunk with
-  | Mfloat32 ->
-      let combine accu b =
-        Int32.logor (Int32.shift_left accu 8) (camlint_of_coqint b) in
-      Int32.float_of_bits
-        (List.fold_left combine 0l
-          (if big_endian then bytes else List.rev bytes))
-  | Mfloat64 ->
-      let combine accu b =
-        Int64.logor (Int64.shift_left accu 8)
-                    (Int64.of_int32 (camlint_of_coqint b)) in
-      Int64.float_of_bits
-        (List.fold_left combine 0L
-          (if big_endian then bytes else List.rev bytes))
-  | _ ->
-      0.0 (* unspecified *)
-