MAJ suite ajouts dans Kildall. Compiler en code natif par defaut

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

2 files changed, 29 insertions, 11 deletions

diff --git a/extraction/.depend b/extraction/.depend
index e70b567..9e201ba 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -99,6 +99,8 @@ Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
 Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \
     Datatypes.cmi CList.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 
@@ -108,8 +110,9 @@ InterfGraph.cmi: Specif.cmi Registers.cmi OrderedType.cmi Locations.cmi \
     Int.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi 
 Int.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi 
 Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi 
-Kildall.cmi: Specif.cmi Maps.cmi Lattice.cmi Iteration.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi BinPos.cmi 
+Kildall.cmi: Specif.cmi setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \
+    Iteration.cmi Int.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
+    BinInt.cmi 
 Lattice.cmi: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi 
 Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \
     Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
@@ -153,6 +156,7 @@ RTL.cmi: Values.cmi Registers.cmi Op.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 Locations.cmi \
     Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi AST.cmi 
+setoid.cmi: Datatypes.cmi 
 Sets.cmi: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi 
 Specif.cmi: Datatypes.cmi 
 Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \
@@ -263,6 +267,14 @@ FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi FSetList.cmi \
     Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi 
 FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx Int.cmx FSetList.cmx \
     Datatypes.cmx CList.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 \
@@ -285,10 +297,12 @@ 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 Maps.cmi Lattice.cmi Iteration.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi BinPos.cmi Kildall.cmi 
-Kildall.cmx: Specif.cmx Maps.cmx Lattice.cmx Iteration.cmx Datatypes.cmx \
-    Coqlib.cmx CList.cmx BinPos.cmx Kildall.cmi 
+Kildall.cmo: Specif.cmi setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \
+    Iteration.cmi Int.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 Int.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \
+    CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi 
 Lattice.cmo: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi Lattice.cmi 
 Lattice.cmx: Specif.cmx Maps.cmx Datatypes.cmx BinPos.cmx Lattice.cmi 
 Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \
@@ -391,6 +405,8 @@ RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \
 RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \
     Op.cmx Maps.cmx Locations.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
     CList.cmx AST.cmx RTLtyping.cmi 
+setoid.cmo: Datatypes.cmi setoid.cmi 
+setoid.cmx: Datatypes.cmx setoid.cmi 
 Sets.cmo: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Sets.cmi 
 Sets.cmx: Specif.cmx Maps.cmx Datatypes.cmx CList.cmx Sets.cmi 
 Specif.cmo: Datatypes.cmi Specif.cmi 
diff --git a/extraction/Makefile b/extraction/Makefile
index e4dcdbe..0df787b 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -2,7 +2,7 @@ FILES=\
   Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \
   Bool.ml CList.ml Sumbool.ml BinPos.ml BinNat.ml BinInt.ml \
   ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \
-  Int.ml OrderedType.ml FSetList.ml FSetAVL.ml \
+  Int.ml OrderedType.ml FSetInterface.ml FSetFacts.ml FSetList.ml FSetAVL.ml \
   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 \
@@ -39,13 +39,15 @@ 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 $(OCAMLLIBS) $(FILES:.ml=.cmo)
+executables: ../ccomp ../ccomp.byt
+
+../ccomp.byt: $(FILES:.ml=.cmo)
+	$(OCAMLC) -o ../ccomp.byt $(OCAMLLIBS) $(FILES:.ml=.cmo)
 clean::
 	rm -f ../ccomp
 
-../ccomp.opt: $(FILES:.ml=.cmx)
-	$(OCAMLOPT) -o ../ccomp.opt $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx)
+../ccomp: $(FILES:.ml=.cmx)
+	$(OCAMLOPT) -o ../ccomp $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx)
 clean::
 	rm -f ../ccomp.opt