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
---
 ia32/PrintAsm.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'ia32')

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index d30c856..56e837d 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -529,6 +529,9 @@ let print_builtin_inline oc name args res =
         fprintf oc "	movl	%a, %a\n" ireg a2 ireg tmp;
       fprintf oc "	bswap	%a\n" ireg tmp;
       fprintf oc "	movl	%a, 0(%a)\n" ireg tmp ireg a1
+  (* Synchronization *)
+  | "__builtin_membar", [], _ ->
+      ()
   (* Vararg stuff *)
   | "__builtin_va_start", [IR a], _ ->
       print_builtin_va_start oc a
-- 
cgit v1.2.3