From ac69dfdd1d7acc64035c70177f0c04b72627ed2e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 20 Aug 2014 13:02:53 +0000
Subject: Add some more synchronization builtins

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/CBuiltins.ml | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'arm/CBuiltins.ml')

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 4446ab27..daeabdaa 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -44,10 +44,28 @@ let builtins = {
     "__builtin_write32_reversed",
       (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
     (* Synchronization *)
+    "__builtin_dmb",
+      (TVoid [], [], false);
     "__builtin_dsb",
       (TVoid [], [], false);
     "__builtin_isb",
-      (TVoid [], [], false)
+      (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, [AConst]), []); TInt(IUInt, [])], false);
+    "__builtin_strexb",
+      (TInt(IInt, []), [TPtr(TInt(IUChar, [AConst]), []); TInt(IUChar, [])], false);
+    "__builtin_strexh",
+      (TInt(IInt, []), [TPtr(TInt(IUShort, [AConst]), []); TInt(IUShort, [])], false);
+    "__builtin_strexd",
+      (TInt(IInt, []), [TPtr(TInt(IULongLong, [AConst]), []); TInt(IULongLong, [])], false);
   ]
 }
 
-- 
cgit