From 1c4e0ece041f87cc0c328c94270f2b23facc8b77 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 8 Mar 2018 16:02:52 +0100
Subject: Print symbols as symbols.

This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438
---
 arm/AsmToJSON.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'arm/AsmToJSON.ml')

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 22adc44c..276ceecc 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -130,10 +130,11 @@ let pp_arg pp = function
 
 let pp_instructions pp ic =
   let ic = List.filter (fun s -> match s with
-      | Pbuiltin (ef,_,_) ->
+      | Pbuiltin (ef,args,_) ->
         begin match ef with
-          | EF_inline_asm _
-          | EF_annot _ -> true
+          | EF_inline_asm _ -> true
+          | EF_annot  (kind,txt,targs) ->
+            P.to_int kind = 2 && AisAnnot.json_ais_annot TargetPrinter.preg_annot "r13" (camlstring_of_coqstring txt) args <> []
           | _ -> false
         end
       (* Only debug relevant *)
@@ -156,19 +157,18 @@ let pp_instructions pp ic =
           instruction pp "Pinlineasm" [Id];
           Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump")
         | EF_annot (kind,txt, targs) ->
-          let annot_string = PrintAsmaux.annot_text TargetPrinter.preg_annot "r1" (camlstring_of_coqstring txt) args in
-          let len = String.length annot_string in
-          let buf = Buffer.create len in
-          String.iter (fun c -> begin match c with
-              | '\\' | '"' -> Buffer.add_char buf '\\'
-              | _ -> () end;
-              Buffer.add_char buf c) annot_string;
-          let annot_string = Buffer.contents buf in
-        let kind = match P.to_int kind with
-          | 1 -> "normal"
-          | 2 -> "ais"
-          | _ -> assert false in
-          instruction pp "Pannot" [String kind;String annot_string]
+
+          begin match P.to_int kind with
+          | 2 ->
+            let annots = AisAnnot.json_ais_annot TargetPrinter.preg_annot "r13" (camlstring_of_coqstring txt) args in
+            let annots = List.map (function
+                | AisAnnot.String s -> String s
+                | AisAnnot.Symbol s -> Atom s
+                | AisAnnot.Label _ -> assert false (* should never happen *)
+              ) annots in
+            instruction pp "Pannot" annots
+          | _ -> assert false
+          end
         (* Builtins that are not exported to JSON *)
         | EF_annot_val _
         | EF_builtin _
-- 
cgit