From 593ce3f7c5647e284cd2fdc3dd3ed41be9563982 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 7 Sep 2006 15:30:24 +0000 Subject: Integration du front-end CIL developpe par Thomas Moniot git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/.depend | 58 +++++++++++++++++++++++++++++++++-------------------- extraction/Makefile | 16 ++++++++------- 2 files changed, 45 insertions(+), 29 deletions(-) (limited to 'extraction') diff --git a/extraction/.depend b/extraction/.depend index e18eef8..aa7e42a 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -8,6 +8,10 @@ BinInt.cmi ../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \ BinInt.cmx +../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ + CList.cmi BinInt.cmi AST.cmi +../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ + CList.cmx BinInt.cmx AST.cmx ../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \ ../caml/CMlexer.cmi ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ @@ -30,10 +34,20 @@ ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx -../caml/Main2.cmo: ../caml/PrintPPC.cmi Main.cmi Datatypes.cmi \ - ../caml/CMtypecheck.cmi ../caml/CMparser.cmi ../caml/CMlexer.cmi -../caml/Main2.cmx: ../caml/PrintPPC.cmx Main.cmx Datatypes.cmx \ - ../caml/CMtypecheck.cmx ../caml/CMparser.cmx ../caml/CMlexer.cmx +../caml/Main2.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \ + Datatypes.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 \ + ../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 \ + 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 \ @@ -76,11 +90,11 @@ CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.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 \ AST.cmi -cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi csyntax.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 \ +Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi csyntax.cmi Coqlib.cmi \ +Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ CList.cmi AST.cmi Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \ @@ -113,7 +127,7 @@ 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 \ + Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \ Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi Maps.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ BinInt.cmi @@ -227,18 +241,18 @@ Csharpminor.cmo: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.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 \ 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 -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 +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 +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 Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \ @@ -312,11 +326,11 @@ Mach.cmx: Zmax.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.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 \ + 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 \ + Linearize.cmx Datatypes.cmx Ctyping.cmx Csyntax.cmx Cshmgen.cmx \ Constprop.cmx Cminorgen.cmx Cminor.cmx CSE.cmx Allocation.cmx AST.cmx \ Main.cmi Maps.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ diff --git a/extraction/Makefile b/extraction/Makefile index 72bf244..e4dcdbe 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -6,10 +6,9 @@ FILES=\ Coqlib.ml Maps.ml Sets.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 \ - cshmgen.ml \ + Csyntax.ml Ctyping.ml Csharpminor.ml Cshmgen.ml \ Op.ml Cminor.ml Cmconstr.ml \ - Csharpminor.ml Cminorgen.ml \ + Cminorgen.ml \ Registers.ml RTL.ml \ ../caml/RTLgenaux.ml RTLgen.ml \ Locations.ml Conventions.ml \ @@ -23,27 +22,30 @@ FILES=\ Mach.ml Stacking.ml \ PPC.ml PPCgen.ml \ Main.ml \ + ../caml/Cil2Csyntax.ml \ ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \ - ../caml/PrintPPC.ml ../caml/Main2.ml + ../caml/PrintCsyntax.ml ../caml/PrintPPC.ml \ + ../caml/Main2.ml EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES)) GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli) -CAMLINCL=-I ../caml +CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX 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 COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source ../ccomp: $(FILES:.ml=.cmo) - $(OCAMLC) -o ../ccomp $(FILES:.ml=.cmo) + $(OCAMLC) -o ../ccomp $(OCAMLLIBS) $(FILES:.ml=.cmo) clean:: rm -f ../ccomp ../ccomp.opt: $(FILES:.ml=.cmx) - $(OCAMLOPT) -o ../ccomp.opt $(FILES:.ml=.cmx) + $(OCAMLOPT) -o ../ccomp.opt $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx) clean:: rm -f ../ccomp.opt -- cgit v1.2.3