From 0486654fac91947fec93d18a0738dd7aa10bcf96 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 3 Nov 2009 08:43:54 +0000
Subject: PowerPC/EABI port: preliminary support for #pragma section and  
 #pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts
 of extraction/extraction.v into    <arch>/extractionMachdep.v

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/PrintAsm.ml | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

(limited to 'powerpc/PrintAsm.ml')

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 95074988..539d9894 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -192,9 +192,9 @@ let (text, data, const_data, sdata, float_literal) =
   | Diab ->
       (".text",
        ".data",
-       ".data",  (* to check *)
-       ".sdata", (* to check *)
-       ".data")  (* to check *)
+       ".data", (* or: .rodata? *)
+       ".sdata",  (* to check *)
+       ".data")  (* or: .rodata? *)
 
 (* Encoding masks for rlwinm instructions *)
 
@@ -480,7 +480,10 @@ let rec labels_of_code = function
 
 let print_function oc name code =
   Hashtbl.clear current_function_labels;
-  section oc text;
+  section oc
+    (match CPragmas.section_for_atom name true with
+     | Some s -> ".section\t" ^ s
+     | None -> text);
   fprintf oc "	.align 2\n";
   if not (Cil2Csyntax.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
@@ -692,13 +695,19 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   match init_data with
   | [] -> ()
   | _  ->
+      let init =
+        match init_data with [Init_space _] -> false | _ -> true in
       let sec =
-        if Cil2Csyntax.atom_is_small_data name (coqint_of_camlint 0l) then
-          sdata
-        else if Cil2Csyntax.atom_is_readonly name then
-          const_data
-        else
-          data in
+        match CPragmas.section_for_atom name init with
+        | Some s -> ".section\t" ^ s
+        | None ->
+            if CPragmas.atom_is_small_data name (coqint_of_camlint 0l) then
+              sdata
+            else if Cil2Csyntax.atom_is_readonly name then
+              const_data
+            else
+              data
+      in
       section oc sec;
       fprintf oc "	.align	3\n";
       if not (Cil2Csyntax.atom_is_static name) then
-- 
cgit