From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/.depend | 529 -------------------------------------------- extraction/Kildall.ml.patch | 4 +- extraction/Makefile | 117 +--------- extraction/extraction.v | 22 +- 4 files changed, 26 insertions(+), 646 deletions(-) delete mode 100644 extraction/.depend (limited to 'extraction') diff --git a/extraction/.depend b/extraction/.depend deleted file mode 100644 index a8ae227..0000000 --- a/extraction/.depend +++ /dev/null @@ -1,529 +0,0 @@ -../caml/CMlexer.cmi: ../caml/CMparser.cmi -../caml/CMparser.cmi: Cminor.cmi AST.cmi -../caml/CMtypecheck.cmi: Cminor.cmi -../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \ - InterfGraph.cmi -../caml/PrintPPC.cmi: PPC.cmi -../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 \ - CList.cmx AST.cmx -../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \ - ../caml/CMlexer.cmi -../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ - ../caml/CMlexer.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: Integers.cmx Datatypes.cmx Cminor.cmx \ - ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ - ../caml/CMparser.cmi -../caml/CMtypecheck.cmo: Integers.cmi Datatypes.cmi Cminor.cmi \ - ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi -../caml/CMtypecheck.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \ - ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.cmi -../caml/Coloringaux.cmo: Registers.cmi RTLtyping.cmi RTL.cmi Maps.cmi \ - Locations.cmi InterfGraph.cmi Datatypes.cmi Conventions.cmi \ - ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi ../caml/Coloringaux.cmi -../caml/Coloringaux.cmx: Registers.cmx RTLtyping.cmx RTL.cmx Maps.cmx \ - Locations.cmx InterfGraph.cmx Datatypes.cmx Conventions.cmx \ - ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi -../caml/Driver.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \ - Errors.cmi Csyntax.cmi ../caml/Configuration.cmo ../caml/Clflags.cmo \ - ../caml/Cil2Csyntax.cmo ../caml/Camlcoq.cmo ../caml/CMtypecheck.cmi \ - ../caml/CMparser.cmi ../caml/CMlexer.cmi -../caml/Driver.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \ - Errors.cmx Csyntax.cmx ../caml/Configuration.cmx ../caml/Clflags.cmx \ - ../caml/Cil2Csyntax.cmx ../caml/Camlcoq.cmx ../caml/CMtypecheck.cmx \ - ../caml/CMparser.cmx ../caml/CMlexer.cmx -../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo -../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx -../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTL.cmi Datatypes.cmi \ - Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi -../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \ - Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.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 \ - CList.cmx AST.cmx -../caml/PrintPPC.cmo: PPC.cmi Datatypes.cmi ../caml/Camlcoq.cmo CList.cmi \ - 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: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \ - ../caml/Camlcoq.cmo -../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \ - ../caml/Camlcoq.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 -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 -AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \ - Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.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 -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 -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: Values.cmi Specif.cmi Op.cmi Mem.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.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 -Compare_dec.cmi: Specif.cmi Datatypes.cmi -Constprop.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ - Floats.cmi Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi -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 -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 -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: Specif.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 -CString.cmi: Specif.cmi Datatypes.cmi Ascii.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 -Floats.cmi: Specif.cmi Integers.cmi Datatypes.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 -FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi -FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi -Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi Bool.cmi BinPos.cmi BinInt.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 Ordered.cmi Maps.cmi \ - Lattice.cmi Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi \ - BinPos.cmi BinInt.cmi -Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ - BinPos.cmi -Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \ - Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \ - CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi -Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Coqlib.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 -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 -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 -Mach.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 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 -OrderedType.cmi: Specif.cmi Datatypes.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 -PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ - Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \ - BinPos.cmi BinInt.cmi Ascii.cmi AST.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 -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 Integers.cmi Datatypes.cmi Conventions.cmi CList.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 Cminor.cmi \ - CString.cmi CList.cmi BinPos.cmi Ascii.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 -RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Errors.cmi \ - Datatypes.cmi Coqlib.cmi Conventions.cmi CString.cmi CList.cmi Ascii.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 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: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.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 -ZArith_dec.cmi: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi -Zbool.cmi: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.cmi \ - BinInt.cmi -Zdiv.cmi: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \ - BinInt.cmi -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 -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 -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 -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 -BinNat.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinNat.cmi -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 -CList.cmx: Specif.cmx Datatypes.cmx CList.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 -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: Values.cmi Specif.cmi Op.cmi Mem.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi AST.cmi \ - CminorSel.cmi -CminorSel.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Integers.cmx \ - Globalenvs.cmx Datatypes.cmx Cminor.cmx CList.cmx BinInt.cmx AST.cmx \ - CminorSel.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 -Coloring.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx Maps.cmx \ - Locations.cmx InterfGraph.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ - ../caml/Coloringaux.cmx CList.cmx BinInt.cmx AST.cmx Coloring.cmi -Compare_dec.cmo: Specif.cmi Datatypes.cmi Compare_dec.cmi -Compare_dec.cmx: Specif.cmx Datatypes.cmx Compare_dec.cmi -Constprop.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Lattice.cmi \ - Kildall.cmi Integers.cmi Floats.cmi Datatypes.cmi CList.cmi Bool.cmi \ - BinPos.cmi BinInt.cmi AST.cmi Constprop.cmi -Constprop.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Lattice.cmx \ - Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx CList.cmx Bool.cmx \ - BinPos.cmx BinInt.cmx AST.cmx Constprop.cmi -Conventions.cmo: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ - BinInt.cmi AST.cmi Conventions.cmi -Conventions.cmx: Locations.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ - BinInt.cmx AST.cmx Conventions.cmi -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 -CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \ - Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ - AST.cmi CSE.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 -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 Mem.cmx Maps.cmx Integers.cmx \ - Globalenvs.cmx Floats.cmx Datatypes.cmx Cminor.cmx CList.cmx BinInt.cmx \ - AST.cmx Csharpminor.cmi -Cshmgen.cmo: Specif.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 Cshmgen.cmi -Cshmgen.cmx: Specif.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 -CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi -CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.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 -Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \ - Floats.cmi -Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \ - Floats.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 \ - Datatypes.cmx CList.cmx CInt.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi -FSetFacts.cmo: Specif.cmi Setoid.cmi OrderedType.cmi FSetInterface.cmi \ - Datatypes.cmi FSetFacts.cmi -FSetFacts.cmx: Specif.cmx Setoid.cmx OrderedType.cmx FSetInterface.cmx \ - Datatypes.cmx FSetFacts.cmi -FSetInterface.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi \ - FSetInterface.cmi -FSetInterface.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx \ - FSetInterface.cmi -FSetList.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi -FSetList.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx FSetList.cmi -Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi -Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx Integers.cmx Datatypes.cmx \ - CList.cmx BinPos.cmx BinInt.cmx AST.cmx Globalenvs.cmi -Integers.cmo: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi Bool.cmi BinPos.cmi BinInt.cmi Integers.cmi -Integers.cmx: Zpower.cmx Zdiv.cmx Specif.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx Bool.cmx BinPos.cmx BinInt.cmx Integers.cmi -InterfGraph.cmo: Specif.cmi Registers.cmi OrderedType.cmi Ordered.cmi \ - Locations.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ - BinInt.cmi InterfGraph.cmi -InterfGraph.cmx: Specif.cmx Registers.cmx OrderedType.cmx Ordered.cmx \ - Locations.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ - BinInt.cmx InterfGraph.cmi -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 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 -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 -Linearize.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \ - ../caml/Linearizeaux.cmo Lattice.cmi LTLin.cmi LTL.cmi Kildall.cmi \ - FSetAVL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi \ - BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linearize.cmi -Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \ - ../caml/Linearizeaux.cmx Lattice.cmx LTLin.cmx LTL.cmx Kildall.cmx \ - FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \ - BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi -Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi \ - BinPos.cmi BinInt.cmi AST.cmi Linear.cmi -Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \ - Globalenvs.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx CList.cmx \ - BinPos.cmx BinInt.cmx AST.cmx Linear.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 -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 -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 -Mach.cmo: 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: 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 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 \ - BinInt.cmx Maps.cmi -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 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 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 -Ordered.cmx: Specif.cmx OrderedType.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \ - BinPos.cmx Ordered.cmi -OrderedType.cmo: Specif.cmi Datatypes.cmi OrderedType.cmi -OrderedType.cmx: Specif.cmx Datatypes.cmx OrderedType.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 \ - Parallelmove.cmi -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 -PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.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 \ - Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \ - BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi -PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi PPC.cmi -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 -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 Integers.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 Integers.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx \ - Reload.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 Cminor.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 Cminor.cmx CString.cmx CList.cmx BinPos.cmx Ascii.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 -RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \ - Op.cmi Maps.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ - CString.cmi CList.cmi Ascii.cmi AST.cmi RTLtyping.cmi -RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \ - Op.cmx Maps.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ - CString.cmx CList.cmx Ascii.cmx AST.cmx RTLtyping.cmi -Selection.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ - CminorSel.cmi Cminor.cmi ../caml/Clflags.cmo 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 ../caml/Clflags.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 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: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi Switch.cmi -Switch.cmx: Specif.cmx Integers.cmx EqNat.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx BinPos.cmx BinInt.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 \ - BinPos.cmi BinInt.cmi AST.cmi Values.cmi -Values.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ - BinPos.cmx BinInt.cmx AST.cmx Values.cmi -Wf.cmo: Wf.cmi -Wf.cmx: Wf.cmi -ZArith_dec.cmo: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi \ - ZArith_dec.cmi -ZArith_dec.cmx: Sumbool.cmx Specif.cmx Datatypes.cmx BinInt.cmx \ - ZArith_dec.cmi -Zbool.cmo: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.cmi \ - BinInt.cmi Zbool.cmi -Zbool.cmx: Zeven.cmx ZArith_dec.cmx Sumbool.cmx Specif.cmx Datatypes.cmx \ - BinInt.cmx Zbool.cmi -Zdiv.cmo: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \ - BinInt.cmi Zdiv.cmi -Zdiv.cmx: Zbool.cmx ZArith_dec.cmx Specif.cmx Datatypes.cmx BinPos.cmx \ - BinInt.cmx Zdiv.cmi -Zeven.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zeven.cmi -Zeven.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zeven.cmi -Zmax.cmo: Datatypes.cmi BinInt.cmi Zmax.cmi -Zmax.cmx: Datatypes.cmx BinInt.cmx Zmax.cmi -Zmisc.cmo: Datatypes.cmi BinPos.cmi BinInt.cmi Zmisc.cmi -Zmisc.cmx: Datatypes.cmx BinPos.cmx BinInt.cmx Zmisc.cmi -Zpower.cmo: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi -Zpower.cmx: Zmisc.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zpower.cmi diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch index a5b7bc9..453d40c 100644 --- a/extraction/Kildall.ml.patch +++ b/extraction/Kildall.ml.patch @@ -1,5 +1,5 @@ -*** Kildall.ml.orig 2006-09-11 13:50:56.266682206 +0200 ---- Kildall.ml 2006-09-11 14:29:50.392200227 +0200 +*** kildall.ml.orig 2006-09-11 13:50:56.266682206 +0200 +--- kildall.ml 2006-09-11 14:29:50.392200227 +0200 *************** *** 163,171 **** Maps.PMap.t option **) diff --git a/extraction/Makefile b/extraction/Makefile index 044f89f..d4163bb 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -12,66 +12,15 @@ include ../Makefile.config -FILES=\ - 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 Errors.ml AST.ml Iteration.ml Integers.ml \ - ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \ - Mem.ml Globalenvs.ml \ - ../caml/Clflags.ml \ - Csyntax.ml Ctyping.ml Cminor.ml Csharpminor.ml Cshmgen.ml \ - Cminorgen.ml \ - Op.ml CminorSel.ml \ - Selection.ml \ - Registers.ml RTL.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 LTLin.ml \ - InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ - Allocation.ml \ - Tunneling.ml Linear.ml ../caml/Linearizeaux.ml Linearize.ml \ - Parallelmove.ml Reload.ml \ - Mach.ml Bounds.ml Stacking.ml \ - PPC.ml PPCgen.ml \ - Main.ml \ - ../caml/PrintCsyntax.ml ../caml/Cil2Csyntax.ml \ - ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \ - ../caml/PrintPPC.ml \ - ../caml/Configuration.ml ../caml/Driver.ml +DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver -EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES)) -GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli) - -CAMLINCL=-I ../caml -I ../cil/obj/$(ARCHOS) -OCAMLC=ocamlc -g $(CAMLINCL) -OCAMLOPT=ocamlopt $(CAMLINCL) -OCAMLDEP=ocamldep $(CAMLINCL) -OCAMLLIBS=unix.cma str.cma cil.cma - -COQINCL=-I ../lib -I ../common -I ../backend -I ../cfrontend +COQINCL=$(patsubst %,-I ../%,$(DIRS)) COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source -executables: ../ccomp ../ccomp.byt - -../ccomp.byt: $(FILES:.ml=.cmo) - $(OCAMLC) -o ../ccomp.byt $(OCAMLLIBS) $(FILES:.ml=.cmo) -clean:: - rm -f ../ccomp.byt - -../ccomp: $(FILES:.ml=.cmx) - $(OCAMLOPT) -o ../ccomp $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx) -clean:: - rm -f ../ccomp +all: Configuration.ml extraction extraction: - @rm -f $(GENFILES) + rm -f [:lower:]*.mli [:lower:]*.ml $(COQEXEC) extraction.v @echo "Fixing file names..." @mv list.ml CList.ml @@ -80,61 +29,19 @@ extraction: @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, String -> CString, Int -> CInt..." - @./convert $(GENFILES) + @./convert *.mli *.ml @echo "Patching files..." @for i in *.patch; do patch < $$i; done -../caml/CMparser.ml ../caml/CMparser.mli: ../caml/CMparser.mly - ocamlyacc -v ../caml/CMparser.mly - -beforedepend:: ../caml/CMparser.ml ../caml/CMparser.mli -clean:: - rm -f ../caml/CMparser.ml ../caml/CMparser.mli ../caml/CMparser.output - -../caml/CMlexer.ml: ../caml/CMlexer.mll - ocamllex ../caml/CMlexer.mll - -beforedepend:: ../caml/CMlexer.ml -clean:: - rm -f ../caml/CMlexer.ml - -../caml/Configuration.ml: ../Makefile.config +Configuration.ml: ../Makefile.config (echo 'let stdlib_path = "$(LIBDIR)"'; \ echo 'let prepro = "$(CPREPRO)"'; \ echo 'let asm = "$(CASM)"'; \ - echo 'let linker = "$(CLINKER)"') \ - > ../caml/Configuration.ml - -beforedepend:: ../caml/Configuration.ml -clean:: - rm -f ../caml/Configuration.ml - -.SUFFIXES: .ml .mli .cmo .cmi .cmx - -.mli.cmi: - $(OCAMLC) -c $*.mli -.ml.cmo: - $(OCAMLC) -c $*.ml -.ml.cmx: - $(OCAMLOPT) -c $*.ml - -clean:: - rm -f $(GENFILES) - rm -f *.cm? *.o - cd ../caml && rm -f *.cm? *.o - -depend: beforedepend - $(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend - -install: - install -d $(BINDIR) - install ../ccomp ../ccomp.byt $(BINDIR) - -include .depend - + echo 'let linker = "$(CLINKER)"'; \ + echo 'let arch = "$(ARCH)"'; \ + echo 'let variant = "$(VARIANT)"') \ + > Configuration.ml +clean: + rm -f *.mli *.ml diff --git a/extraction/extraction.v b/extraction/extraction.v index cdb1fd6..58da9c0 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -16,7 +16,7 @@ Require Floats. Require RTLgen. Require Coloring. Require Allocation. -Require Main. +Require Compiler. (* Standard lib *) Extract Inductive unit => "unit" [ "()" ]. @@ -68,16 +68,18 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". -(* PPC *) -Extract Constant PPC.low_half => "fun _ -> assert false". -Extract Constant PPC.high_half => "fun _ -> assert false". +(* Asm *) +Extract Constant Asm.low_half => "fun _ -> assert false". +Extract Constant Asm.high_half => "fun _ -> assert false". (* Suppression of stupidly big equality functions *) -Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y". -Extract Constant Locations.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y". -Extract Constant PPC.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". -Extract Constant PPC.freg_eq => "fun (x: freg) (y: freg) -> x = y". -Extract Constant PPC.preg_eq => "fun (x: preg) (y: preg) -> x = y". +Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y". +Extract Constant Op.eq_addressing => "fun (x: addressing) (y: addressing) -> x = y". +(*Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y".*) +Extract Constant Machregs.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y". +Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". +Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". +Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". (* Go! *) -Recursive Extraction Library Main. +Recursive Extraction Library Compiler. -- cgit v1.2.3