Cold feet: suppress builtins for load with reservation/store conditional, use case is unclear.

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

1 files changed, 1 insertions, 17 deletions

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 6f62bed..17aa511 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -49,23 +49,7 @@ let builtins = {
     "__builtin_dsb",
       (TVoid [], [], false);
     "__builtin_isb",
-      (TVoid [], [], false);
-    "__builtin_ldrex",
-      (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
-    "__builtin_ldrexb",
-      (TInt(IUChar, []), [TPtr(TInt(IUChar, [AConst]), [])], false);
-    "__builtin_ldrexh",
-      (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
-    "__builtin_ldrexd",
-      (TInt(IULongLong, []), [TPtr(TInt(IULongLong, [AConst]), [])], false);
-    "__builtin_strex",
-      (TInt(IInt, []), [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
-    "__builtin_strexb",
-      (TInt(IInt, []), [TPtr(TInt(IUChar, []), []); TInt(IUChar, [])], false);
-    "__builtin_strexh",
-      (TInt(IInt, []), [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
-    "__builtin_strexd",
-      (TInt(IInt, []), [TPtr(TInt(IULongLong, []), []); TInt(IULongLong, [])], false);
+      (TVoid [], [], false)
   ]
 }