From 1b5db339bb05f773a6a132be4c0b8cea54d50461 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 17 Apr 2015 16:30:43 +0200 Subject: Experiment: support a subset of GCC's extended asm statements. --- ia32/TargetPrinter.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 58b7aa37..7e9471a5 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -871,9 +871,10 @@ module Target(System: SYSTEM):TARGET = (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 -> + | EF_inline_asm(txt, sg) -> fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); + fprintf oc "\t"; + PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false -- cgit