From 5312915c1b29929f82e1f8de80609a277584913f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 28 Jun 2012 07:59:03 +0000
Subject: Use Flocq for floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 driver/Interp.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'driver/Interp.ml')

diff --git a/driver/Interp.ml b/driver/Interp.ml
index a74d4d8e..0c19673d 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -12,6 +12,8 @@
 
 (* Interpreting CompCert C sources *)
 
+type caml_float = float
+
 open Format
 open Camlcoq
 open Datatypes
@@ -48,7 +50,7 @@ let print_id_ofs p (id, ofs) =
 
 let print_eventval p = function
   | EVint n -> fprintf p "%ld" (camlint_of_coqint n)
-  | EVfloat f -> fprintf p "%F" f
+  | EVfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f)
   | EVptr_global(id, ofs) -> fprintf p "&%a" print_id_ofs (id, ofs)
 
 let print_eventval_list p = function
@@ -297,7 +299,7 @@ let extract_string ge m id ofs =
 let re_conversion = Str.regexp
   "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\)?\\([aAcdeEfgGinopsuxX%]\\)"
 
-external format_float: string -> float -> string
+external format_float: string -> caml_float -> string
   = "caml_format_float"
 external format_int32: string -> int32 -> string
   = "caml_int32_format"
@@ -332,7 +334,7 @@ let do_printf ge m fmt args =
             Buffer.add_string b (format_int32 pat (camlint_of_coqint i));
             scan pos' args'
         | EVfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') ->
-            Buffer.add_string b (format_float pat f);
+            Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f));
             scan pos' args'
         | EVptr_global(id, ofs) :: args', 's' ->
             Buffer.add_string b
@@ -372,8 +374,9 @@ and world_vload chunk id ofs =
     | Mint16signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x10000l) 0x8000l))
     | Mint16unsigned -> EVint(coqint_of_camlint(Random.int32 0x10000l))
     | Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl))
-    | Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0))
-    | Mfloat64 -> EVfloat(Random.float 1.0)
+    | Mfloat32 -> EVfloat(
+	Floats.Float.singleoffloat(coqfloat_of_camlfloat(Random.float 1.0)))
+    | Mfloat64 -> EVfloat(coqfloat_of_camlfloat(Random.float 1.0))
   in Some(res, world)
 
 and world_vstore chunk id ofs v =
-- 
cgit