From 712f3cbae6bfd3c6f6cc40d44f438aa0affcd371 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 18 Dec 2012 07:54:35 +0000
Subject: Support for inline assembly (asm statements). cparser: add primitive
 support for enum types. bitfield emulation: for bitfields with enum type,
 choose signed/unsigned as appropriate

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/PrintAsm.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'ia32/PrintAsm.ml')

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 08bd2f5..da08de8 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -714,6 +714,10 @@ let print_instruction oc = function
                                   (Int32.to_int (camlint_of_coqint al)) args
       | EF_annot_val(txt, targ) ->
           print_annot_val oc (extern_atom txt) args res
+      | EF_inline_asm txt ->
+          fprintf oc "%s begin inline assembly\n" comment;
+          fprintf oc "	%s\n" (extern_atom txt);
+          fprintf oc "%s end inline assembly\n" comment
       | _ ->
           assert false
       end
-- 
cgit v1.2.3