From 202bc495442a1a8fa184b73ac0063bdbbbcdf846 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 24 Feb 2013 09:01:28 +0000 Subject: Constant propagation within __builtin_annot. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/PrintAsm.ml | 30 +++++------------------------- 1 file changed, 5 insertions(+), 25 deletions(-) (limited to 'ia32/PrintAsm.ml') diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 00744055..4f626405 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -231,33 +231,13 @@ let need_masks = ref false (* Handling of annotations *) -let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" - -let print_annot_text print_arg oc txt args = - fprintf oc "%s annotation: " comment; - 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_arg oc (List.nth args (n-1)) - with Failure _ -> - fprintf oc "" s in - List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n" - let print_annot_stmt oc txt args = - let print_annot_param oc = function - | APreg r -> preg oc r - | APstack(chunk, ofs) -> - fprintf oc "mem(ESP + %a, %a)" coqint ofs coqint (size_chunk chunk) in - print_annot_text print_annot_param oc txt args + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "ESP" oc txt args let print_annot_val oc txt args res = - print_annot_text preg oc txt args; + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_val preg oc txt args; match args, res with | IR src :: _, IR dst -> if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst @@ -723,7 +703,7 @@ let print_instruction oc = 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