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 /backend/PrintCminor.ml | |
| parent | 2f31ded1ab2a78f1362b95b6079023c94909fe6b (diff) | |
| download | compcert-kvx-4b0f05cf84ac5d38f8e31aa7b8f7c9e1b0617ea0.tar.gz compcert-kvx-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 'backend/PrintCminor.ml')
| -rw-r--r-- | backend/PrintCminor.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 9b6b1488..45c18e9a 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -148,9 +148,9 @@ let rec expr p (prec, e) = | Econst(Ointconst n) -> fprintf p "%ld" (camlint_of_coqint n) | Econst(Ofloatconst f) -> - fprintf p "%F" (camlfloat_of_coqfloat f) + fprintf p "%.15F" (camlfloat_of_coqfloat f) | Econst(Osingleconst f) -> - fprintf p "%Ff" (camlfloat_of_coqfloat32 f) + fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f) | Econst(Olongconst n) -> fprintf p "%LdLL" (camlint64_of_coqint n) | Econst(Oaddrsymbol(id, ofs)) -> @@ -326,8 +326,8 @@ let print_init_data p = function | Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i) | Init_int32 i -> fprintf p "%ld" (camlint_of_coqint i) | Init_int64 i -> fprintf p "%LdLL" (camlint64_of_coqint i) - | Init_float32 f -> fprintf p "float32 %F" (camlfloat_of_coqfloat f) - | Init_float64 f -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Init_float32 f -> fprintf p "float32 %.15F" (camlfloat_of_coqfloat f) + | Init_float64 f -> fprintf p "%.15F" (camlfloat_of_coqfloat f) | Init_space i -> fprintf p "[%ld]" (camlint_of_coqint i) | Init_addrof(id,off) -> fprintf p "%ld(\"%s\")" (camlint_of_coqint off) (extern_atom id) |