From 21e269ee37b934428306f53dda0495fee30dd8fa Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 28 Jul 2014 14:29:42 +0000
Subject: All targets: add __builtin_membar ARM: add __builtin_dsb
 __builtin_isb

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/C2C.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'cfrontend')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index e7d8337..6ee217c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -92,6 +92,11 @@ let builtins_generic = {
         (TInt(IInt, []),
           [TPtr(TInt(IChar, [AConst]), []); TInt(IInt, [])],
           false);
+    (* Software memory barrier *)
+    "__builtin_membar",
+        (TVoid [],
+          [],
+          false);
     (* Variable arguments *)
 (* va_start(ap,n)
       (preprocessing) --> __builtin_va_start(ap, arg)
-- 
cgit v1.2.3