From f401437a97b09726d029e3a1b65143f34baaea70 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 24 Feb 2013 09:40:25 +0000
Subject: Updated ARM and PowerPC ports with new handling of __builtin_annot.
 ARM: add support for builtin_volatile_{read,write}_global, after all.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/PrintAsm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'powerpc/PrintAsm.ml')

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 9c0f471..c9203ec 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -231,9 +231,9 @@ let rolm_mask n =
 
 (* Handling of annotations *)
 
-let print_annot_stmt oc txt args =
+let print_annot_stmt oc txt targs args =
   fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_stmt preg "R1" oc txt args
+  PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
@@ -737,7 +737,7 @@ let print_instruction oc tbl pc fallthrough = function
   | Pannot(ef, args) ->
       begin match ef with
       | EF_annot(txt, targs) ->
-          print_annot_stmt oc (extern_atom txt) args
+          print_annot_stmt oc (extern_atom txt) targs args
       | _ ->
           assert false
       end
-- 
cgit v1.2.3