From 61f6aed04b846b174126d4b1cec28f6f1da20e52 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 17 May 2013 09:17:48 +0000
Subject: Update PowerPC port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2255 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/Asmgenproof.v |  2 +-
 powerpc/PrintAsm.ml   | 20 +++++++++++++-------
 2 files changed, 14 insertions(+), 8 deletions(-)

(limited to 'powerpc')

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 37c8808..e723c86 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -903,7 +903,7 @@ Local Transparent destroyed_by_jumptable.
   intros [m1' [C D]].
   exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. 
   intros [m2' [F G]].
-  simpl Mach.chunk_of_type in F. 
+  simpl chunk_of_type in F. 
   exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. 
   intros [m3' [P Q]].
   (* Execution of function prologue *)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 07ed87c..dd0ec1f 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -230,25 +230,25 @@ let print_location oc loc =
 
 let cfi_startproc oc =
   if Configuration.asm_supports_cfi then
-    match config with
+    match target with
     | Linux -> fprintf oc "	.cfi_startproc\n"
     | Diab  -> assert false
 
 let cfi_endproc oc =
   if Configuration.asm_supports_cfi then
-    match config with
+    match target with
     | Linux -> fprintf oc "	.cfi_endproc\n"
     | Diab  -> assert false
 
 let cfi_adjust oc delta =
   if Configuration.asm_supports_cfi then
-    match config with
+    match target with
     | Linux -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
     | Diab  -> assert false
 
 let cfi_rel_offset oc reg ofs =
   if Configuration.asm_supports_cfi then
-    match config with
+    match target with
     | Linux -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs
     | Diab  -> assert false
 
@@ -283,9 +283,15 @@ let rolm_mask n =
 
 (* 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 "R1" 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 "R1" oc txt targs args
+  end
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
@@ -526,7 +532,7 @@ let print_builtin_inline oc name args res =
       fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13 ireg GPR1;
       cfi_adjust oc 8l;
       fprintf oc "	lwz	%a, 4(%a)\n" ireg res ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1
+      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
       cfi_adjust oc (-8l)
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
-- 
cgit v1.2.3