From b65bf2e23dd27ba468eb5061b88da1f8551bb801 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 8 Jun 2022 17:26:32 +0200
Subject: [PATCH] [Makefile] updates about testing

---
 Makefile                                   | 12 +++-
 Makefile.testing => share/Makefile.testing | 67 ++++++++++++++++------
 2 files changed, 61 insertions(+), 18 deletions(-)
 rename Makefile.testing => share/Makefile.testing (72%)

diff --git a/Makefile b/Makefile
index cfc27bfac27..8383af72bdf 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 0936111d089..4496fd212ce 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)
-- 
GitLab