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.

9 files changed, 22 insertions, 22 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. *)
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)
 
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index ed19e178..9600b3fa 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -84,9 +84,9 @@ let rec expr p (prec, e) =
   | Econst_int(n, _) ->
       fprintf p "%ld" (camlint_of_coqint n)
   | Econst_float(f, _) ->
-      fprintf p "%F" (camlfloat_of_coqfloat f)
+      fprintf p "%.15F" (camlfloat_of_coqfloat f)
   | Econst_single(f, _) ->
-      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
+      fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f)
   | Econst_long(n, Tlong(Unsigned, _)) ->
       fprintf p "%LuLLU" (camlint64_of_coqint n)
   | Econst_long(n, _) ->
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index bb6576aa..f68f520d 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -182,9 +182,9 @@ let print_typed_value p v ty =
   | Vint n, _ ->
       fprintf p "%ld" (camlint_of_coqint n)
   | Vfloat f, _ ->
-      fprintf p "%F" (camlfloat_of_coqfloat f)
+      fprintf p "%.15F" (camlfloat_of_coqfloat f)
   | Vsingle f, _ ->
-      fprintf p "%Ff" (camlfloat_of_coqfloat32 f)
+      fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f)
   | Vlong n, Tlong(Unsigned, _) ->
       fprintf p "%LuLLU" (camlint64_of_coqint n)
   | Vlong n, _ ->
@@ -457,8 +457,8 @@ let print_init p = function
   | Init_int16 n -> fprintf p "%ld" (camlint_of_coqint n)
   | Init_int32 n -> fprintf p "%ld" (camlint_of_coqint n)
   | Init_int64 n -> fprintf p "%LdLL" (camlint64_of_coqint n)
-  | Init_float32 n -> fprintf p "%F" (camlfloat_of_coqfloat n)
-  | Init_float64 n -> fprintf p "%F" (camlfloat_of_coqfloat n)
+  | Init_float32 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n)
+  | Init_float64 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n)
   | Init_space n -> fprintf p "/* skip %ld */@ " (camlint_of_coqint n)
   | Init_addrof(symb, ofs) ->
       let ofs = camlint_of_coqint ofs in
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 39481bfb..4994026a 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -55,8 +55,8 @@ let rec print_builtin_arg px oc = function
   | BA x -> px oc x
   | BA_int n -> fprintf oc "int %ld" (camlint_of_coqint n)
   | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n)
-  | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n)
-  | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n)
+  | BA_float n -> fprintf oc "float %.15F" (camlfloat_of_coqfloat n)
+  | BA_single n -> fprintf oc "single %.15F" (camlfloat_of_coqfloat32 n)
   | BA_loadstack(chunk, ofs) ->
       fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs)
   | BA_addrstack(ofs) ->
diff --git a/driver/Interp.ml b/driver/Interp.ml
index fb1c85f0..4b6d0a44 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -45,8 +45,8 @@ 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" (camlfloat_of_coqfloat f)
-  | EVsingle f -> fprintf p "%F" (camlfloat_of_coqfloat32 f)
+  | EVfloat f -> fprintf p "%.15F" (camlfloat_of_coqfloat f)
+  | EVsingle f -> fprintf p "%.15F" (camlfloat_of_coqfloat32 f)
   | EVlong n -> fprintf p "%LdLL" (camlint64_of_coqint n)
   | EVptr_global(id, ofs) -> fprintf p "&%a" print_id_ofs (id, ofs)
 
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
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index b0213014..a3fac2c3 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -48,8 +48,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, [] ->