From 32d25a371fc0e1aaea2a94459363b21e9841d637 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 19 Jul 2017 12:39:17 +0200
Subject: Print_annot should produce a string.

---
 arm/TargetPrinter.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'arm')

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 6f1cb6c1..0626a371 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -81,6 +81,11 @@ struct
     | FR r -> freg oc r
     | _    -> assert false
 
+  let preg_annot = function
+    | IR r -> int_reg_name r
+    | FR r -> float_reg_name r
+    | _ -> assert false
+
   let condition_name = function
     | TCeq -> "eq"
     | TCne -> "ne"
@@ -730,11 +735,11 @@ struct
     | Pbuiltin(ef, args, res) ->
       begin match ef with
         | EF_annot(txt, targs) ->
-          fprintf oc "%s annotation: " comment;
-          print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args;
+          fprintf oc "%s annotation: %s\n" comment
+          (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args);
           0
         | EF_debug(kind, txt, targs) ->
-          print_debug_info comment print_file_line preg "sp" oc
+          print_debug_info comment print_file_line preg_annot "sp" oc
             (P.to_int kind) (extern_atom txt) args;
           0
         | EF_inline_asm(txt, sg, clob) ->
-- 
cgit