diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1ed308fbe2e3c7a98dc272d43e4473ad77868d50..6c476bdc22580c33b197836782dfaefb7734c055 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -30,6 +30,11 @@ variables: ################################################################################ ### PREPARE +check-makefile: + stage: prepare + script: + - ./nix/shell-checkers.sh "make --warn-undefined-variables help > /dev/null 2> errors && [[ "$(cat errors)" == "" ]]" + check-no-old-frama-c: stage: prepare script: diff --git a/Makefile b/Makefile index 97057c87d67f18146d12e0892271a9dd521fc17d..92ccb6f36b481cf0198b9f721cc00d5c4b3864f2 100644 --- a/Makefile +++ b/Makefile @@ -43,12 +43,16 @@ FRAMAC_LINTCK_SRC:=tools/lint .PHONY: all +DUNE_WS?= + ifneq (${DUNE_WS},) WORKSPACE_OPT:=--workspace dev/dune-workspace.${DUNE_WS} else WORKSPACE_OPT:= endif +DISABLED_PLUGINS?= + all:: ifeq (${FRAMAC_DEVELOPER},yes) dune build --no-print-directory --root ${FRAMAC_LINTCK_SRC} diff --git a/ivette/Makefile.installation b/ivette/Makefile.installation index 53fa6bd109860db169c2854a87800d9825d86f6e..214b5aaad5c88a3c53d16c9287ac87ea9c14aed5 100644 --- a/ivette/Makefile.installation +++ b/ivette/Makefile.installation @@ -32,6 +32,8 @@ FILTER= \ --exclude "_build" \ --exclude "node_modules" \ +OS?= + ifndef PREFIX then install:: @@ -56,5 +58,5 @@ uninstall:: @rm -f "${FULLPREFIX}/lib/frama-c/ivette.tgz" @rm -fr "${FULLPREFIX}/lib/frama-c/Ivette.app" @rm -fr "${FULLPREFIX}/lib/frama-c/ivette" - + endif diff --git a/share/Makefile.common b/share/Makefile.common index e4f009831c4328d7a357b0880c4ae57a986b0c82..ae9d02f9d7e0696f0d75f9ac783aba62f24de892 100644 --- a/share/Makefile.common +++ b/share/Makefile.common @@ -65,6 +65,8 @@ endif endif endif +DESTDIR?= + ############# # Verbosing # ############# diff --git a/share/Makefile.headers b/share/Makefile.headers index c5226fa4f4fd9098233fbe387427fe628d32704d..b55d1a6919c60a5d538abc01f158d1fa686ad8cd 100644 --- a/share/Makefile.headers +++ b/share/Makefile.headers @@ -62,6 +62,10 @@ HEADER_EXCEPTIONS?= # Extra parameters for "frama-c-hdrck" HDRCK_EXTRA?= +# Can be set to a file +# - <file>: file containing the header specification for distributed files +HEADER_DISTRIB_FILE?= + ########################################################################## ## Tools diff --git a/share/Makefile.testing b/share/Makefile.testing index e435ecc129023e3e86ec273d6d1917f880a9cc9c..1856b10afb4a28141ac4db5ae0ba114b1835043d 100644 --- a/share/Makefile.testing +++ b/share/Makefile.testing @@ -40,6 +40,12 @@ PTEST_DEPS?= PTEST_USE_WP_CACHE?=no # Defines the related dune targets PTEST_ALIASES?=$(addsuffix /ptests,$(addprefix @,$(PTEST_DIRS))) +# Ptests command +FRAMAC_PTEST?= +# Wtests command +FRAMAC_WTEST?= + +FRAMAC_WP_QUALIF?= ifneq ($(FRAMAC_WP_QUALIF),) FRAMAC_WP_CACHEDIR=$(FRAMAC_WP_QUALIF)