diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
| commit | 5312915c1b29929f82e1f8de80609a277584913f (patch) | |
| tree | 0f7ee475743f0eb05d352148a9e1f0b861ee9d34 /driver/Interp.ml | |
| parent | f3250c32ff42ae18fd03a5311c1f0caec3415aba (diff) | |
| download | compcert-kvx-5312915c1b29929f82e1f8de80609a277584913f.tar.gz compcert-kvx-5312915c1b29929f82e1f8de80609a277584913f.zip | |
Use Flocq for floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Interp.ml')
| -rw-r--r-- | driver/Interp.ml | 13 |
1 files changed, 8 insertions, 5 deletions
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 = |