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

1 files changed, 24 insertions, 16 deletions

diff --git a/Makefile b/Makefile
index 00b0000..bea28ac 100644
--- a/Makefile
+++ b/Makefile
@@ -12,30 +12,32 @@ LIB=Coqlib.v Maps.v Lattice.v Ordered.v \
 
 # Files in common/
 
-COMMON=AST.v Events.v Globalenvs.v Mem.v Values.v Main.v
+COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \
+  Smallstep.v Switch.v Main.v
 
 # Files in backend/
 
 BACKEND=\
-  Op.v Cminor.v \
-  Cmconstr.v Cmconstrproof.v \
+  Cminor.v Op.v CminorSel.v \
+  Selection.v Selectionproof.v \
   Registers.v RTL.v \
-  RTLgen.v RTLgenproof1.v RTLgenproof.v \
+  RTLgen.v RTLgenspec.v RTLgenproof.v \
   RTLtyping.v \
   Kildall.v \
   Constprop.v Constpropproof.v \
   CSE.v CSEproof.v \
   Locations.v Conventions.v LTL.v LTLtyping.v \
   InterfGraph.v Coloring.v Coloringproof.v \
-  Parallelmove.v Allocation.v \
-  Allocproof.v Alloctyping.v \
+  Allocation.v Allocproof.v Alloctyping.v \
   Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
-  Linear.v Lineartyping.v \
+  LTLin.v LTLintyping.v \
   Linearize.v Linearizeproof.v Linearizetyping.v \
+  Linear.v Lineartyping.v \
+  Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
   Mach.v Machabstr.v Machtyping.v \
-  Stacking.v Stackingproof.v Stackingtyping.v \
-  Machabstr2mach.v \
-  PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v
+  Bounds.v Stacking.v Stackingproof.v Stackingtyping.v \
+  Machconcr.v Machabstr2concr.v \
+  PPC.v PPCgen.v PPCgenretaddr.v PPCgenproof1.v PPCgenproof.v
 
 # Files in cfrontend/
 
@@ -47,7 +49,7 @@ CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \
 
 FILES=$(LIB:%=lib/%) $(COMMON:%=common/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%)
 
-FLATFILES=$(LIB) $(BACKEND) $(CFRONTEND)
+FLATFILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND)
 
 proof: $(FILES:.v=.vo)
 
@@ -65,24 +67,30 @@ cil:
 	$(MAKE) -C cil
 
 documentation:
-	$(COQDOC) --html -d doc $(FLATFILES:%.v=--glob-from doc/%.glob) $(FILES)
-	doc/removeproofs doc/lib.*.html doc/backend.*.html
+	@ln -f $(FILES) doc/
+	@mkdir -p doc/html
+	cd doc; $(COQDOC) --html -d html \
+          $(FLATFILES:%.v=--glob-from %.glob) $(FLATFILES)
+	@cd doc; rm -f $(FLATFILES)
+	cp doc/coqdoc.css doc/html/coqdoc.css
+	doc/removeproofs doc/html/*.html
 
 latexdoc:
-	$(COQDOC) --latex -o doc/doc.tex -g $(FILES)
+	cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
 
 .SUFFIXES: .v .vo
 
 .v.vo:
 	@rm -f doc/glob/$(*F).glob
-	$(COQC) -dump-glob doc/$(*F).glob $*.v
+	@echo "COQC $*.v"
+	@$(COQC) -dump-glob doc/$(*F).glob $*.v
 
 depend:
 	$(COQDEP) $(FILES) > .depend
 
 clean:
 	rm -f */*.vo *~ */*~
-	rm -f doc/lib.*.html doc/backend.*.html doc/*.glob
+	rm -rf doc/html doc/*.glob
 	$(MAKE) -C extraction clean
 	$(MAKE) -C test/cminor clean