diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-15 15:05:11 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-15 15:05:11 +0100 |
commit | 4b0f05cf84ac5d38f8e31aa7b8f7c9e1b0617ea0 (patch) | |
tree | a52ac11cdc92b969748e6086af116e2613dba21a /arm | |
parent | 2f31ded1ab2a78f1362b95b6079023c94909fe6b (diff) | |
download | compcert-4b0f05cf84ac5d38f8e31aa7b8f7c9e1b0617ea0.tar.gz compcert-4b0f05cf84ac5d38f8e31aa7b8f7c9e1b0617ea0.zip |
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.
Diffstat (limited to 'arm')
-rw-r--r-- | arm/PrintOp.ml | 4 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 886f6de3..71e1dfc3 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -66,8 +66,8 @@ let print_condition 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) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 6536bc55..3ca90ce9 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -650,7 +650,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Pflid(r1, f) -> let f = camlint64_of_coqint(Floats.Float.to_bits f) in if Opt.vfpv3 && is_immediate_float64 f then begin - fprintf oc " vmov.f64 %a, #%F\n" + fprintf oc " vmov.f64 %a, #%.15F\n" freg r1 (Int64.float_of_bits f); 1 (* immediate floats have at most 4 bits of fraction, so they should print exactly with OCaml's F decimal format. *) @@ -702,7 +702,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Pflis(r1, f) -> let f = camlint_of_coqint(Floats.Float32.to_bits f) in if Opt.vfpv3 && is_immediate_float32 f then begin - fprintf oc " vmov.f32 %a, #%F\n" + fprintf oc " vmov.f32 %a, #%.15F\n" freg_single r1 (Int32.float_of_bits f); 1 (* immediate floats have at most 4 bits of fraction, so they should print exactly with OCaml's F decimal format. *) |