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 /arm/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 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 28 |
1 files changed, 4 insertions, 24 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index d90d7b64..186e327d 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -226,33 +226,13 @@ let call_helper oc fn dst arg1 arg2 = (* 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(R1 + %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 "sp" 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 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) |