diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
| commit | 01e32a075023ce7b037d42d048b1904ba3d9a82b (patch) | |
| tree | 2d01f3855234e6eb945b929e489232001c406592 /backend/PrintCminor.ml | |
| parent | 093e0ea167fde39429bf4bd3fc693a232af0d093 (diff) | |
| parent | 1fdca8371317e656cb08eaec3adb4596d6447e9b (diff) | |
| download | compcert-kvx-01e32a075023ce7b037d42d048b1904ba3d9a82b.tar.gz compcert-kvx-01e32a075023ce7b037d42d048b1904ba3d9a82b.zip | |
Merge branch 'master' into cleanup
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 5e686b55..d50e07a3 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -147,9 +147,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)) -> @@ -325,8 +325,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) |