diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-07-19 12:39:17 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-07-19 12:39:17 +0200 |
| commit | 32d25a371fc0e1aaea2a94459363b21e9841d637 (patch) | |
| tree | b96b4c7555eb3fbe0190caaae79010e27c731123 /powerpc/TargetPrinter.ml | |
| parent | 2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6 (diff) | |
| download | compcert-kvx-32d25a371fc0e1aaea2a94459363b21e9841d637.tar.gz compcert-kvx-32d25a371fc0e1aaea2a94459363b21e9841d637.zip | |
Print_annot should produce a string.
Diffstat (limited to 'powerpc/TargetPrinter.ml')
| -rw-r--r-- | powerpc/TargetPrinter.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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 |