diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/PrintClight.ml | 4 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 |
2 files changed, 6 insertions, 6 deletions
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 |