Add __builtin_bswap16 and __builtin_bswap32 to all ports.

Remove __builtin_{read,write}_reversed from IA32 and ARM ports.
Machregs: tighten destroyed_by_builtin
Packedstructs: use bswap if read/write-reversed not available.


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

1 files changed, 5 insertions, 10 deletions

diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index 596d291..4a3dde5 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -23,21 +23,16 @@ let builtins = {
     (* Integer arithmetic *)
     "__builtin_bswap",
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
+    "__builtin_bswap32",
+      (TInt(IUInt, []), [TInt(IUInt, [])], false);
+    "__builtin_bswap16",
+      (TInt(IUShort, []), [TInt(IUShort, [])], false);
     (* Float arithmetic *)
     "__builtin_fsqrt",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     "__builtin_fmax",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmin",
-      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
-    (* Memory accesses *)
-    "__builtin_read16_reversed",
-      (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
-    "__builtin_read32_reversed",
-      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
-    "__builtin_write16_reversed",
-      (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
-    "__builtin_write32_reversed",
-      (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
+      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false)
   ]
 }