diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
commit | 202bc495442a1a8fa184b73ac0063bdbbbcdf846 (patch) | |
tree | 46c6920201b823bf47252bc52864b0bf60f3233e /ia32/PrintAsm.ml | |
parent | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (diff) | |
download | compcert-kvx-202bc495442a1a8fa184b73ac0063bdbbbcdf846.tar.gz compcert-kvx-202bc495442a1a8fa184b73ac0063bdbbbcdf846.zip |
Constant propagation within __builtin_annot.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/PrintAsm.ml')
-rw-r--r-- | ia32/PrintAsm.ml | 30 |
1 files changed, 5 insertions, 25 deletions
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 "<bad parameter %s>" 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 |