From ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 25 Jan 2010 12:47:40 +0000 Subject: Updated ARM port git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 6 ++++-- extraction/extraction.v | 4 ---- powerpc/extractionMachdep.v | 3 +++ 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 2239911..5e2cfbb 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 diff --git a/extraction/extraction.v b/extraction/extraction.v index 77c6c62..6488d8b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -52,10 +52,6 @@ Extract Constant Iteration.GenIter.iterate => match f a with Coq_inl b -> Some b | Coq_inr a' -> iter f a' in iter". - -(* Selection *) -Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". - (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 46c40ca..83fda76 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -12,6 +12,9 @@ (* Additional extraction directives specific to the PowerPC port *) +(* Selection *) +Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". + (* Asm *) Extract Constant Asm.low_half => "fun _ -> assert false". Extract Constant Asm.high_half => "fun _ -> assert false". -- cgit v1.2.3