From e9704f237a400630ba45ee65779123b054dc1d6c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 17 May 2013 08:59:15 +0000
Subject: Update ARM port.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/Asmgenproof.v |  4 ++--
 arm/PrintAsm.ml   | 26 ++++++++++++--------------
 2 files changed, 14 insertions(+), 16 deletions(-)

(limited to 'arm')

diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index aede0da..6899040 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -693,7 +693,7 @@ Opaque loadind.
     exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. 
     econstructor; split.
     eapply exec_straight_trans. eexact P. apply exec_straight_one. 
-    simpl. rewrite R; auto with asmgen. unfold Mach.chunk_of_type in A. rewrite A. 
+    simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. 
     rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. 
     split. Simpl.
     split. Simpl.
@@ -896,7 +896,7 @@ Opaque loadind.
   rewrite <- H5 at 2; unfold fn_code.
   apply exec_straight_two with rs2 m2'.
   unfold exec_instr. rewrite C. fold sp.
-  rewrite <- (sp_val _ _ _ AG). unfold Mach.chunk_of_type in F. rewrite F. auto. 
+  rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. 
   simpl. auto.
   simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). 
   rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index fafd1d5..a506bed 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -206,27 +206,19 @@ let print_location oc loc =
 
 let cfi_startproc oc =
   if Configuration.asm_supports_cfi then
-    match config with
-    | Linux -> fprintf oc "	.cfi_startproc\n"
-    | Diab  -> assert false
+    fprintf oc "	.cfi_startproc\n"
 
 let cfi_endproc oc =
   if Configuration.asm_supports_cfi then
-    match config with
-    | Linux -> fprintf oc "	.cfi_endproc\n"
-    | Diab  -> assert false
+    fprintf oc "	.cfi_endproc\n"
 
 let cfi_adjust oc delta =
   if Configuration.asm_supports_cfi then
-    match config with
-    | Linux -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
-    | Diab  -> assert false
+    fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
 
 let cfi_rel_offset oc reg ofs =
   if Configuration.asm_supports_cfi then
-    match config with
-    | Linux -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs
-    | Diab  -> assert false
+    fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs
 
 (* Built-ins.  They come in two flavors: 
    - annotation statements: take their arguments in registers or stack
@@ -237,9 +229,15 @@ let cfi_rel_offset oc reg ofs =
 
 (* Handling of annotations *)
 
+let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
+
 let print_annot_stmt oc txt targs args =
-  fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_stmt preg "sp" oc txt targs args
+  if Str.string_match re_file_line txt 0 then begin
+    print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt)
+  end else begin
+    fprintf oc "%s annotation: " comment;
+    PrintAnnot.print_annot_stmt preg "sp" oc txt targs args
+  end
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
-- 
cgit v1.2.3