Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,

for compatibility with earlier CompCert versions.
But don't use them in PackedStructs.


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

1 files changed, 10 insertions, 1 deletions

diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index 4a3dde5..cbd5998 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -33,6 +33,15 @@ let builtins = {
     "__builtin_fmax",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmin",
-      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false)
+      (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);
   ]
 }