diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:25:09 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:25:09 +0200 |
| commit | 3b79923a6c9fa8c76916df1eecfdecd7ae2124a5 (patch) | |
| tree | 98b27b88ea7195a244eff90eaa5f63028ad518a6 /Makefile | |
| parent | 9bc337d05eed466e2bfc9b18aa35fac34d3954a9 (diff) | |
| parent | 91381b65f5aa76e5195caae9ef331b3f5f95afaf (diff) | |
| download | compcert-kvx-3b79923a6c9fa8c76916df1eecfdecd7ae2124a5.tar.gz compcert-kvx-3b79923a6c9fa8c76916df1eecfdecd7ae2124a5.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 24 |
1 files changed, 12 insertions, 12 deletions
@@ -25,9 +25,10 @@ BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ - exportclight cparser cparser/MenhirLib + exportclight MenhirLib cparser -RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser +RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ + MenhirLib cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d))) @@ -64,7 +65,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ COMMON=Errors.v AST.v Linking.v \ Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v \ - Separation.v + Separation.v Builtins0.v Builtins1.v Builtins.v # Back-end modules (in backend/, $(ARCH)/) @@ -106,16 +107,16 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ Cshmgen.v Cshmgenproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v -# LR(1) parser validator - -PARSERVALIDATOR=Alphabet.v Interpreter_complete.v Interpreter.v \ - Validator_complete.v Automaton.v Interpreter_correct.v Main.v \ - Validator_safe.v Grammar.v Interpreter_safe.v Tuples.v - # Parser PARSER=Cabs.v Parser.v +# MenhirLib + +MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \ + Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \ + Validator_safe.v Validator_classes.v + # Putting everything together (in driver/) DRIVER=Compopts.v Compiler.v Complements.v @@ -123,7 +124,7 @@ DRIVER=Compopts.v Compiler.v Complements.v # All source files FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ - $(PARSERVALIDATOR) $(PARSER) + $(MENHIRLIB) $(PARSER) # Generated source files @@ -145,7 +146,6 @@ ifeq ($(CLIGHTGEN),true) $(MAKE) clightgen endif - proof: $(FILES:.v=.vo) # Turn off some warnings for compiling Flocq @@ -229,7 +229,7 @@ driver/Version.ml: VERSION cparser/Parser.v: cparser/Parser.vy @rm -f $@ - $(MENHIR) $(MENHIR_FLAGS) --coq cparser/Parser.vy + $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy @chmod a-w $@ depend: $(GENERATED) depend1 |