diff --git a/Makefile b/Makefile index cfc27bfac27e51dceebf5c55cf807ef54bce06a3..8383af72bdfadee6a04665cddf4ed0183b8b673f 100644 --- a/Makefile +++ b/Makefile @@ -193,16 +193,24 @@ endif # HEADER MANAGEMENT ################################ +# HDRCK is internal FRAMAC_HDRCK:=headers/hdrck.exe # Part that can be shared for external plugins include share/Makefile.headers ############################################################################### - # Testing +################################ + +# PTESTS is internal +FRAMAC_PTESTS:=ptests/ptests.exe -include Makefile.testing +# WTESTS is internal +FRAMAC_WTESTS:=ptests/wtests.exe + +# Part that can be shared for external plugins +include share/Makefile.testing ############################################################################### diff --git a/Makefile.testing b/share/Makefile.testing similarity index 72% rename from Makefile.testing rename to share/Makefile.testing index 0936111d0891d9e8b97a78ad38ebfaeedc364475..4496fd212ce2941432ca4503cbde1b9f813f96a3 100644 --- a/Makefile.testing +++ b/share/Makefile.testing @@ -36,35 +36,68 @@ PTEST_ALIASES=$(addsuffix /ptests,$(addprefix @, tests src/plugins)) .PHONY: tests.info tests.info: - echo "PURGED_PTEST_DIRS=$(PURGED_PTEST_DIRS)" - echo "PTEST_DIRS=$(PTEST_DIRS)" - echo "PTEST_OPTS=$(PTEST_OPTS)" - echo "PTEST_ALIASES=$(PTEST_ALIASES)" + echo "FRAMAC_WTESTS='$(FRAMAC_WTESTS)'" + echo "WTESTS='$(WTESTS)'" + echo "FRAMAC_PTESTS='$(FRAMAC_PTESTS)'" + echo "PTESTS='$(PTESTS)'" + echo "PURGED_PTEST_DIRS='$(PURGED_PTEST_DIRS)'" + echo "PTEST_DIRS='$(PTEST_DIRS)'" + echo "PTEST_OPTS='$(PTEST_OPTS)'" + echo "PTEST_ALIASES='$(PTEST_ALIASES)'" -# Note: the public name of ptest.exe is frama-c-ptests -ptests/ptests.exe: ptests/ptests.ml - dune build --root ptests ptests.exe +########################################################################## +## Command used to execute ptests (in order to generate dune test files) -# Note: the public name of wtest.exe is frama-c-wtests -ptests/wtests.exe: ptests/wtests.ml - dune build --root ptests wtests.exe +# Note: the public name of ptests.exe is frama-c-ptests +ifeq ($(FRAMAC_PTESTS),"") + +# PTESTS is external +PTESTS=frama-c-ptests + +else -# Command for executing ptest (in order to generate dune test files) +# PTESTS is internal PTESTS=dune exec --root ptests -- frama-c-ptests #PTESTS=dune exec --root ptests -- frama-c-ptests -v +# Note: the public name of ptest.exe is frama-c-ptests +$(FRAMAC_PTESTS): ptests/ptests.ml + dune build --root ptests ptests.exe + +endif + .PHONY: ptests-help ptests-help: $(PTESTS) --help -# Note: wrapper that can be used during dune testing (c.f. frama-c-ptests) +########################################################################## +## Command used to execute wtests, the wrapper that can be used during +## dune testing (c.f. frama-c-ptests) + +# Note: the public name of wtests.exe is frama-c-wtests +ifeq ($(FRAMAC_WTESTS),"") + +# WTESTS is external to Frama-C +WTESTS=frama-c-wtests + +else + +# WTESTS is internal to Frama-C WTESTS=dune exec --root ptests -- frama-c-wtests +# Note: the public name of wtest.exe is frama-c-wtests +$(FRAMAC_WTESTS): ptests/wtests.ml + dune build --root ptests wtests.exe + +endif + .PHONY: wtests-help wtests-help: $(WTESTS) --help -# Removes all dune files generated for testing: xargs -n 10 avoids a too long line +########################################################################## +## Removes all dune files generated for testing: xargs -n 10 avoids a too long line + .PHONY: purge-tests purge-tests: find $(PURGED_PTEST_DIRS) -name dune -print0 \ @@ -76,13 +109,15 @@ purge-tests: clean-tests: purge-tests rm -rf $(addprefix _build/default/,$(PURGED_PTEST_DIRS)) -# Generates all dune files used for testing +########################################################################## +## Generates all dune files used for testing + .PHONY: run-ptests -run-ptests: config.sed purge-tests ptests/ptests.exe ptests/wtests.exe +run-ptests: config.sed purge-tests $(FRAMAC_PTEST) $(FRAMAC_WTEST) $(PTESTS) $(PTEST_OPTS) $(PTEST_DIRS) .PHONY: run-ptests.replay -run-ptests.replay: config.sed ptests/ptests.exe +run-ptests.replay: config.sed $(FRAMAC_PTEST) $(PTESTS) $(PTEST_OPTS) $(PTEST_DIRS) # Run tests of for all configurations (and build all dune files)