diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 08:39:30 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 08:39:30 +0000 |
commit | fb202a70ccc2872aa3849854c09810a6bee268e5 (patch) | |
tree | 1b2fa2f5fa1c7f84ff7589f778985a0db306d845 /arm/PrintAsm.ml | |
parent | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (diff) | |
download | compcert-kvx-fb202a70ccc2872aa3849854c09810a6bee268e5.tar.gz compcert-kvx-fb202a70ccc2872aa3849854c09810a6bee268e5.zip |
powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).
Added -dmach option and corresponding printer for Mach code.
CleanupLabelsproof.v: fixed for ARM
Driver.ml: -E sends output to stdout; support for .s and .S source files.
cparser/Elab.ml: spurious comment deleted.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 23 |
1 files changed, 5 insertions, 18 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 66ee7722..8be92fd5 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -363,9 +363,7 @@ let shift_addr oc = function | SAasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n | SAror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n -module Labelset = Set.Make(struct type t = label let compare = compare end) - -let print_instruction oc labels = function +let print_instruction oc = function (* Core instructions *) | Padd(r1, r2, so) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 @@ -492,8 +490,7 @@ let print_instruction oc labels = function else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 | Plabel lbl -> - if Labelset.mem lbl labels then - fprintf oc "%a:\n" print_label lbl; 0 + fprintf oc "%a:\n" print_label lbl; 0 | Ploadsymbol(r1, id, ofs) -> let lbl = label_symbol id ofs in fprintf oc " ldr %a, .L%d @ %a\n" @@ -517,7 +514,7 @@ let no_fallthrough = function | Pbreg _ -> true | _ -> false -let rec print_instructions oc labels instrs = +let rec print_instructions oc instrs = match instrs with | [] -> () | i :: il -> @@ -532,17 +529,7 @@ let rec print_instructions oc labels instrs = emit_constants oc; fprintf oc ".L%d:\n" lbl end; - print_instructions oc labels il - -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 + print_instructions oc il let print_function oc name code = Hashtbl.clear current_function_labels; @@ -554,7 +541,7 @@ let print_function oc name code = if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; - print_instructions oc (labels_of_code Labelset.empty code) code; + print_instructions oc code; emit_constants oc; fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name |