diff options
-rw-r--r-- | arm/PrintOp.ml | 4 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | backend/PrintCminor.ml | 8 | ||||
-rw-r--r-- | cfrontend/PrintClight.ml | 4 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 | ||||
-rw-r--r-- | common/PrintAST.ml | 4 | ||||
-rw-r--r-- | driver/Interp.ml | 4 | ||||
-rw-r--r-- | ia32/PrintOp.ml | 4 | ||||
-rw-r--r-- | powerpc/PrintOp.ml | 4 |
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, [] -> |