diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-25 12:47:40 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-25 12:47:40 +0000 |
commit | ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab (patch) | |
tree | f5569a9fffa5a7e0df14fc704e81143e2d185ea4 /arm/PrintAsm.ml | |
parent | 307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac (diff) | |
download | compcert-ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab.tar.gz compcert-ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab.zip |
Updated ARM port
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 22399112..5e2cfbbe 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -14,6 +14,7 @@ open Printf open Datatypes +open Integers open Camlcoq open AST open Asm @@ -116,7 +117,7 @@ let label_float f = max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' -let symbol_labels = (Hashtbl.create 39 : (ident * Integers.int, int) Hashtbl.t) +let symbol_labels = (Hashtbl.create 39 : (ident * Int.int, int) Hashtbl.t) let label_symbol id ofs = try @@ -360,7 +361,8 @@ let print_instruction oc labels = function fprintf oc " ldr pc, [pc, %a]\n" ireg r; fprintf oc " mov r0, r0\n"; (* no-op *) List.iter - (fun l -> fprintf oc " .word %a\n" label (transl_label l)); + (fun l -> fprintf oc " .word %a\n" print_label l) + tbl; 2 + List.length tbl let no_fallthrough = function |