diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 59 |
1 files changed, 40 insertions, 19 deletions
@@ -15,20 +15,31 @@ include Makefile.config COQC=coqc $(INCLUDES) COQDEP=coqdep $(INCLUDES) COQDOC=coqdoc +OCAMLBUILD=ocamlbuild +OCB_OPTIONS=\ + -no-hygiene \ + -I extraction $(INCLUDES) \ + -cflags -I,`pwd`/cil/obj/$(ARCHOS) \ + -lflags -I,`pwd`/cil/obj/$(ARCHOS) \ + -libs unix,str,cil -INCLUDES=-I lib -I common -I backend -I cfrontend +DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver -# Files in lib/ +VPATH=$(DIRS) +GPATH=$(DIRS) +INCLUDES=$(patsubst %,-I %, $(DIRS)) + +# General-purpose libraries (in lib/) LIB=Coqlib.v Maps.v Lattice.v Ordered.v \ Iteration.v Integers.v Floats.v Parmov.v -# Files in common/ +# Parts common to the front-ends and the back-end (in common/) COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \ - Smallstep.v Switch.v Main.v Complements.v + Smallstep.v Switch.v -# Files in backend/ +# Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) BACKEND=\ Cminor.v Op.v CminorSel.v \ @@ -39,7 +50,7 @@ BACKEND=\ Kildall.v \ Constprop.v Constpropproof.v \ CSE.v CSEproof.v \ - Locations.v Conventions.v LTL.v LTLtyping.v \ + Machregs.v Locations.v Conventions.v LTL.v LTLtyping.v \ InterfGraph.v Coloring.v Coloringproof.v \ Allocation.v Allocproof.v Alloctyping.v \ Tunneling.v Tunnelingproof.v Tunnelingtyping.v \ @@ -48,29 +59,34 @@ BACKEND=\ Linear.v Lineartyping.v \ Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \ Mach.v Machabstr.v Machtyping.v \ - Bounds.v Stacking.v Stackingproof.v Stackingtyping.v \ + Bounds.v Stacklayout.v Stacking.v Stackingproof.v Stackingtyping.v \ Machconcr.v Machabstr2concr.v \ - PPC.v PPCgen.v PPCgenretaddr.v PPCgenproof1.v PPCgenproof.v + Asm.v Asmgen.v Asmgenretaddr.v Asmgenproof1.v Asmgenproof.v -# Files in cfrontend/ +# C front-end modules (in cfrontend/) CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \ Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v -# All source files +# Putting everything together (in driver/) + +DRIVER=Compiler.v Complements.v -FILES=$(LIB:%=lib/%) $(COMMON:%=common/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%) +# All source files -FLATFILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) +FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) proof: $(FILES:.v=.vo) +exec: + $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native && mv Driver.native ccomp + all: $(MAKE) proof $(MAKE) -C cil - $(MAKE) -C extraction extraction - $(MAKE) -C extraction depend + $(MAKE) -C extraction + $(MAKE) exec $(MAKE) -C extraction $(MAKE) -C runtime @@ -78,8 +94,8 @@ documentation: doc/removeproofs @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) + $(FILES:%.v=--glob-from %.glob) $(FILES) + @cd doc; rm -f $(FILES) cp doc/coqdoc.css doc/html/coqdoc.css doc/removeproofs doc/html/*.html @@ -100,14 +116,19 @@ latexdoc: @$(COQC) -dump-glob doc/$(*F).glob $*.v depend: - $(COQDEP) $(FILES) > .depend + $(COQDEP) $(patsubst %, %/*.v, $(DIRS)) \ + | sed -e 's|$(ARCH)/$(VARIANT)/|$$(ARCH)/$$(VARIANT)/|g' \ + -e 's|$(ARCH)/|$$(ARCH)/|g' \ + > .depend install: - $(MAKE) -C extraction install + install -d $(BINDIR) + install ../ccomp $(BINDIR) $(MAKE) -C runtime install clean: - rm -f */*.vo *~ */*~ + rm -f $(patsubst %, %/*.vo, $(DIRS)) + rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/removeproofs.ml doc/removeproofs $(MAKE) -C extraction clean |