From 32d25a371fc0e1aaea2a94459363b21e9841d637 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 19 Jul 2017 12:39:17 +0200 Subject: Print_annot should produce a string. --- powerpc/TargetPrinter.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index cb5f2304..bff2a7fa 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -335,9 +335,9 @@ module Target (System : SYSTEM):TARGET = (* For printing annotations, use the full register names [rN] and [fN] to avoid ambiguity with constants. *) - let preg_annot oc = function - | IR r -> fprintf oc "r%s" (int_reg_name r) - | FR r -> fprintf oc "f%s" (float_reg_name r) + let preg_annot = function + | IR r -> sprintf "r%s" (int_reg_name r) + | FR r -> sprintf "f%s" (float_reg_name r) | _ -> assert false (* Encoding masks for rlwinm instructions *) @@ -834,8 +834,8 @@ module Target (System : SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args + fprintf oc "%s annotation: %s\n" comment + (annot_text preg_annot "r1" (camlstring_of_coqstring txt) args) | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "r1" oc (P.to_int kind) (extern_atom txt) args -- cgit