From 2b5f5cb0bb6d8dbf302ab6d84c27eda30252912d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:23:18 +0100 Subject: Add support for EF_runtime externals Also: in Events, use Senv.equiv to state invariance wrt changes of global envs. --- cfrontend/PrintClight.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/PrintClight.ml') diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ed19e178..42892901 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -258,7 +258,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res, cconv) -> + | External((EF_external _ | EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | External(_, _, _, _) -> -- cgit From 4b0f05cf84ac5d38f8e31aa7b8f7c9e1b0617ea0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Mar 2016 15:05:11 +0100 Subject: 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. --- cfrontend/PrintClight.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'cfrontend/PrintClight.ml') 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, _) -> -- cgit