diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 14 |
1 files changed, 9 insertions, 5 deletions
@@ -16,11 +16,13 @@ include Makefile.config ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) -ARCHDIRS=$(ARCH) +ARCHDIRS?=$(ARCH) else -ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +ARCHDIRS?=$(ARCH)_$(BITSIZE) $(ARCH) endif +BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v + DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ exportclight MenhirLib cparser @@ -28,7 +30,7 @@ DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ MenhirLib cparser -COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) +COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d))) COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) @@ -68,7 +70,7 @@ COMMON=Errors.v AST.v Linking.v \ # Back-end modules (in backend/, $(ARCH)/) BACKEND=\ - Cminor.v Cminortyping.v Op.v CminorSel.v \ + Cminor.v Cminortyping.v Op.v CminorSel.v OpHelpers.v OpHelpersproof.v \ SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \ SelectOpproof.v SelectDivproof.v SplitLongproof.v \ SelectLongproof.v Selectionproof.v \ @@ -93,7 +95,8 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ - Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v + Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ + $(BACKENDLIB) # C front-end modules (in cfrontend/) @@ -135,6 +138,7 @@ all: $(MAKE) proof $(MAKE) extraction $(MAKE) ccomp + $(MAKE) ccomp.byte ifeq ($(HAS_RUNTIME_LIB),true) $(MAKE) runtime endif |