powerpc/: new unary operation "addsymbol"

Support far-data addressing in sections.
(Currently ignored in checklink.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 10 insertions, 9 deletions

diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index a31378e..3c0c9f1 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -20,19 +20,20 @@ open Camlcoq
 
 (* #pragma section *)
 
-let sda_supported =
-  match Configuration.arch, Configuration.system with
-  | "powerpc", "linux" -> true
-  | "powerpc", "diab"  -> true
-  | _, _ -> false
-
 let process_section_pragma classname istring ustring addrmode accmode =
   Sections.define_section classname
     ?iname: (if istring = "" then None else Some istring)
     ?uname: (if ustring = "" then None else Some ustring)
-    ?writable: (if accmode = "" then None else Some(String.contains accmode 'W'))
-    ?executable: (if accmode = "" then None else Some(String.contains accmode 'X'))
-    ?near: (if addrmode = "" then None else Some(sda_supported && addrmode = "near-data"))
+    ?writable:
+      (if accmode = "" then None else Some(String.contains accmode 'W'))
+    ?executable:
+      (if accmode = "" then None else Some(String.contains accmode 'X'))
+    ?access:
+      (match addrmode with
+       | "" -> None
+       | "near-data" -> Some Sections.Access_near
+       | "far-data" -> Some Sections.Access_far
+       | _ -> Some Sections.Access_default)
     ()
 
 (* #pragma use_section *)