From 1b5db339bb05f773a6a132be4c0b8cea54d50461 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 17 Apr 2015 16:30:43 +0200
Subject: Experiment: support a subset of GCC's extended asm statements.

---
 backend/PrintAnnot.ml | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

(limited to 'backend/PrintAnnot.ml')

diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index 995f22dd..88f5d8d6 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -148,7 +148,29 @@ let print_annot_val print_preg oc txt args =
   print_annot_text print_preg "<internal error>" oc txt
     (List.map (fun r -> AA_base r) args)
 
-(* Print CompCert version and command-line as asm comment *)
+(** Inline assembly *)
+
+let re_asm_param = Str.regexp "%%\\|%[0-9]+"
+
+let print_inline_asm print_preg oc txt sg args res =
+  let operands =
+    if sg.sig_res = None then args else res @ args in
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_preg oc (List.nth operands n)
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_asm_param txt);
+  fprintf oc "\n"
+
+
+(** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
   fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
-- 
cgit