From d58c35ebb8c3124d67c51091bb6e4cfedc59d999 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Mar 2016 14:57:27 +0100 Subject: GPR#84: add missing IA32 operators to PrintOp --- ia32/PrintOp.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'ia32/PrintOp.ml') diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml index 1f7f4a65..fbdcdac1 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -119,6 +119,9 @@ let print_operation reg pp = function | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 + | Onot, [r1] -> fprintf pp "not(%a)" reg r1 + | Omulhs, [r1;r2] -> fprintf pp "mulhs(%a,%a)" reg r1 reg r2 + | Omulhu, [r1;r2] -> fprintf pp "mulhu(%a,%a)" reg r1 reg r2 | Ocmp c, args -> print_condition reg pp (c, args) | _ -> fprintf pp "" -- cgit From 4b0f05cf84ac5d38f8e31aa7b8f7c9e1b0617ea0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Mar 2016 15:05:11 +0100 Subject: Print floating-point numbers with more digits in debug outputs As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always). Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing. --- ia32/PrintOp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ia32/PrintOp.ml') diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml index fbdcdac1..2a80e3d4 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -67,8 +67,8 @@ let print_addressing reg pp = function let print_operation reg pp = function | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) - | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) - | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n) + | Ofloatconst n, [] -> fprintf pp "%.15F" (camlfloat_of_coqfloat n) + | Osingleconst n, [] -> fprintf pp "%.15Ff" (camlfloat_of_coqfloat32 n) | Oindirectsymbol id, [] -> fprintf pp "&%s" (extern_atom id) | Ocast8signed, [r1] -> fprintf pp "int8signed(%a)" reg r1 | Ocast8unsigned, [r1] -> fprintf pp "int8unsigned(%a)" reg r1 -- cgit