From 3df67218d4551653683640bd52cda5bf8401f77b Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 25 Jan 2010 13:14:38 +0000 Subject: Updated ARM asm printer git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1233 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'arm') 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. -- cgit