Experiment: support a subset of GCC's extended asm statements.

25 files changed, 341 insertions, 63 deletions

diff --git a/.depend b/.depend
index 0f786903..7f4bee68 100644
--- a/.depend
+++ b/.depend
@@ -36,7 +36,7 @@ $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)
 backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
 backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo common/Globalenvs.vo
 backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo common/Switch.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo
-$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
+$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
 backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo
 backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo
 backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo
@@ -60,12 +60,12 @@ $(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)
 backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo
 $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo
 backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo
-$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo
+$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo
 backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo
 backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo
 $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/CSEdomain.vo
 backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/CSEdomain.vo backend/Kildall.vo $(ARCH)/CombineOp.vo
-$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo
+$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo
 backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo
 backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: backend/NeedDomain.v lib/Coqlib.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Registers.vo backend/ValueDomain.vo $(ARCH)/Op.vo backend/RTL.vo
 $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo
@@ -73,12 +73,12 @@ backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend
 backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo
 backend/Unusedglob.vo backend/Unusedglob.glob backend/Unusedglob.v.beautified: backend/Unusedglob.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo common/Errors.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo
 backend/Unusedglobproof.vo backend/Unusedglobproof.glob backend/Unusedglobproof.v.beautified: backend/Unusedglobproof.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Unusedglob.vo
-$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo
+$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo
 backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo
 $(ARCH)/Conventions1.vo $(ARCH)/Conventions1.glob $(ARCH)/Conventions1.v.beautified: $(ARCH)/Conventions1.v lib/Coqlib.vo common/AST.vo common/Events.vo backend/Locations.vo
 backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/Conventions1.vo
 backend/LTL.vo backend/LTL.glob backend/LTL.v.beautified: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo
-backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo
+backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo
 backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo
 backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo
 backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
@@ -94,10 +94,10 @@ $(ARCH)/Stacklayout.vo $(ARCH)/Stacklayout.glob $(ARCH)/Stacklayout.v.beautified
 backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Lineartyping.vo
 backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Stacking.vo
 $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/Stacklayout.vo backend/Conventions.vo
-$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
+$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
 backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
+$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo backend/Asmgenproof0.vo
+$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo
 cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo
 cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Errors.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
@@ -107,7 +107,7 @@ cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified
 cfrontend/Cexec.vo cfrontend/Cexec.glob cfrontend/Cexec.v.beautified: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo
 cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo
 cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
-cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo
+cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo
 cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
 cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob cfrontend/SimplExprproof.v.beautified: cfrontend/SimplExprproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
 cfrontend/Clight.vo cfrontend/Clight.glob cfrontend/Clight.v.beautified: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 17aa5115..00de4df7 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -55,3 +55,7 @@ let builtins = {
 
 let size_va_list = 4
 let va_list_scalar = true
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "[%s, #0]" arg
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index df17e595..913bff9e 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -1003,9 +1003,9 @@ module Target (Opt: PRINTER_OPTIONS) : 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);
+              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment;
               5 (* hoping this is an upper bound...  *)
           | _ ->
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 69b70e72..bcfa4548 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -60,7 +60,7 @@ let mkef sg toks =
       if sg.sig_args = [] then raise Parsing.Parse_error;
       EF_annot_val(intern_string txt, List.hd sg.sig_args)
   | [EFT_tok "inline_asm"; EFT_string txt] ->
-      EF_inline_asm(intern_string txt)
+      EF_inline_asm(intern_string txt, sg)
   | _ ->
       raise Parsing.Parse_error
 
diff --git a/backend/CSE.v b/backend/CSE.v
index 2c0c5f33..9f295402 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -476,7 +476,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
           empty_numbering
       | Ibuiltin ef args res s =>
           match ef with
-          | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ =>
+          | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ =>
               empty_numbering
           | EF_builtin _ _ | EF_vstore _ | EF_vstore_global _ _ _ =>
               set_unknown (kill_all_loads before) res
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index 995f22dd..88f5d8d6 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -148,7 +148,29 @@ let print_annot_val print_preg oc txt args =
   print_annot_text print_preg "<internal error>" oc txt
     (List.map (fun r -> AA_base r) args)
 
-(* Print CompCert version and command-line as asm comment *)
+(** Inline assembly *)
+
+let re_asm_param = Str.regexp "%%\\|%[0-9]+"
+
+let print_inline_asm print_preg oc txt sg args res =
+  let operands =
+    if sg.sig_res = None then args else res @ args in
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_preg oc (List.nth operands n)
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_asm_param txt);
+  fprintf oc "\n"
+
+
+(** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
   fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index fd10efb4..7413c443 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -831,6 +831,97 @@ and convertExprList env el =
   | [] -> Enil
   | e1 :: el' -> Econs(convertExpr env e1, convertExprList env el')
 
+(** ** Extended assembly *)
+
+module StringMap = Map.Make(String)
+
+let re_asm_placeholder =
+  Str.regexp "\\(%[0-9]+\\|%\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\|%%\\)"
+
+let convertAsm env txt outputs inputs clobber =
+
+  (* On the fly renaming of labeled and numbered arguments *)
+  let name_of_label lbl pos =
+    match lbl with
+    | None   -> sprintf "%%%d" pos
+    | Some l -> sprintf "%%[%s]" l in
+  let set_label_reg lbl pos pos' subst =
+    StringMap.add (name_of_label lbl pos) (sprintf "%%%d" pos') subst
+  and set_label_mem lbl pos pos' subst =
+    StringMap.add (name_of_label lbl pos)
+                  (CBuiltins.asm_mem_argument (sprintf "%%%d" pos'))
+                  subst
+  and set_label_const lbl pos n subst =
+    StringMap.add (name_of_label lbl pos) (sprintf "%Ld" n) subst in
+
+  (* Fix up the input expressions:
+      - add "&" for inputs of kind "m"
+      - evaluate constants for inputs of kind "i" *)
+  let rec fixupInputs accu pos pos' subst = function
+  | [] ->
+      (List.rev accu, subst)
+  | (lbl, cstr, e) :: inputs ->
+      match cstr with
+      | "r" | "rm" ->
+        fixupInputs (e :: accu) (pos + 1) (pos' + 1)
+                    (set_label_reg lbl pos pos' subst) inputs
+      | "m" | "o" ->
+        fixupInputs (Cutil.eaddrof e :: accu) (pos + 1) (pos' + 1)
+                    (set_label_mem lbl pos pos' subst) inputs
+      | "i" | "n" ->
+        let n =
+          match Ceval.integer_expr env e with
+          | Some n -> n
+          | None -> error "asm argument of kind 'i'/'n' is not a constant"; 0L in
+        fixupInputs accu (pos + 1) pos'
+                    (set_label_const lbl pos n subst) inputs
+      | _ ->
+        unsupported ("asm argument of kind '" ^ cstr ^ "'");
+        ([], subst) in
+  
+  (* Check the output expressions *)
+  let (output', ty_res, (inputs', subst)) =
+    match outputs with
+    | [] ->
+        (None, TVoid [], fixupInputs [] 0 0 StringMap.empty inputs)
+    | [(lbl, cstr, e)] ->
+        if not (cstr = "=r" || cstr = "=rm") then
+          unsupported ("asm result of kind '" ^ cstr ^ "'");
+        (Some e, e.etyp,
+         fixupInputs [] 1 1 (set_label_reg lbl 0 0 StringMap.empty) inputs)
+    | _ ->
+        error "asm statement with 2 or more results";
+        (None, TVoid [], ([], StringMap.empty)) in
+
+  (* Check the clobber list *)
+  List.iter
+    (fun c ->
+      if not (c = "memory" || c = "cc") then
+        unsupported ("asm register clobber '" ^ c ^ "'"))
+    clobber;
+
+  (* Rename the %[ident] and %nnn placeholders in the asm text *)
+  let txt' =
+    Str.global_substitute re_asm_placeholder 
+      (fun txt -> let s = Str.matched_group 1 txt in
+                  try StringMap.find s subst with Not_found -> s)
+      txt in
+
+  (* Build the Ebuiltin expression *)
+  let e = 
+    let tinputs = convertTypArgs env [] inputs' in
+    let toutput = convertTyp env ty_res in
+    Ebuiltin(EF_inline_asm(intern_string txt', 
+                           signature_of_type tinputs toutput cc_default),
+             tinputs,
+             convertExprList env inputs',
+             convertTyp env ty_res) in
+
+  (* Add an assignment to the output, if any *)
+  match output' with
+  | None -> e
+  | Some lhs -> Eassign (convertLvalue env lhs, e, typeof e)
+
 (* Separate the cases of a switch statement body *)
 
 type switchlabel =
@@ -940,11 +1031,11 @@ let rec convertStmt ploc env s =
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
       unsupported "inner declarations"; Sskip
-  | C.Sasm txt ->
+  | C.Sasm(attrs, txt, outputs, inputs, clobber) ->
       if not !Clflags.option_finline_asm then
         unsupported "inline 'asm' statement (consider adding option -finline-asm)";
       add_lineno ploc s.sloc
-        (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid)))
+        (Sdo (convertAsm env txt outputs inputs clobber))
 
 and convertSwitch ploc env is_64 = function
   | [] ->
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7c00ab47..487c0df6 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -405,18 +405,18 @@ Hypothesis do_external_function_complete:
   do_external_function id sg ge w vargs m = Some(w', t, vres, m').
 
 Variable do_inline_assembly:
-  ident -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
+  ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
 
 Hypothesis do_inline_assembly_sound:
-  forall txt ge vargs m t vres m' w w',
-  do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') ->
-  inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'.
+  forall txt sg ge vargs m t vres m' w w',
+  do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m') ->
+  inline_assembly_sem txt sg ge vargs m t vres m' /\ possible_trace w t w'.
 
 Hypothesis do_inline_assembly_complete:
-  forall txt ge vargs m t vres m' w w',
-  inline_assembly_sem txt ge vargs m t vres m' ->
+  forall txt sg ge vargs m t vres m' w w',
+  inline_assembly_sem txt sg ge vargs m t vres m' ->
   possible_trace w t w' ->
-  do_inline_assembly txt ge w vargs m = Some(w', t, vres, m').
+  do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m').
 
 Definition do_ef_volatile_load (chunk: memory_chunk)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
@@ -541,7 +541,7 @@ Definition do_external (ef: external_function):
   | EF_memcpy sz al => do_ef_memcpy sz al
   | EF_annot text targs => do_ef_annot text targs
   | EF_annot_val text targ => do_ef_annot_val text targ
-  | EF_inline_asm text => do_inline_assembly text ge
+  | EF_inline_asm text sg => do_inline_assembly text sg ge
   end.
 
 Lemma do_ef_external_sound:
diff --git a/common/AST.v b/common/AST.v
index d2926178..1e1e2b9d 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -584,7 +584,7 @@ Inductive external_function : Type :=
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident).
+  | EF_inline_asm (text: ident) (sg: signature).
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
@@ -606,7 +606,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
   | EF_annot text targs => mksignature targs None cc_default
   | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default
-  | EF_inline_asm text => mksignature nil None cc_default
+  | EF_inline_asm text sg => sg
   end.
 
 (** Whether an external function should be inlined by the compiler. *)
@@ -624,7 +624,7 @@ Definition ef_inline (ef: external_function) : bool :=
   | EF_memcpy sz al => true
   | EF_annot text targs => true
   | EF_annot_val text targ => true
-  | EF_inline_asm text => true
+  | EF_inline_asm text targs => true
   end.
 
 (** Whether an external function must reload its arguments. *)
diff --git a/common/Events.v b/common/Events.v
index 15bf4e12..62765fd3 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1449,10 +1449,10 @@ Axiom external_functions_properties:
 
 (** We treat inline assembly similarly. *)
 
-Parameter inline_assembly_sem: ident -> extcall_sem.
+Parameter inline_assembly_sem: ident -> signature -> extcall_sem.
 
 Axiom inline_assembly_properties:
-  forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default) nil.
+  forall id sg, extcall_properties (inline_assembly_sem id sg) sg nil.
 
 (** ** Combined semantics of external calls *)
 
@@ -1479,8 +1479,8 @@ Definition external_call (ef: external_function): extcall_sem :=
   | EF_free              => extcall_free_sem
   | EF_memcpy sz al      => extcall_memcpy_sem sz al
   | EF_annot txt targs   => extcall_annot_sem txt targs
-  | EF_annot_val txt targ=> extcall_annot_val_sem txt targ
-  | EF_inline_asm txt    => inline_assembly_sem txt
+  | EF_annot_val txt targ => extcall_annot_val_sem txt targ
+  | EF_inline_asm txt sg => inline_assembly_sem txt sg
   end.
 
 Theorem external_call_spec:
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 52aa963a..387bf261 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -53,7 +53,7 @@ let name_of_external = function
       sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al)
   | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text)
   | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (extern_atom text)
-  | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text)
+  | EF_inline_asm(text, sg) -> sprintf "inline_asm %S" (extern_atom text)
 
 let rec print_annot_arg px oc = function
   | AA_base x -> px oc x
diff --git a/cparser/C.mli b/cparser/C.mli
index 71ab1d4d..72e1f787 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -190,6 +190,10 @@ and init =
   | Init_struct of ident * (field * init) list
   | Init_union of ident * field * init
 
+(** GCC extended asm *)
+
+type asm_operand = string option * string * exp
+
 (** Statements *)
 
 type stmt = { sdesc: stmt_desc; sloc: location }
@@ -210,7 +214,7 @@ and stmt_desc =
   | Sreturn of exp option
   | Sblock of stmt list
   | Sdecl of decl
-  | Sasm of string
+  | Sasm of attributes * string * asm_operand list * asm_operand list * string list
 
 and slabel = 
   | Slabel of string
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 920f4603..6d9e95d5 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -180,6 +180,12 @@ Definition init_name_group := (list spec_elem * list init_name)%type.
 (* e.g.: int x, y; *)
 Definition name_group := (list spec_elem * list name)%type.
 
+(* GCC extended asm *)
+Inductive asm_operand :=
+| ASMOPERAND: option string -> bool -> list char_code -> expression -> asm_operand.
+
+Definition asm_flag := (bool * list char_code)%type.
+
 (*
 ** Declaration definition (at toplevel)
 *)
@@ -209,7 +215,7 @@ with statement :=
  | DEFAULT : statement -> cabsloc -> statement
  | LABEL : string -> statement -> cabsloc -> statement
  | GOTO : string -> cabsloc -> statement
- | ASM : bool -> list char_code -> cabsloc -> statement
+ | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> cabsloc -> statement
  | DEFINITION : definition -> statement (*definition or declaration of a variable or type*)
 
 with for_clause :=
diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml
index 9d4a91f6..5e6a19d0 100644
--- a/cparser/Cabshelper.ml
+++ b/cparser/Cabshelper.ml
@@ -70,7 +70,7 @@ begin
   | LABEL(_,_,loc) -> loc
   | GOTO(_,loc) -> loc
   | DEFINITION d -> get_definitionloc d
-  | ASM(_,_,loc) -> loc
+  | ASM(_,_,_,_,_,_,loc) -> loc
 end
 
 let string_of_cabsloc l =
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index ee8002d4..4ceaa016 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -364,6 +364,27 @@ let full_decl pp (sto, id, ty, int) =
   end;
   fprintf pp ";@]"
 
+let asm_operand pp (label, constr, e) =
+  begin match label with
+  | None -> ()
+  | Some l -> fprintf pp "[%s] " l
+  end;
+  fprintf pp "%a (%a)" const (CStr constr) exp (0, e)
+
+let asm_operands pp = function
+  | [] -> ()
+  | op1 :: ops ->
+      fprintf pp "@[<hov 0>%a" asm_operand op1;
+      List.iter (fun op -> fprintf pp ",@ %a" asm_operand op) ops;
+      fprintf pp "@]"
+
+let asm_flags pp = function
+  | [] -> ()
+  | fl1 :: fls ->
+      fprintf pp "@[<hov 0>%a" const (CStr fl1);
+      List.iter (fun fl -> fprintf pp ",@ %a" const (CStr fl)) fls;
+      fprintf pp "@]"
+
 exception Not_expr
 
 let rec exp_of_stmt s =
@@ -429,8 +450,21 @@ let rec stmt pp s =
       fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s
   | Sdecl d ->
       full_decl pp d
-  | Sasm txt ->
-      fprintf pp "asm(%a);" const (CStr txt)
+  | Sasm(attrs, txt, [], [], []) ->
+      fprintf pp "asm%a(%a);" attributes attrs const (CStr txt)
+  | Sasm(attrs, txt, outputs, inputs, []) ->
+      fprintf pp "asm%a(@[<hov 0>%a@ :%a@ :%a@]);"
+                 attributes attrs
+                 const (CStr txt)
+                 asm_operands outputs
+                 asm_operands inputs
+  | Sasm(attrs, txt, outputs, inputs, flags) ->
+      fprintf pp "asm%a(@[<hov 0>%a@ :%a@ :%a@ : %a@]);"
+                 attributes attrs
+                 const (CStr txt)
+                 asm_operands outputs
+                 asm_operands inputs
+                 asm_flags flags
 
 and slabel pp = function
   | Slabel s ->
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 612103a6..a1dd552b 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -270,6 +270,11 @@ let elab_constant loc = function
   | CONST_STRING(wide, s) ->
       elab_string_literal loc wide s
 
+let elab_simple_string loc wide chars =
+  match elab_string_literal loc wide chars with
+  | CStr s -> s
+  | _ -> error loc "wide character string not allowed here"; ""
+
 
 (** * Elaboration of type expressions, type specifiers, name declarations *)
 
@@ -498,13 +503,16 @@ and elab_cvspec env = function
   | CV_RESTRICT -> [ARestrict]
   | CV_ATTR attr -> elab_attribute env attr
 
+and elab_cvspecs env cv_specs =
+  List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs)
+
 (* Elaboration of a type declarator.  C99 section 6.7.5. *)
 
 and elab_type_declarator loc env ty = function
   | Cabs.JUSTBASE ->
       (ty, env)
   | Cabs.ARRAY(d, cv_specs, sz) ->
-      let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in
+      let a = elab_cvspecs env cv_specs in
       let sz' =
         match sz with
         | None ->
@@ -520,7 +528,7 @@ and elab_type_declarator loc env ty = function
                 Some 1L in (* produces better error messages later *)
        elab_type_declarator loc env (TArray(ty, sz', a)) d
   | Cabs.PTR(cv_specs, d) ->
-      let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in
+      let a = elab_cvspecs env cv_specs in
       elab_type_declarator loc env (TPtr(ty, a)) d
   | Cabs.PROTO(d, (params, vararg)) ->
        begin match unroll env ty with
@@ -1933,6 +1941,13 @@ and elab_definitions local env = function
       let (decl2, env2) = elab_definitions local env1 dl in
       (decl1 @ decl2, env2)
 
+(* Extended asm *)
+
+let elab_asm_operand loc env (ASMOPERAND(label, wide, chars, e)) =
+  let s = elab_simple_string loc wide chars in
+  let e' = elab_expr loc env e in
+  (label, s, e')
+
 
 (* Contexts for elaborating statements *)
 
@@ -2118,14 +2133,14 @@ let rec elab_stmt env ctx s =
       { sdesc = Sskip; sloc = elab_loc loc }
 
 (* Traditional extensions *)
-  | ASM(wide, chars, loc) ->
-      begin match elab_string_literal loc wide chars with
-      | CStr s ->
-          { sdesc = Sasm s; sloc = elab_loc loc }
-      | _ ->
-          error loc "wide strings not supported in asm statement";
-          sskip
-      end
+  | ASM(cv_specs, wide, chars, outputs, inputs, flags, loc) ->
+      let a = elab_cvspecs env cv_specs in
+      let s = elab_simple_string loc wide chars in
+      let outputs = List.map (elab_asm_operand loc env) outputs in
+      let inputs = List.map (elab_asm_operand loc env) inputs in
+      let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in
+      { sdesc = Sasm(a, s, outputs, inputs, flags);
+        sloc = elab_loc loc }
 
 (* Unsupported *)
   | DEFINITION def ->
diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index a058a8d1..7c0bfb55 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -97,6 +97,12 @@ Require Import List.
 %type<gcc_attribute_word> gcc_attribute_word
 %type<name * list string> old_function_declarator direct_old_function_declarator
 %type<list string (* Reverse order *)> identifier_list
+%type<list asm_flag> asm_flags
+%type<option string> asm_op_name
+%type<asm_operand> asm_operand
+%type<list asm_operand> asm_operands asm_operands_ne
+%type<list asm_operand * list asm_operand * list asm_flag> asm_arguments
+%type<list cvspec> asm_attributes
 
 %start<list definition> translation_unit_file
 %%
@@ -820,10 +826,50 @@ jump_statement:
 
 (* Non-standard *)
 asm_statement:
-| loc = ASM LPAREN template = STRING_LITERAL RPAREN SEMICOLON
-    { let '(wide, chars, _) := template in ASM wide chars loc }
-| loc = ASM VOLATILE LPAREN template = STRING_LITERAL RPAREN SEMICOLON
-    { let '(wide, chars, _) := template in ASM wide chars loc }
+| loc = ASM attr = asm_attributes LPAREN template = STRING_LITERAL args = asm_arguments RPAREN SEMICOLON
+    { let '(wide, chars, _) := template in
+      let '(outputs, inputs, flags) := args in
+      ASM attr wide chars outputs inputs flags loc }
+
+asm_attributes:
+| /* empty */
+     { [] }
+| CONST attr = asm_attributes
+     { CV_CONST :: attr }
+| VOLATILE attr = asm_attributes 
+     { CV_VOLATILE :: attr }
+
+asm_arguments:
+| /* empty */
+     { ([], [], []) }
+| COLON o = asm_operands
+     { (o, [], []) }
+| COLON o = asm_operands COLON i = asm_operands
+     { (o, i, []) }
+| COLON o = asm_operands COLON i = asm_operands COLON f = asm_flags
+     { (o, i, f) }
+
+asm_operands:
+| /* empty */                                   { [] }
+| ol = asm_operands_ne                          { rev' ol }
+
+asm_operands_ne:
+| ol = asm_operands_ne COMMA o = asm_operand    { o :: ol }
+| o = asm_operand                               { [o] }
+
+asm_operand:
+| n = asm_op_name cstr = STRING_LITERAL LPAREN e = expression RPAREN
+    { let '(wide, s, loc) := cstr in ASMOPERAND n wide s (fst e) }
+
+asm_op_name:
+| /* empty */                         { None }
+| LBRACK n = OTHER_NAME RBRACK        { Some (fst n) }
+
+asm_flags:
+| f = STRING_LITERAL
+    { let '(wide, s, loc) := f in (wide, s) :: nil }
+| f = STRING_LITERAL COMMA fl = asm_flags
+    { let '(wide, s, loc) := f in (wide, s) :: fl }
 
 (* 6.9 *)
 translation_unit_file:
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 2b7ec2ca..0d533b56 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -150,6 +150,8 @@ let decl env (sto, id, ty, int) =
     match int with None -> None | Some i -> Some(init env' i)),
    env')
 
+let asm_operand env (lbl, cstr, e) = (lbl, cstr, exp env e)
+
 let rec stmt env s =
   { sdesc = stmt_desc env s.sdesc; sloc = s.sloc }
 
@@ -170,7 +172,11 @@ and stmt_desc env = function
   | Sreturn a -> Sreturn (optexp env a)
   | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl'
   | Sdecl d -> assert false
-  | Sasm txt -> Sasm txt
+  | Sasm(attr, txt, outputs, inputs, flags) ->
+       Sasm(attr, txt,
+            List.map (asm_operand env) outputs,
+            List.map (asm_operand env) inputs,
+            flags)
 
 and stmt_or_decl env s =
   match s.sdesc with
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index ef356d3a..44a06f8a 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -616,7 +616,43 @@ jump_statement:
     {}
 
 asm_statement:
-| ASM VOLATILE? LPAREN string_literals_list RPAREN SEMICOLON
+| ASM asm_attributes LPAREN string_literals_list asm_arguments RPAREN SEMICOLON
+    {}
+
+asm_attributes:
+| /* empty */
+| CONST asm_attributes    
+| VOLATILE asm_attributes
+    {}
+
+asm_arguments:
+| /* empty */
+| COLON asm_operands
+| COLON asm_operands COLON asm_operands
+| COLON asm_operands COLON asm_operands COLON asm_flags
+    {}
+
+asm_operands:
+| /* empty */
+| asm_operands_ne
+    {}
+
+asm_operands_ne:
+| asm_operands_ne COMMA asm_operand
+| asm_operand
+    {}
+
+asm_operand:
+| asm_op_name string_literals_list LPAREN expression RPAREN
+    {}
+
+asm_op_name:
+| /*empty*/                             {}
+| LBRACK i = general_identifier RBRACK  { set_id_type i OtherId }
+
+asm_flags:
+| string_literals_list
+| string_literals_list COMMA asm_flags
     {}
 
 translation_unit_file:
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 2725dbfe..b16d2cae 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -397,7 +397,7 @@ let do_external_function id sg ge w args m =
   | _ ->
       None
 
-let do_inline_assembly txt ge w args m = None
+let do_inline_assembly txt sg ge w args m = None
 
 (* Implementing external functions producing observable events *)
 
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index 765f5b18..b1be612b 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -70,3 +70,7 @@ let builtins = {
 
 let size_va_list = 4
 let va_list_scalar = true
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "0(%s)" arg
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
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 47895cb1..fbe5f782 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -523,7 +523,7 @@ let expand_instruction instr =
           expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
       | EF_annot_val(txt, targ) ->
           expand_annot_val txt targ args res
-      | EF_inline_asm txt ->
+      | EF_inline_asm(txt, sg) ->
           emit instr
       | _ ->
           assert false
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 8840d2c3..222a4d94 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -90,3 +90,7 @@ let builtins = {
 
 let size_va_list = 12
 let va_list_scalar = false
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "0(%s)" arg
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index b3d228b3..49954998 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -284,10 +284,14 @@ module Target (System : SYSTEM):TARGET =
     let ireg_or_zero oc r =
       if r = GPR0 then output_string oc "0" else ireg oc r
 
-    (* [preg] is only used for printing annotations.
-       Use the full register names [rN] and [fN] to avoid
-       ambiguity with constants. *)
     let preg oc = function
+      | IR r -> ireg oc r
+      | FR r -> freg oc r
+      | _    -> assert false
+
+    (* For printing annotations, use the full register names [rN] and [fN]
+       to avoid ambiguity with constants. *)
+    let preg_annot oc = function
       | IR r -> fprintf oc "r%s" (int_reg_name r)
       | FR r -> fprintf oc "f%s" (float_reg_name r)
       | _    -> assert false
@@ -327,7 +331,7 @@ module Target (System : SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
+        PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args
       end
 
     (* Determine if the displacement of a conditional branch fits the short form *)
@@ -646,9 +650,10 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "%a:\n" label (transl_label lbl)
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | 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