Add option -Os to optimize for code size rather than for execution speed.

Refactored compilation flags that affect the Coq part (module Compopts).
Added support for C99 for loops with declarations.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

31 files changed, 215 insertions, 97 deletions

diff --git a/.depend b/.depend
index 2b18734..8c02175 100644
--- a/.depend
+++ b/.depend
@@ -35,7 +35,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 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
 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 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 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 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
@@ -44,7 +44,7 @@ backend/RTL.vo backend/RTL.glob backend/RTL.v.beautified: backend/RTL.v lib/Coql
 backend/RTLgen.vo backend/RTLgen.glob backend/RTLgen.v.beautified: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo
 backend/RTLgenspec.vo backend/RTLgenspec.glob backend/RTLgenspec.v.beautified: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo
 backend/RTLgenproof.vo backend/RTLgenproof.glob backend/RTLgenproof.v.beautified: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo
-backend/Tailcall.vo backend/Tailcall.glob backend/Tailcall.v.beautified: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo
+backend/Tailcall.vo backend/Tailcall.glob backend/Tailcall.v.beautified: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo
 backend/Tailcallproof.vo backend/Tailcallproof.glob backend/Tailcallproof.v.beautified: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo
 backend/Inlining.vo backend/Inlining.glob backend/Inlining.v.beautified: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo
 backend/Inliningspec.vo backend/Inliningspec.glob backend/Inliningspec.v.beautified: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo
@@ -54,23 +54,23 @@ backend/Renumberproof.vo backend/Renumberproof.glob backend/Renumberproof.v.beau
 backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo common/Subtyping.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Memory.vo common/Events.vo backend/RTL.vo backend/Conventions.vo
 backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo
 backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo
-backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.v lib/Coqlib.vo lib/Maps.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 backend/RTL.vo
-$(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.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/ValueDomain.vo backend/RTL.vo
-backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.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
+backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.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 backend/RTL.vo
+$(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.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 $(ARCH)/Op.vo backend/ValueDomain.vo backend/RTL.vo
+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 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 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 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
+$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.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 $(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
 backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo
 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
-$(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)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.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)/$(VARIANT)/Conventions1.vo
@@ -91,10 +91,10 @@ $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob $(ARCH)/$(
 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)/$(VARIANT)/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)/$(VARIANT)/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)/$(VARIANT)/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 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 cfrontend/Ctypes.vo cfrontend/Cop.vo
@@ -115,6 +115,7 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob cfrontend/Cshmgenproof.v.b
 cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob cfrontend/Csharpminor.v.beautified: cfrontend/Csharpminor.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 backend/Cminor.vo common/Smallstep.vo
 cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob cfrontend/Cminorgen.v.beautified: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo cfrontend/Csharpminor.vo backend/Cminor.vo
 cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob cfrontend/Cminorgenproof.v.beautified: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.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 common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
+driver/Compopts.vo driver/Compopts.glob driver/Compopts.v.beautified: driver/Compopts.v
 driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo
 driver/Complements.vo driver/Complements.glob driver/Complements.v.beautified: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
 flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob flocq/Core/Fcore_Raux.v.beautified: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo
diff --git a/Changelog b/Changelog
index d02866a..8984ee8 100644
--- a/Changelog
+++ b/Changelog
@@ -27,6 +27,8 @@ Language features:
   just as the last case.
 - Support for incomplete array as last field of a struct,
   as specified in ISO C 99.
+- Support for declarations within 'for' loops, as specified in ISO C 99.
+  (E.g. "for (int i = 0; i < 4; i++) ...")
 - Revised semantics and implementation of _Alignas(N) attribute
   to better match those of GCC and Clang.
 - Better tolerance for functions declared without prototypes
diff --git a/Makefile b/Makefile
index b527a8c..d206461 100644
--- a/Makefile
+++ b/Makefile
@@ -111,7 +111,7 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \
 
 # Putting everything together (in driver/)
 
-DRIVER=Compiler.v Complements.v
+DRIVER=Compopts.v Compiler.v Complements.v
 
 # All source files
 
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 0540781..bf08610 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -14,6 +14,7 @@
   and conditions.  This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index ad7dcd1..90e18f2 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for constant propagation (processor-dependent part). *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index c968213..037b22e 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 76d8e6c..d2c4d44 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -74,7 +74,7 @@ Definition transf_ros (ae: AE.t) (ros: reg + ident) : reg + ident :=
 Definition const_for_result (a: aval) : option operation :=
   match a with
   | I n => Some(Ointconst n)
-  | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
+  | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | Ptr(Gl symb ofs) => Some(Oaddrsymbol symb ofs)
   | Ptr(Stk ofs) => Some(Oaddrstack ofs)
   | _ => None
@@ -108,7 +108,7 @@ Fixpoint annot_strength_reduction
       let (targs'', args'') := annot_strength_reduction ae targs' args' in
       match ty, areg ae arg with
       | Tint, I n => (AA_int n :: targs'', args'')
-      | Tfloat, F n => if generate_float_constants tt
+      | Tfloat, F n => if Compopts.generate_float_constants tt
                        then (AA_float n :: targs'', args'')
                        else (AA_arg ty :: targs'', arg :: args'')
       | _, _ => (AA_arg ty :: targs'', arg :: args'')
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 41afe8c..d88d6e4 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
@@ -157,7 +158,7 @@ Proof.
 - (* integer *)
   inv H. inv H0. exists (Vint n); auto.
 - (* float *)
-  destruct (generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto.
+  destruct (Compopts.generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto.
 - (* pointer *)
   destruct p; try discriminate.
   + (* global *)
@@ -235,7 +236,7 @@ Proof.
     * exists eargs''; split; auto; simpl; f_equal; auto. 
       generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM.
       inv VM. rewrite <- H0 in *. inv H5; auto.
-    * destruct (generate_float_constants tt); inv H1; auto. 
+    * destruct (Compopts.generate_float_constants tt); inv H1; auto. 
       exists eargs''; split; auto; simpl; f_equal; auto. 
       generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM.
       inv VM. rewrite <- H0 in *. inv H5; auto.
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 1d9168c..938ce5d 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -13,6 +13,7 @@
 (** Instruction selection for division and modulus *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -77,10 +78,13 @@ Definition divuimm (e1: expr) (n2: int) :=
   match Int.is_power2 n2 with
   | Some l => shruimm e1 l
   | None =>
-      match divu_mul_params (Int.unsigned n2) with
-      | None => divu_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (divu_mul p m)
-      end
+      if optim_for_size tt then
+        divu_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divu_mul_params (Int.unsigned n2) with
+        | None => divu_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (divu_mul p m)
+        end
   end.
 
 Nondetfunction divu (e1: expr) (e2: expr) := 
@@ -96,10 +100,13 @@ Definition moduimm (e1: expr) (n2: int) :=
   match Int.is_power2 n2 with
   | Some l => andimm (Int.sub n2 Int.one) e1
   | None =>
-      match divu_mul_params (Int.unsigned n2) with
-      | None => modu_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
-      end
+      if optim_for_size tt then
+        modu_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divu_mul_params (Int.unsigned n2) with
+        | None => modu_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
+        end
   end.
 
 Nondetfunction modu (e1: expr) (e2: expr) := 
@@ -123,10 +130,13 @@ Definition divsimm (e1: expr) (n2: int) :=
       then shrximm e1 l
       else divs_base e1 (Eop (Ointconst n2) Enil)
   | None =>
-      match divs_mul_params (Int.signed n2) with
-      | None => divs_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (divs_mul p m)
-      end
+      if optim_for_size tt then
+        divs_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divs_mul_params (Int.signed n2) with
+        | None => divs_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (divs_mul p m)
+        end
   end.
 
 Nondetfunction divs (e1: expr) (e2: expr) := 
@@ -142,10 +152,13 @@ Definition modsimm (e1: expr) (n2: int) :=
       then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2)
       else mods_base e1 (Eop (Ointconst n2) Enil)
   | None =>
-      match divs_mul_params (Int.signed n2) with
-      | None => mods_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2)
-      end
+      if optim_for_size tt then
+        mods_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divs_mul_params (Int.signed n2) with
+        | None => mods_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2)
+        end
   end.
 
 Nondetfunction mods (e1: expr) (e2: expr) := 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 0719a5e..9228cde 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -369,10 +369,12 @@ Proof.
   replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). 
   apply eval_shruimm; auto.
   simpl. erewrite Int.is_power2_range; eauto. 
-- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
-  + exists (Vint (Int.divu i n2)); split; auto.
-    econstructor; eauto. eapply eval_divu_mul; eauto. 
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_divu_base; eauto. EvalOp.
+  + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+    * exists (Vint (Int.divu i n2)); split; auto.
+      econstructor; eauto. eapply eval_divu_mul; eauto. 
+    * eapply eval_divu_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_divu:
@@ -412,13 +414,15 @@ Proof.
   change (Vint (Int.and i (Int.sub n2 Int.one)))
     with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))).
   apply eval_andimm. auto.
-- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
-  + econstructor; split. 
-    econstructor; eauto. eapply eval_mod_from_div. 
-    eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. 
-    rewrite Int.modu_divu. auto. 
-    red; intros; subst n2; discriminate.
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_modu_base; eauto. EvalOp.
+  + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+    * econstructor; split. 
+      econstructor; eauto. eapply eval_mod_from_div. 
+      eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. 
+      rewrite Int.modu_divu. auto. 
+      red; intros; subst n2; discriminate.
+    * eapply eval_modu_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_modu:
@@ -485,10 +489,12 @@ Proof.
 - destruct (Int.ltu l (Int.repr 31)) eqn:LT31.
   + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto.
   + eapply eval_divs_base; eauto. EvalOp.
-- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
-  + exists (Vint (Int.divs i n2)); split; auto.
-    econstructor; eauto. eapply eval_divs_mul; eauto. 
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_divs_base; eauto. EvalOp.
+  + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
+    * exists (Vint (Int.divs i n2)); split; auto.
+      econstructor; eauto. eapply eval_divs_mul; eauto. 
+    * eapply eval_divs_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_divs:
@@ -524,12 +530,14 @@ Proof.
     apply eval_mod_from_div. eexact X. simpl; eauto. 
     simpl. auto.
   + eapply eval_mods_base; eauto. EvalOp.
-- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
-  + econstructor; split. 
-    econstructor. eauto. apply eval_mod_from_div with (x := i); auto.
-    eapply eval_divs_mul with (x := i); eauto.
-    simpl. auto.
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_mods_base; eauto. EvalOp.
+  + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
+    * econstructor; split. 
+      econstructor. eauto. apply eval_mod_from_div with (x := i); auto.
+      eapply eval_divs_mul with (x := i); eauto.
+      simpl. auto.
+    * eapply eval_mods_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_mods:
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 26beb34..25da531 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Registers.
 Require Import Op.
@@ -98,8 +99,6 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
   as explained above.  Moreover, we can turn tail calls off
   using a compilation option. *)
 
-Parameter eliminate_tailcalls: unit -> bool.
-
 Definition transf_function (f: function) : function :=
   if zeq f.(fn_stacksize) 0 && eliminate_tailcalls tt
   then RTL.transf_function (transf_instr f) f
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 77725cf..1965b18 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -13,6 +13,7 @@
 (** Recognition of tail calls: correctness proof *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index f580438..e293028 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -12,6 +12,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -74,7 +75,7 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func
   match classify_builtin ef args ae with
   | Builtin_vload chunk aaddr => 
       let a :=
-        if strict
+        if va_strict tt
         then vlub (loadv chunk rm am aaddr) (vnormalize chunk (Ifptr Glob))
         else vnormalize chunk Vtop in
       VA.State (AE.set res a ae) am
@@ -1255,11 +1256,11 @@ Proof.
   * (* true volatile access *)
     assert (V: vmatch bc v0 (Ifptr Glob)).
     { inv H4; constructor. econstructor. eapply GE; eauto. }
-    destruct strict. apply vmatch_lub_r. apply vnormalize_sound. auto. 
+    destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. 
     apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor.
   * (* normal memory access *)
     exploit loadv_sound; eauto. simpl; eauto. intros V.
-    destruct strict. 
+    destruct (va_strict tt). 
     apply vmatch_lub_l. auto.
     eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. 
 + (* volatile store *)
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index eee4762..239dd47 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -13,6 +13,7 @@
 Require Import Coqlib.
 Require Import Zwf.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -25,10 +26,6 @@ Require Import Kildall.
 Require Import Registers.
 Require Import RTL.
 
-Parameter strict: bool.
-Parameter propagate_float_constants: unit -> bool.
-Parameter generate_float_constants : unit -> bool.
-
 Inductive block_class : Type :=
   | BCinvalid
   | BCglob (id: ident)
@@ -819,7 +816,7 @@ Definition vlub (v w: aval) : aval :=
   | I i, Sgn n | Sgn n, I i =>
       sgn (Z.max (ssize i) n)
   | I i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i =>
-      if strict || Int.eq i Int.zero then Ifptr p else Vtop
+      if va_strict tt || Int.eq i Int.zero then Ifptr p else Vtop
   | Uns n1, Uns n2 => Uns (Z.max n1 n2)
   | Uns n1, Sgn n2 => sgn (Z.max (n1 + 1) n2)
   | Sgn n1, Uns n2 => sgn (Z.max n1 (n2 + 1))
@@ -837,7 +834,7 @@ Definition vlub (v w: aval) : aval :=
   | Ptr p1, Ifptr p2 => Ifptr(plub p1 p2)
   | Ifptr p1, Ptr p2 => Ifptr(plub p1 p2)
   | Ifptr p1, Ifptr p2 => Ifptr(plub p1 p2)
-  | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if strict then Ifptr p else Vtop
+  | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if va_strict tt then Ifptr p else Vtop
   | _, _ => Vtop
   end.
 
@@ -989,8 +986,8 @@ Lemma pmatch_vplub:
   forall b ofs x p, pmatch b ofs p -> pmatch b ofs (vplub x p).
 Proof.
   intros. 
-  assert (DFL: pmatch b ofs (if strict then p else Ptop)).
-  { destruct strict; auto. eapply pmatch_top'; eauto. }
+  assert (DFL: pmatch b ofs (if va_strict tt then p else Ptop)).
+  { destruct (va_strict tt); auto. eapply pmatch_top'; eauto. }
   unfold vplub; destruct x; auto; apply pmatch_lub_r; auto.
 Qed.
 
@@ -1495,7 +1492,7 @@ Definition divs (v w: aval) :=
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
       || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
-      then if strict then Vbot else itop
+      then if va_strict tt then Vbot else itop
       else I (Int.divs i1 i2)
   | _, _ => itop
   end.
@@ -1513,7 +1510,7 @@ Definition divu (v w: aval) :=
   match w, v with
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
-       then if strict then Vbot else itop
+       then if va_strict tt then Vbot else itop
       else I (Int.divu i1 i2)
   | _, _ => itop
   end.
@@ -1531,7 +1528,7 @@ Definition mods (v w: aval) :=
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
       || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
-      then if strict then Vbot else itop
+      then if va_strict tt then Vbot else itop
       else I (Int.mods i1 i2)
   | _, _ => itop
   end.
@@ -1549,7 +1546,7 @@ Definition modu (v w: aval) :=
   match w, v with
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
-      then if strict then Vbot else itop
+      then if va_strict tt then Vbot else itop
       else I (Int.modu i1 i2)
   | I i2, _ => uns (usize i2)
   | _, _ => itop
@@ -1693,7 +1690,7 @@ Definition intoffloat (x: aval) :=
   | F f =>
       match Float.intoffloat f with
       | Some i => I i
-      | None => if strict then Vbot else itop
+      | None => if va_strict tt then Vbot else itop
       end
   | _ => itop
   end.
@@ -1711,7 +1708,7 @@ Definition intuoffloat (x: aval) :=
   | F f =>
       match Float.intuoffloat f with
       | Some i => I i
-      | None => if strict then Vbot else itop
+      | None => if va_strict tt then Vbot else itop
       end
   | _ => itop
   end.
@@ -2823,7 +2820,7 @@ Definition mtop := minit Ptop.
 
 Definition load (chunk: memory_chunk) (rm: romem) (m: amem) (p: aptr) : aval :=
   match p with
-  | Pbot => if strict then Vbot else Vtop
+  | Pbot => if va_strict tt then Vbot else Vtop
   | Gl id ofs =>
       match rm!id with
       | Some ab => ablock_load chunk ab (Int.unsigned ofs)
@@ -2882,7 +2879,7 @@ Definition storev (chunk: memory_chunk) (m: amem) (addr: aval) (v: aval): amem :
 
 Definition loadbytes (m: amem) (rm: romem) (p: aptr) : aptr :=
   match p with
-  | Pbot => if strict then Pbot else Ptop
+  | Pbot => if va_strict tt then Pbot else Ptop
   | Gl id _ | Glo id =>
       match rm!id with
       | Some ab => ablock_loadbytes ab
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b99c9af..90662a3 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1765,22 +1765,28 @@ let rec elab_stmt env ctx s =
       { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc }
 
   | FOR(fc, a2, a3, s1, loc) ->
-      let a1' =
+      let (a1', env', decls') =
         match fc with
         | FC_EXP a1 ->
-            elab_for_expr loc env a1
+            (elab_for_expr loc env a1, env, None)
         | FC_DECL def ->
-            error loc "C99 declaration within `for' not supported";
-            sskip in
+            let (dcl, env') = elab_definition true (Env.new_scope env) def in
+            let loc = elab_loc (get_definitionloc def) in
+            (sskip, env', 
+             Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in
       let a2' =
         if a2 = NOTHING
         then intconst 1L IInt
-        else elab_expr loc env a2 in
-      if not (is_scalar_type env a2'.etyp) then
+        else elab_expr loc env' a2 in
+      if not (is_scalar_type env' a2'.etyp) then
         error loc "the condition of 'for' does not have scalar type";
-      let a3' = elab_for_expr loc env a3 in
-      let s1' = elab_stmt env (ctx_loop ctx) s1 in
-      { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc }
+      let a3' = elab_for_expr loc env' a3 in
+      let s1' = elab_stmt env' (ctx_loop ctx) s1 in
+      let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in
+      begin match decls' with
+      | None -> sfor
+      | Some sl -> { sdesc = Sblock (sl @ [sfor]); sloc = elab_loc loc }
+      end
 
 (* 6.8.4 Switch statement *)
   | SWITCH(a, s1, loc) ->
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 5d068b6..b1f2bd8 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -28,6 +28,7 @@ let option_falignfunctions = ref (None: int option)
 let option_falignbranchtargets = ref 0
 let option_faligncondbranchs = ref 0
 let option_finline_asm = ref false
+let option_Osize = ref false
 let option_dparse = ref false
 let option_dcmedium = ref false
 let option_dclight = ref false
diff --git a/driver/Compopts.v b/driver/Compopts.v
new file mode 100644
index 0000000..205f768
--- /dev/null
+++ b/driver/Compopts.v
@@ -0,0 +1,33 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Compilation options *)
+
+(** This file collects Coq functions to query the command-line
+  options that influence the code generated by the verified
+  part of CompCert.   These functions are mapped by extraction
+  to accessors for the flags in [Clflags.ml]. *)
+
+(** Flag [-Os].  For instruction selection (mainly). *)
+Parameter optim_for_size: unit -> bool.
+
+(** Flag [-ffloat-const-prop].  For value analysis and constant propagation. *)
+Parameter propagate_float_constants: unit -> bool.
+Parameter generate_float_constants: unit -> bool.
+
+(** For value analysis.  Currently always false. *)
+Parameter va_strict: unit -> bool.
+
+(** Flag -ftailcalls.  For tail call optimization. *)
+Parameter eliminate_tailcalls: unit -> bool.
+
+
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 47061cd..8853794 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -426,6 +426,8 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fall          Activate all language support options above
   -fnone         Turn off all language support options above
 Code generation options: (use -fno-<opt> to turn off -f<opt>) :
+  -O             Optimize for speed [on by default]
+  -Os            Optimize for code size
   -ffpu          Use FP registers for some integer operations [on]
   -fsmall-data <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
@@ -525,6 +527,8 @@ let cmdline_actions =
       assembler_options := s :: !assembler_options);
   "-Wl,", Self (fun s ->
       push_linker_arg s);
+  "-Os$", Set option_Osize;
+  "-O$", Unset option_Osize;
   "-fsmall-data$", Integer(fun n -> option_small_data := n);
   "-fsmall-const$", Integer(fun n -> option_small_const := n);
   "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n);
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 25d363c..5975ae3 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -454,6 +454,7 @@ let diagnose_stuck_expr p ge w f a kont e m =
     | RV, Ecomma(r1, r2, ty) -> diagnose RV r1
     | RV, Eparen(r1, ty) -> diagnose RV r1
     | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs
+    | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs
     | _, _ -> false in
   if found then true else begin
     let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in
diff --git a/extraction/extraction.v b/extraction/extraction.v
index b8442a8..654e80f 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -68,18 +68,6 @@ Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2.
 Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline".
 Extraction Inline Inlining.ret Inlining.bind.
 
-(* ValueDomain *)
-Extract Constant ValueDomain.strict =>
-  "false".
-Extract Constant ValueDomain.propagate_float_constants =>
-  "fun _ -> !Clflags.option_ffloatconstprop >= 1".
-Extract Constant ValueDomain.generate_float_constants =>
-  "fun _ -> !Clflags.option_ffloatconstprop >= 2".
-
-(* Tailcall *)
-Extract Constant Tailcall.eliminate_tailcalls =>
-  "fun _ -> !Clflags.option_ftailcalls".
-
 (* Allocation *)
 Extract Constant Allocation.regalloc => "Regalloc.regalloc".
 
@@ -90,6 +78,18 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident".
 Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
 
+(* Compopts *)
+Extract Constant Compopts.optim_for_size =>
+  "fun _ -> !Clflags.option_Osize".
+Extract Constant Compopts.va_strict =>
+  "fun _ -> false".
+Extract Constant Compopts.propagate_float_constants =>
+  "fun _ -> !Clflags.option_ffloatconstprop >= 1".
+Extract Constant Compopts.generate_float_constants =>
+  "fun _ -> !Clflags.option_ffloatconstprop >= 2".
+Extract Constant Compopts.eliminate_tailcalls =>
+  "fun _ -> !Clflags.option_ftailcalls".
+
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 396c94c..aaf08a1 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -14,6 +14,7 @@
     This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index d9e6068..148a08d 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for operator strength reduction. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 022e015..1802e11 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 9dbaa78..6aa0925 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -14,6 +14,7 @@
     This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index e7dd3a4..0c88246 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for operator strength reduction. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index bdb94bd..ad4f3b9 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -37,6 +37,7 @@
 *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -190,9 +191,12 @@ Definition mulimm_base (n1: int) (e2: expr) :=
   | i :: nil =>
       shlimm e2 i
   | i :: j :: nil =>
-      Elet e2
-        (Eop Oadd (shlimm (Eletvar 0) i :::
-                   shlimm (Eletvar 0) j ::: Enil))
+      if optim_for_size tt then
+        Eop (Omulimm n1) (e2:::Enil)
+      else
+        Elet e2
+          (Eop Oadd (shlimm (Eletvar 0) i :::
+                     shlimm (Eletvar 0) j ::: Enil))
   | _ =>
       Eop (Omulimm n1) (e2:::Enil)
   end.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 0cfa707..4d26cf6 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -304,7 +305,8 @@ Proof.
   replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul.
   apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib.
   destruct l.
-  intros. rewrite H1. simpl.
+  intros. destruct (optim_for_size tt). TrivialExists.
+  rewrite H1. simpl.
   exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
   exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
   exists (Val.add v1 v2); split.
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 3789953..7f16bb3 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/test/regression/Makefile b/test/regression/Makefile
index c653a01..4d9683c 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -11,7 +11,7 @@ LIBS=$(LIBMATH)
 TESTS=int32 int64 floats floats-basics \
   expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \
   funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
-  sizeof1 sizeof2 binops bool
+  sizeof1 sizeof2 binops bool for1
 
 # Can run, but only in compiled mode, and have reference output in Results
 
diff --git a/test/regression/Results/for1 b/test/regression/Results/for1
new file mode 100644
index 0000000..72ef7e0
--- /dev/null
+++ b/test/regression/Results/for1
@@ -0,0 +1,15 @@
+loop1: 0
+loop1: 1
+loop1: 2
+loop2: 0
+loop2: 1
+loop2: 2
+old i = 3
+loop3: 0 1
+loop3: 1 3
+loop3: 2 5
+old i = 3
+loop4: 0 4
+loop4: 1 3
+loop4: 2 2
+old i = 3
diff --git a/test/regression/for1.c b/test/regression/for1.c
new file mode 100644
index 0000000..4563dde
--- /dev/null
+++ b/test/regression/for1.c
@@ -0,0 +1,20 @@
+/* C99 'for' loops with declarations */
+
+#include <stdio.h>
+
+int main()
+{
+  int i;
+  for (i = 0; i < 3; i++) printf("loop1: %d\n", i);
+  for (int i = 0; i < 3; i++) printf("loop2: %d\n", i);
+  printf("old i = %d\n", i);
+  for (int i = 0, j; i < 3; i++) {
+    j = i * 2 + 1; printf("loop3: %d %d\n", i, j);
+  }
+  printf("old i = %d\n", i);
+  for (int i = 0, j = i + 4; i < 3; i++, j--) {
+    printf("loop4: %d %d\n", i, j);
+  }
+  printf("old i = %d\n", i);
+  return 0;
+}