diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-25 13:14:38 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-25 13:14:38 +0000 |
commit | 3df67218d4551653683640bd52cda5bf8401f77b (patch) | |
tree | 59c9417d8e9e0a127f1e5f09ad440100de47ff6a /arm/PrintAsm.ml | |
parent | ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab (diff) | |
download | compcert-3df67218d4551653683640bd52cda5bf8401f77b.tar.gz compcert-3df67218d4551653683640bd52cda5bf8401f77b.zip |
Updated ARM asm printer
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1233 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 5e2cfbbe..25d9db2e 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -388,10 +388,15 @@ let rec print_instructions oc labels instrs = end; print_instructions oc labels il -let rec labels_of_code = function - | [] -> Labelset.empty - | (Pb lbl | Pbc(_, lbl)) :: c -> Labelset.add lbl (labels_of_code c) - | _ :: c -> labels_of_code c +let rec labels_of_code accu = function + | [] -> + accu + | (Pb lbl | Pbc(_, lbl)) :: c -> + labels_of_code (Labelset.add lbl accu) c + | Pbtbl(_, tbl) :: c -> + labels_of_code (List.fold_right Labelset.add tbl accu) c + | _ :: c -> + labels_of_code accu c let print_function oc name code = Hashtbl.clear current_function_labels; @@ -402,7 +407,7 @@ let print_function oc name code = fprintf oc " .global %a\n" print_symb name; fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc "%a:\n" print_symb name; - print_instructions oc (labels_of_code code) code; + print_instructions oc (labels_of_code Labelset.empty code) code; emit_constants oc (* Generation of stub code for external functions. |