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 /powerpc | |
parent | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (diff) | |
download | compcert-fb202a70ccc2872aa3849854c09810a6bee268e5.tar.gz compcert-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 'powerpc')
-rw-r--r-- | powerpc/PrintAsm.ml | 19 |
1 files changed, 3 insertions, 16 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 22644985..daa7f90b 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -422,12 +422,10 @@ let print_annotation oc txt args res = (* Printing of instructions *) -module Labelset = Set.Make(struct type t = label let compare = compare end) - let float_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] -let print_instruction oc labels = function +let print_instruction oc = function | Padd(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Paddi(r1, r2, c) -> @@ -654,8 +652,7 @@ let print_instruction oc labels = function | Pxoris(r1, r2, c) -> fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c | Plabel lbl -> - if Labelset.mem lbl labels then - fprintf oc "%a:\n" label (transl_label lbl) + fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> let name = extern_atom ef.ef_id in if Str.string_match re_builtin_annotation name 0 @@ -673,16 +670,6 @@ let print_jumptable oc (lbl, tbl) = (fun l -> fprintf oc " .long %a\n" label (transl_label l)) tbl -let rec labels_of_code accu = function - | [] -> - accu - | (Pb lbl | Pbf(_, lbl) | Pbt(_, 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; float_literals := []; @@ -693,7 +680,7 @@ let print_function oc name code = if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; - List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code; + List.iter (print_instruction oc) code; if target <> MacOS then begin fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name |