From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/.depend | 370 ++++++++++++++++++++++++++++-------------------- extraction/Makefile | 26 ++-- extraction/convert | 1 + extraction/extraction.v | 1 + 4 files changed, 233 insertions(+), 165 deletions(-) (limited to 'extraction') diff --git a/extraction/.depend b/extraction/.depend index 53f8468..956c4d3 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -8,20 +8,20 @@ ../caml/CMlexer.cmi ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ ../caml/CMlexer.cmi -../caml/CMparser.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ - Cmconstr.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ +../caml/CMparser.cmo: Integers.cmi Datatypes.cmi Cminor.cmi \ + ../caml/Camlcoq.cmo CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ ../caml/CMparser.cmi -../caml/CMparser.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ - Cmconstr.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ +../caml/CMparser.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \ + ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ ../caml/CMparser.cmi ../caml/CMtypecheck.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi ../caml/CMtypecheck.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.cmi -../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CList.cmi BinPos.cmi \ - BinInt.cmi -../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \ - BinInt.cmx +../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CString.cmi CList.cmi \ + BinPos.cmi BinInt.cmi Ascii.cmi +../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CString.cmx CList.cmx \ + BinPos.cmx BinInt.cmx Ascii.cmx ../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ @@ -35,15 +35,11 @@ ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx ../caml/Main2.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \ - Datatypes.cmi Csyntax.cmi ../caml/Cil2Csyntax.cmo ../caml/CMtypecheck.cmi \ + Errors.cmi Csyntax.cmi ../caml/Cil2Csyntax.cmo ../caml/CMtypecheck.cmi \ ../caml/CMparser.cmi ../caml/CMlexer.cmi ../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \ - Datatypes.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \ + Errors.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \ ../caml/CMparser.cmx ../caml/CMlexer.cmx -../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ - ../caml/Camlcoq.cmo CList.cmi AST.cmi -../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ - ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ @@ -52,32 +48,40 @@ AST.cmi ../caml/PrintPPC.cmi ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \ AST.cmx ../caml/PrintPPC.cmi -../caml/RTLgenaux.cmo: Cminor.cmi -../caml/RTLgenaux.cmx: Cminor.cmx +../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \ + CList.cmi +../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \ + CList.cmx ../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \ ../caml/Camlcoq.cmx CList.cmx AST.cmx -AST.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi -Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ - Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi LTL.cmi Datatypes.cmi \ - Conventions.cmi Coloring.cmi CList.cmi BinPos.cmi AST.cmi +AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \ + Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi +Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \ + Maps.cmi Locations.cmi LTL.cmi Errors.cmi Datatypes.cmi Coloring.cmi \ + CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi +Ascii.cmi: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi BinNat.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinPos.cmi: Peano.cmi Datatypes.cmi Bool.cmi: Specif.cmi Datatypes.cmi +Bounds.cmi: Zmax.cmi Locations.cmi Linear.cmi Conventions.cmi CList.cmi \ + BinPos.cmi BinInt.cmi AST.cmi CInt.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CList.cmi: Specif.cmi Datatypes.cmi CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi -Cmconstr.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ - Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Cminor.cmi: Values.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Datatypes.cmi CList.cmi BinInt.cmi AST.cmi -Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Mem.cmi \ - Maps.cmi Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \ - Cmconstr.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi +CString.cmi: Specif.cmi Datatypes.cmi Ascii.cmi +Cminor.cmi: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ + Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ + AST.cmi +CminorSel.cmi: Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi CList.cmi \ + BinInt.cmi AST.cmi +Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \ + Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi \ + Cminor.cmi CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi \ + AST.cmi Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ CList.cmi BinInt.cmi AST.cmi @@ -88,15 +92,19 @@ Conventions.cmi: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ BinInt.cmi AST.cmi Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \ BinPos.cmi BinInt.cmi -Csharpminor.cmi: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ - Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ +Csharpminor.cmi: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \ + Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \ AST.cmi -Cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi Csyntax.cmi \ - Csharpminor.cmi CList.cmi AST.cmi -Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ - Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi +Cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \ + Csyntax.cmi Csharpminor.cmi Cminor.cmi CString.cmi CList.cmi Ascii.cmi \ + AST.cmi +Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \ + Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \ + Ascii.cmi AST.cmi Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ CList.cmi AST.cmi +EqNat.cmi: Specif.cmi Datatypes.cmi +Errors.cmi: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Datatypes.cmi \ CList.cmi CInt.cmi BinPos.cmi BinInt.cmi FSetFacts.cmi: Specif.cmi Setoid.cmi FSetInterface.cmi Datatypes.cmi @@ -110,34 +118,36 @@ Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ InterfGraph.cmi: Specif.cmi Registers.cmi OrderedType.cmi Locations.cmi \ Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi -Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \ - Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi \ - BinInt.cmi -LTL.cmi: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ - BinInt.cmi AST.cmi +Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \ + Lattice.cmi Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi \ + BinPos.cmi BinInt.cmi +LTL.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \ + Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \ + BinPos.cmi BinInt.cmi AST.cmi +LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ + AST.cmi Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ BinPos.cmi -Linear.cmi: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \ +Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi -Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ +Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \ Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi -Lineartyping.cmi: Zmax.cmi Locations.cmi Linear.cmi Datatypes.cmi \ - Conventions.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ BinInt.cmi AST.cmi -Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \ - Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ - Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \ - Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi +Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Locations.cmi \ + Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ + BinInt.cmi AST.cmi +Main.cmi: Tunneling.cmi Stacking.cmi Selection.cmi Reload.cmi RTLgen.cmi \ + RTL.cmi PPCgen.cmi PPC.cmi Linearize.cmi Errors.cmi Datatypes.cmi \ + Ctyping.cmi Csyntax.cmi Cshmgen.cmi Constprop.cmi Cminorgen.cmi \ + Cminor.cmi CString.cmi CSE.cmi Ascii.cmi Allocation.cmi AST.cmi Maps.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ BinInt.cmi Mem.cmi: Zmax.cmi Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Op.cmi: Values.cmi Specif.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ +Op.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Ordered.cmi: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi @@ -145,24 +155,32 @@ OrderedType.cmi: Specif.cmi Datatypes.cmi PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi + Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \ + BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Peano.cmi: Datatypes.cmi -RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ - Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi BinPos.cmi AST.cmi -RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ - Coqlib.cmi CList.cmi AST.cmi +RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi +RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \ + Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi \ + CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi +RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Errors.cmi \ + Datatypes.cmi Coqlib.cmi Conventions.cmi CString.cmi CList.cmi BinPos.cmi \ + BinInt.cmi Ascii.cmi AST.cmi Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \ Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi +Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \ + LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi +Selection.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ + CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Setoid.cmi: Datatypes.cmi Specif.cmi: Datatypes.cmi -Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \ - Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi +Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Linear.cmi \ + Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ + CString.cmi CList.cmi Bounds.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Sumbool.cmi: Specif.cmi Datatypes.cmi +Switch.cmi: Integers.cmi EqNat.cmi Datatypes.cmi CList.cmi Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi BinInt.cmi AST.cmi @@ -175,18 +193,20 @@ Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zmax.cmi: Datatypes.cmi BinInt.cmi Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi -AST.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi -AST.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx BinPos.cmx BinInt.cmx AST.cmi -Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ - Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi Lattice.cmi LTL.cmi \ - Kildall.cmi Datatypes.cmi Conventions.cmi Coloring.cmi CList.cmi \ - BinPos.cmi AST.cmi Allocation.cmi -Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx \ - Parallelmove.cmx Op.cmx Maps.cmx Locations.cmx Lattice.cmx LTL.cmx \ - Kildall.cmx Datatypes.cmx Conventions.cmx Coloring.cmx CList.cmx \ - BinPos.cmx AST.cmx Allocation.cmi +AST.cmo: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \ + Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi +AST.cmx: Specif.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \ + Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmi +Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \ + Maps.cmi Locations.cmi Lattice.cmi LTL.cmi Kildall.cmi Errors.cmi \ + Datatypes.cmi Coloring.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \ + AST.cmi Allocation.cmi +Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx \ + Maps.cmx Locations.cmx Lattice.cmx LTL.cmx Kildall.cmx Errors.cmx \ + Datatypes.cmx Coloring.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx \ + AST.cmx Allocation.cmi +Ascii.cmo: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi Ascii.cmi +Ascii.cmx: Specif.cmx Peano.cmx Datatypes.cmx Bool.cmx BinPos.cmx Ascii.cmi BinInt.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi BinInt.cmi BinInt.cmx: Datatypes.cmx BinPos.cmx BinNat.cmx BinInt.cmi BinNat.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinNat.cmi @@ -195,6 +215,10 @@ BinPos.cmo: Peano.cmi Datatypes.cmi BinPos.cmi BinPos.cmx: Peano.cmx Datatypes.cmx BinPos.cmi Bool.cmo: Specif.cmi Datatypes.cmi Bool.cmi Bool.cmx: Specif.cmx Datatypes.cmx Bool.cmi +Bounds.cmo: Zmax.cmi Locations.cmi Linear.cmi Conventions.cmi CList.cmi \ + BinPos.cmi BinInt.cmi AST.cmi Bounds.cmi +Bounds.cmx: Zmax.cmx Locations.cmx Linear.cmx Conventions.cmx CList.cmx \ + BinPos.cmx BinInt.cmx AST.cmx Bounds.cmi CInt.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CInt.cmi CInt.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx CInt.cmi CList.cmo: Specif.cmi Datatypes.cmi CList.cmi @@ -205,22 +229,26 @@ CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \ CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \ Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ AST.cmx CSE.cmi -Cmconstr.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ - Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cmconstr.cmi -Cmconstr.cmx: Specif.cmx Op.cmx Integers.cmx Datatypes.cmx Compare_dec.cmx \ - Cminor.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Cmconstr.cmi -Cminor.cmo: Values.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Datatypes.cmi CList.cmi BinInt.cmi AST.cmi Cminor.cmi -Cminor.cmx: Values.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ - Datatypes.cmx CList.cmx BinInt.cmx AST.cmx Cminor.cmi -Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Mem.cmi \ - Maps.cmi Integers.cmi FSetAVL.cmi Datatypes.cmi Csharpminor.cmi \ - Coqlib.cmi Cminor.cmi Cmconstr.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi Cminorgen.cmi -Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Mem.cmx \ - Maps.cmx Integers.cmx FSetAVL.cmx Datatypes.cmx Csharpminor.cmx \ - Coqlib.cmx Cminor.cmx Cmconstr.cmx CList.cmx BinPos.cmx BinInt.cmx \ - AST.cmx Cminorgen.cmi +CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi +CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.cmi +Cminor.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ + Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ + AST.cmi Cminor.cmi +Cminor.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \ + Globalenvs.cmx Floats.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \ + AST.cmx Cminor.cmi +CminorSel.cmo: Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi CList.cmi \ + BinInt.cmi AST.cmi CminorSel.cmi +CminorSel.cmx: Op.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx CList.cmx \ + BinInt.cmx AST.cmx CminorSel.cmi +Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \ + Maps.cmi Integers.cmi FSetAVL.cmi Errors.cmi Datatypes.cmi \ + Csharpminor.cmi Coqlib.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi \ + BinInt.cmi Ascii.cmi AST.cmi Cminorgen.cmi +Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Mem.cmx \ + Maps.cmx Integers.cmx FSetAVL.cmx Errors.cmx Datatypes.cmx \ + Csharpminor.cmx Coqlib.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx \ + BinInt.cmx Ascii.cmx AST.cmx Cminorgen.cmi Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ ../caml/Coloringaux.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi @@ -243,26 +271,34 @@ Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \ BinPos.cmi BinInt.cmi Coqlib.cmi Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx Datatypes.cmx CList.cmx \ BinPos.cmx BinInt.cmx Coqlib.cmi -Csharpminor.cmo: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ - Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ +Csharpminor.cmo: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \ + Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \ AST.cmi Csharpminor.cmi -Csharpminor.cmx: Zmax.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \ - Globalenvs.cmx Floats.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \ +Csharpminor.cmx: Zmax.cmx Values.cmx Mem.cmx Maps.cmx Integers.cmx \ + Globalenvs.cmx Floats.cmx Datatypes.cmx Cminor.cmx CList.cmx BinInt.cmx \ AST.cmx Csharpminor.cmi -Cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi Csyntax.cmi \ - Csharpminor.cmi CList.cmi AST.cmi Cshmgen.cmi -Cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Datatypes.cmx Csyntax.cmx \ - Csharpminor.cmx CList.cmx AST.cmx Cshmgen.cmi -Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ - Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Csyntax.cmi -Csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx \ - Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Csyntax.cmi +Cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \ + Csyntax.cmi Csharpminor.cmi Cminor.cmi CString.cmi CList.cmi Ascii.cmi \ + AST.cmi Cshmgen.cmi +Cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \ + Csyntax.cmx Csharpminor.cmx Cminor.cmx CString.cmx CList.cmx Ascii.cmx \ + AST.cmx Cshmgen.cmi +Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \ + Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \ + Ascii.cmi AST.cmi Csyntax.cmi +Csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Errors.cmx \ + Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx \ + Ascii.cmx AST.cmx Csyntax.cmi Ctyping.cmo: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ CList.cmi AST.cmi Ctyping.cmi Ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx Csyntax.cmx Coqlib.cmx \ CList.cmx AST.cmx Ctyping.cmi Datatypes.cmo: Datatypes.cmi Datatypes.cmx: Datatypes.cmi +EqNat.cmo: Specif.cmi Datatypes.cmi EqNat.cmi +EqNat.cmx: Specif.cmx Datatypes.cmx EqNat.cmi +Errors.cmo: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi Errors.cmi +Errors.cmx: Datatypes.cmx CString.cmx CList.cmx BinPos.cmx Errors.cmi FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi FSetList.cmi \ Datatypes.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx FSetList.cmx \ @@ -299,58 +335,60 @@ Iteration.cmo: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ Iteration.cmi Iteration.cmx: Wf.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ Iteration.cmi -Kildall.cmo: Specif.cmi Setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \ - Iteration.cmi FSetFacts.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi Kildall.cmi -Kildall.cmx: Specif.cmx Setoid.cmx OrderedType.cmx Maps.cmx Lattice.cmx \ - Iteration.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi -LTL.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ - BinInt.cmi AST.cmi LTL.cmi -LTL.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx Integers.cmx \ - Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx BinPos.cmx \ - BinInt.cmx AST.cmx LTL.cmi +Kildall.cmo: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \ + Lattice.cmi Iteration.cmi FSetFacts.cmi FSetAVL.cmi Datatypes.cmi \ + Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi Kildall.cmi +Kildall.cmx: Specif.cmx Setoid.cmx OrderedType.cmx Ordered.cmx Maps.cmx \ + Lattice.cmx Iteration.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx \ + Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi +LTL.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \ + Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \ + BinPos.cmi BinInt.cmi AST.cmi LTL.cmi +LTL.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx Locations.cmx \ + Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx \ + BinPos.cmx BinInt.cmx AST.cmx LTL.cmi +LTLin.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ + AST.cmi LTLin.cmi +LTLin.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \ + Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ + AST.cmx LTLin.cmi Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ BinPos.cmi Lattice.cmi Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \ BinPos.cmx Lattice.cmi -Linear.cmo: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \ +Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi Linear.cmi -Linear.cmx: Values.cmx Specif.cmx Op.cmx Locations.cmx Integers.cmx \ +Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \ Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ AST.cmx Linear.cmi -Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ +Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \ Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \ Linearize.cmi -Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Linear.cmx Lattice.cmx LTL.cmx \ +Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \ Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \ Linearize.cmi -Lineartyping.cmo: Zmax.cmi Locations.cmi Linear.cmi Datatypes.cmi \ - Conventions.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Lineartyping.cmi -Lineartyping.cmx: Zmax.cmx Locations.cmx Linear.cmx Datatypes.cmx \ - Conventions.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Lineartyping.cmi Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ BinInt.cmi AST.cmi Locations.cmi Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ BinInt.cmx AST.cmx Locations.cmi Logic.cmo: Logic.cmi Logic.cmx: Logic.cmi -Mach.cmo: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi \ +Mach.cmo: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Maps.cmi \ Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mach.cmi -Mach.cmx: Zmax.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx \ +Mach.cmx: Zmax.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Maps.cmx \ Locations.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mach.cmi -Main.cmo: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ - Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \ - Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi \ - Main.cmi -Main.cmx: Tunneling.cmx Stacking.cmx RTLgen.cmx PPCgen.cmx PPC.cmx \ - Linearize.cmx Datatypes.cmx Ctyping.cmx Csyntax.cmx Cshmgen.cmx \ - Constprop.cmx Cminorgen.cmx Cminor.cmx CSE.cmx Allocation.cmx AST.cmx \ - Main.cmi +Main.cmo: Tunneling.cmi Stacking.cmi Selection.cmi Reload.cmi RTLgen.cmi \ + RTL.cmi PPCgen.cmi PPC.cmi Linearize.cmi Errors.cmi Datatypes.cmi \ + Ctyping.cmi Csyntax.cmi Cshmgen.cmi Constprop.cmi Cminorgen.cmi \ + Cminor.cmi CString.cmi CSE.cmi Ascii.cmi Allocation.cmi AST.cmi Main.cmi +Main.cmx: Tunneling.cmx Stacking.cmx Selection.cmx Reload.cmx RTLgen.cmx \ + RTL.cmx PPCgen.cmx PPC.cmx Linearize.cmx Errors.cmx Datatypes.cmx \ + Ctyping.cmx Csyntax.cmx Cshmgen.cmx Constprop.cmx Cminorgen.cmx \ + Cminor.cmx CString.cmx CSE.cmx Ascii.cmx Allocation.cmx AST.cmx Main.cmi Maps.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ BinInt.cmi Maps.cmi Maps.cmx: Specif.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinNat.cmx \ @@ -359,9 +397,9 @@ Mem.cmo: Zmax.cmi Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mem.cmi Mem.cmx: Zmax.cmx Values.cmx Specif.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mem.cmi -Op.cmo: Values.cmi Specif.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ +Op.cmo: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Op.cmi -Op.cmx: Values.cmx Specif.cmx Integers.cmx Globalenvs.cmx Floats.cmx \ +Op.cmx: Values.cmx Specif.cmx Mem.cmx Integers.cmx Globalenvs.cmx Floats.cmx \ Datatypes.cmx CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Op.cmi Ordered.cmo: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi Ordered.cmi @@ -376,11 +414,11 @@ PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ AST.cmx PPC.cmi PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi \ - PPCgen.cmi + Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \ + BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi PPCgen.cmi PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \ - Datatypes.cmx Coqlib.cmx CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx \ - PPCgen.cmi + Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \ + BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi Parallelmove.cmo: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi \ Parallelmove.cmi Parallelmove.cmx: Parmov.cmx Locations.cmx Datatypes.cmx CList.cmx AST.cmx \ @@ -389,38 +427,60 @@ Parmov.cmo: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Parmov.cmi Parmov.cmx: Specif.cmx Peano.cmx Datatypes.cmx CList.cmx Parmov.cmi Peano.cmo: Datatypes.cmi Peano.cmi Peano.cmx: Datatypes.cmx Peano.cmi -RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi RTL.cmi -RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ - Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi -RTLgen.cmo: Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi Op.cmi \ - Maps.cmi Integers.cmi Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi \ - BinPos.cmi AST.cmi RTLgen.cmi -RTLgen.cmx: Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx Op.cmx \ - Maps.cmx Integers.cmx Datatypes.cmx Coqlib.cmx Cminor.cmx CList.cmx \ - BinPos.cmx AST.cmx RTLgen.cmi +RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ + RTL.cmi +RTL.cmx: Values.cmx Registers.cmx Op.cmx Mem.cmx Maps.cmx Integers.cmx \ + Globalenvs.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ + RTL.cmi +RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \ + Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \ + CminorSel.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi \ + RTLgen.cmi +RTLgen.cmx: Switch.cmx Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx \ + Op.cmx Maps.cmx Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx \ + CminorSel.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx AST.cmx \ + RTLgen.cmi RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \ - Op.cmi Maps.cmi Datatypes.cmi Coqlib.cmi CList.cmi AST.cmi RTLtyping.cmi + Op.cmi Maps.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ + CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi \ + RTLtyping.cmi RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \ - Op.cmx Maps.cmx Datatypes.cmx Coqlib.cmx CList.cmx AST.cmx RTLtyping.cmi + Op.cmx Maps.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ + CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx \ + RTLtyping.cmi Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \ Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ Registers.cmi Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \ Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ Registers.cmi +Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \ + LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi +Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \ + LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi +Selection.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ + CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ + Selection.cmi +Selection.cmx: Specif.cmx Op.cmx Integers.cmx Datatypes.cmx Compare_dec.cmx \ + CminorSel.cmx Cminor.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ + Selection.cmi Setoid.cmo: Datatypes.cmi Setoid.cmi Setoid.cmx: Datatypes.cmx Setoid.cmi Specif.cmo: Datatypes.cmi Specif.cmi Specif.cmx: Datatypes.cmx Specif.cmi -Stacking.cmo: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \ - Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi Stacking.cmi -Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx Lineartyping.cmx \ - Linear.cmx Integers.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ - CList.cmx BinPos.cmx BinInt.cmx AST.cmx Stacking.cmi +Stacking.cmo: Specif.cmi Op.cmi Mach.cmi Locations.cmi Linear.cmi \ + Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ + CString.cmi CList.cmi Bounds.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi \ + Stacking.cmi +Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx Linear.cmx \ + Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ + CString.cmx CList.cmx Bounds.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx \ + Stacking.cmi Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi +Switch.cmo: Integers.cmi EqNat.cmi Datatypes.cmi CList.cmi Switch.cmi +Switch.cmx: Integers.cmx EqNat.cmx Datatypes.cmx CList.cmx Switch.cmi Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ diff --git a/extraction/Makefile b/extraction/Makefile index 69b5f57..cb7f4c5 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -1,32 +1,36 @@ FILES=\ - Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \ + Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml EqNat.ml \ Bool.ml CList.ml Sumbool.ml Setoid.ml BinPos.ml BinNat.ml BinInt.ml \ ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \ + Ascii.ml CString.ml \ OrderedType.ml FSetInterface.ml FSetFacts.ml FSetList.ml \ CInt.ml FSetAVL.ml \ - Coqlib.ml Maps.ml Ordered.ml AST.ml Iteration.ml Integers.ml \ + Coqlib.ml Maps.ml Ordered.ml Errors.ml AST.ml Iteration.ml Integers.ml \ ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \ Mem.ml Globalenvs.ml \ - Csyntax.ml Ctyping.ml Csharpminor.ml Cshmgen.ml \ - Op.ml Cminor.ml Cmconstr.ml \ + Csyntax.ml Ctyping.ml Cminor.ml Csharpminor.ml Cshmgen.ml \ Cminorgen.ml \ + Op.ml CminorSel.ml \ + Selection.ml \ Registers.ml RTL.ml \ - ../caml/RTLgenaux.ml RTLgen.ml \ + Switch.ml ../caml/RTLgenaux.ml RTLgen.ml \ Locations.ml Conventions.ml \ ../caml/RTLtypingaux.ml RTLtyping.ml \ Lattice.ml Kildall.ml \ Constprop.ml CSE.ml \ - LTL.ml \ + LTL.ml LTLin.ml \ InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ - Parallelmove.ml Allocation.ml \ - Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \ - Mach.ml Stacking.ml \ + Allocation.ml \ + Tunneling.ml Linear.ml Linearize.ml \ + Parallelmove.ml Reload.ml \ + Mach.ml Bounds.ml Stacking.ml \ PPC.ml PPCgen.ml \ Main.ml \ ../caml/Cil2Csyntax.ml \ ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \ ../caml/PrintCsyntax.ml ../caml/PrintPPC.ml \ ../caml/Main2.ml +# ../caml/Configuration.ml ../caml/Driver.ml EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES)) GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli) @@ -58,13 +62,15 @@ extraction: @echo "Fixing file names..." @mv list.ml CList.ml @mv list.mli CList.mli + @mv string.ml CString.ml + @mv string.mli CString.mli @mv int.ml CInt.ml @mv int.mli CInt.mli @for i in $(GENFILES); do \ j=`./uncapitalize $$i`; \ test -f $$i || (test -f $$j && mv $$j $$i); \ done - @echo "Conversion List -> CList and Int -> CInt..." + @echo "Conversion List -> CList, String -> CString, Int -> CInt..." @./convert $(GENFILES) @echo "Patching files..." @for i in *.patch; do patch < $$i; done diff --git a/extraction/convert b/extraction/convert index a29178a..b3d2533 100755 --- a/extraction/convert +++ b/extraction/convert @@ -1,6 +1,7 @@ #!/usr/bin/perl -pi s/\bList\b/CList/g; +s/\bString\b/CString/g; s/\bInt\.Z_as_Int\b/CInt.Z_as_Int/g; s/\bInt\.Int\b/CInt.Int/g; s/\bInt\.MoreInt\b/CInt.MoreInt/g; diff --git a/extraction/extraction.v b/extraction/extraction.v index 47c6f36..cc33c98 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -38,6 +38,7 @@ Extract Constant Iteration.GenIter.iterate => (* RTLgen *) +Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". (* RTLtyping *) -- cgit v1.2.3