From ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 25 Jan 2010 12:47:40 +0000
Subject: [PATCH] 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 22399112a..5e2cfbbe1 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 77c6c62bb..6488d8b1d 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 46c40caed..83fda76e0 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".
--
GitLab