aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/PrintOp.ml4
-rw-r--r--arm/TargetPrinter.ml4
-rw-r--r--backend/PrintCminor.ml8
-rw-r--r--cfrontend/PrintClight.ml4
-rw-r--r--cfrontend/PrintCsyntax.ml8
-rw-r--r--common/PrintAST.ml4
-rw-r--r--driver/Interp.ml4
-rw-r--r--ia32/PrintOp.ml4
-rw-r--r--powerpc/PrintOp.ml4
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, [] ->
generated by cgit (git 2.34.1) at 2024-06-02 16:57:51 +0000