PowerPC: remove the fmadd and fmsub operators/Asm instructions

  (definitely not semantics-preserving; hard to justify).
CPragmas: make sure SDAs are not recognized on MacOSX.


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

1 files changed, 7 insertions, 1 deletions

diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 6fa6d5c..4b4c0f1 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -21,13 +21,19 @@ open Cparser
 
 (* #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(addrmode = "near-data"))
+    ?near: (if addrmode = "" then None else Some(sda_supported && addrmode = "near-data"))
     ()
 
 (* #pragma use_section *)