Skip to content
Snippets Groups Projects
Commit 477ef0e4 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'feature/dune/lint-headers-targets-related-to-commits' into 'master' 

[Makefile] adds/modifies  lint and header targets related to commits

Closes #1099

See merge request frama-c/frama-c!3846
parents 14465a75 18b6b1c5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
dev/git-hooks/pre-commit → dev/git-hooks/pre-commit.sh
+ 20
− 16
View file @ 477ef0e4
#!/bin/bash
# -*- mode: bash
##########################################################################
# #
# This file is part of Frama-C. #
......@@ -22,21 +21,26 @@
# #
##########################################################################
if git rev-parse --verify HEAD >/dev/null 2>&1
then
against=HEAD
else
# Initial commit: diff against an empty tree object
against=4b825dc642cb6eb9a060e54bf8d69288fbee4904
fi
# Examples of installation of this pre-commit hook (client side):
# - cp ./dev/git-hooks/pre-commit.sh .git/hooks/pre-commit
# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-commit.sh pre-commit)
# Note:
# - that checks the unstaged version of the files and these files are
# only commited with a `git commit -a` command.
# - so, a `git commit` command may checks the wrong version of a file.
echo "Pre-commit Hook..."
if git config --get frama-c.makelevel > /dev/null 2>&1 ; then
MAKELEVEL=-j$(git config --int --get frama-c.makelevel);
else
MAKELEVEL=-j4;
# Extract the files that have both an unstaged version and a staged one.
UNSTAGED="git diff --name-status"
STAGED="git diff --name-status --cached"
(($UNSTAGED ; $STAGED) | sed "s:^.::" | sort -u) | diff - <(($UNSTAGED ; $STAGED) | sed "s:^.::" | sort)
if [ "$?" != "0" ]; then
echo "WARNING: These previous files are both unstaged and in the index."
echo " They will be verified only for a 'git commit -a' command."
fi
MANUAL_ML_FILES=\
$(git diff-index --name-only --diff-filter d $against | \
grep -e '^src/.*\.mli\?$' | tr '\n' ' ') \
make ${MAKELEVEL} lint
# Verifies the current version of files
make lint.before-commit-a
make check-headers.before-commit-a
share/Makefile.headers
+ 133
− 39
View file @ 477ef0e4
......@@ -30,7 +30,9 @@
# Must be unset (for external plugins) and set (for FRAMA-C kernel)
FRAMAC_HDRCK?=
# Can be set to no
HDRCK?=frama-c-hdrck
# Can be set to no/yes
# - yes: adds "-exit-on-warning" option to "frama-c-hdrck"
HEADER_STRICT?=yes
......@@ -67,6 +69,13 @@ HEADER_SAVE_SPEC?=no
# Extra parameters for "frama-c-hdrck"
HDRCK_EXTRA?=
##########################################################################
## Tools
GIT ?= git
DUNE ?= dune
TEE ?= tee
##########################################################################
## Command used to execute hdrck
......@@ -74,113 +83,116 @@ HDRCK_EXTRA?=
ifeq ($(FRAMAC_HDRCK),)
# HDRCK is external
HDRCK:= frama-c-hdrck
HDRCK.CMD:= $(HDRCK)
else
# HDRCK is internal
HDRCK:= dune exec --root $(FRAMAC_HDRCK_SRC) -- frama-c-hdrck
HDRCK.CMD:= $(DUNE) exec --root $(FRAMAC_HDRCK_SRC) -- $(HDRCK)
$(FRAMAC_HDRCK): $(FRAMAC_HDRCK_SRC)/hdrck.ml
dune build --root $(FRAMAC_HDRCK_SRC) hdrck.exe
$(FRAMAC_HDRCK): tools/hdrck/hdrck.ml
$(DUNE) build --root $(FRAMAC_HDRCK_SRC) hdrck.exe
endif
HDRCK_OPTS:= --stdin
HDRCK.OPTS:= --stdin
######################################################################
## Identifies how to get the header specification (from git/find/cat)
## and updates HDRCK_OPTS variable
## and updates HDRCK.OPTS variable
HDRCK.FILE_LIST=$(GIT) ls-files -z
HDRCK.FILE_ATTR=$(GIT) check-attr --stdin -z header_spec
ifeq ($(HEADER_SPEC),)
HEADER_HAS_GIT:=$(wildcard .git)
ifneq ($(HEADER_HAS_GIT),)
HDRCK.HAS_GIT:=$(wildcard .git)
ifneq ($(HDRCK.HAS_GIT),)
# From git (including git work-trees)
HDRCK_SPEC:= git ls-files -z | git check-attr --stdin -z header_spec
HDRCK_OPTS+= -z
HDRCK.SPEC:=$(HDRCK.FILE_LIST) | $(HDRCK.FILE_ATTR)
HDRCK.OPTS+= -z
else
# Note: in such a case, GIT is required...
HDRCK_SPEC:=
HDRCK.SPEC:=
endif # HEADER_HAS_GIT
endif # HDRCK.HAS_GIT
else # HEADER_SPEC
ifeq ($(HEADER_SAVE_SPEC),yes)
HEADER_HAS_GIT:=$(wildcard .git)
ifneq ($(HEADER_HAS_GIT),)
HDRCK.HAS_GIT:=$(wildcard .git)
ifneq ($(HDRCK.HAS_GIT),)
# From git (including git work-trees)
HDRCK_SPEC:= git ls-files -z | git check-attr --stdin -z header_spec | tee $(HEADER_SPEC)
HDRCK_OPTS+= -z
HDRCK.SPEC:= $(HDRCK.FILE_LIST) | $(HDRCK.FILE_ATTR) | $(TEE) $(HEADER_SPEC)
HDRCK.OPTS+= -z
else
# Note: in such a case, GIT is required...
HDRCK_SPEC:=
HDRCK.SPEC:=
endif # HEADER_HAS_GIT
endif # HDRCK.HAS_GIT
else # HEADER_SAVE_SPEC
# From a file
HDRCK_SPEC:= cat $(HEADER_SPEC)
HDRCK.SPEC:= cat $(HEADER_SPEC)
# The file format can be overloaded in using the var HDRCK_EXTRA
HDRCK_OPTS+= -spec-format 3-zeros
HDRCK.OPTS+= -spec-format 3-zeros
endif # HEADER_SAVE_SPEC
endif # HEADER_SPEC
################################
## Updates HDRCK_OPTS variable
## Updates HDRCK.OPTS variable
ifneq ($(HEADER_DISTRIB_FILE),)
# Adds the option "-distrib-file"
HDRCK_OPTS+= -distrib-file $(HEADER_DISTRIB_FILE)
HDRCK.OPTS+= -distrib-file $(HEADER_DISTRIB_FILE)
endif
ifneq ($(HEADER_EXCEPTIONS),)
# Adds the option "-header-except-file"
HDRCK_OPTS+= -header-except-file $(HEADER_EXCEPTIONS)
HDRCK.OPTS+= -header-except-file $(HEADER_EXCEPTIONS)
endif
ifneq ($(HEADER_REPO),)
# Adds the option "-C"
HDRCK_OPTS+= -C $(HEADER_REPO)
HDRCK.OPTS+= -C $(HEADER_REPO)
endif
ifeq ($(HEADER_STRICT),yes)
# Adds the option "-exit-on-warning"
HDRCK_OPTS+= -exit-on-warning
HDRCK.OPTS+= -exit-on-warning
endif
#####################################
## Identifies where are the headers
## and updates HDRCK_OPTS variable
## and updates HDRCK.OPTS variable
ifeq ($(HEADER_OPEN_SOURCE),yes)
HDRCK_OPTS+= $(addprefix -header-dirs=,$(addsuffix /open-source,$(HEADER_DIRS)))
HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /open-source,$(HEADER_DIRS)))
else
ifeq ($(HEADER_OPEN_SOURCE),no)
HDRCK_OPTS+= $(addprefix -header-dirs=,$(addsuffix /close-source,$(HEADER_DIRS)))
HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /close-source,$(HEADER_DIRS)))
else
ifeq ($(HEADER_OPEN_SOURCE),)
HDRCK_OPTS+= $(addprefix -header-dirs=,$(HEADER_DIRS))
HDRCK.OPTS+= $(addprefix -header-dirs=,$(HEADER_DIRS))
else
HDRCK_OPTS+= $(addprefix -header-dirs=,$(addsuffix /$(HEADER_OPEN_SOURCE),$(HEADER_DIRS)))
HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /$(HEADER_OPEN_SOURCE),$(HEADER_DIRS)))
endif
endif
endif
#################################
ifeq ($(HDRCK_SPEC),)
ifeq ($(HDRCK.SPEC),)
.PHONY: check-headers
check-headers: $(FRAMAC_HDRCK)
......@@ -192,22 +204,103 @@ headers: $(FRAMAC_HDRCK)
$(error "Please set HEADER_SPEC variable to a file containing the header specification.")
else
ifneq ($(HDRCK.HAS_GIT),)
define HDRCK.file-list-from-git-diff
$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) "s/^.[ \t]*//" | $(TR) '\n' '\000' | $(HDRCK.FILE_ATTR)
endef
HDRCK.main-targets=check-headers headers
define HDRCK.file-list-filter-with-git-diff
HDRCK.$(1)-filter-targets=$$(addsuffix .$(1),$$(HDRCK.main-targets))
.PHONY: $(LINT.$(1)-filter-targets)
$$(HDRCK.$(1)-filter-targets):: HDRCK.SPEC=$$(call HDRCK.file-list-from-git-diff,$(2))
$$(HDRCK.$(1)-filter-targets):: %.$(1) : $(3) %
@echo [HDRCK] Done: HDRCK_DIFF=\"$(2)\" make $$(basename $$@)
@echo [HDRCK] checked file list:
$$(GIT) diff --name-status $(2)
endef
ifneq ($(HEADER_DIFF),)
$(info [HDRCK] Looking at files modified from branch/commit: '$(HEADER_DIFF)')
HDRCK.SPEC=$(call LINT.file-list-from-git-diff,$(HEADER_DIFF))
$(info $(HEADER.FILE_LIST))
endif # $(HEADER_DIFF)
#### rules for make <headers-target>.before-push
## looks at files modified from origin/$(git branch --show-current) and checks that there is no staged nor unstaged files
PHONY: HDRCK.checked-unmodified-ok
HDRCK.checked-unmodified-ok:
$(eval HDRCK.checked-unmodified := $(shell $(GIT) diff --name-status HEAD | $(WC) -l))
if [ 0 != $(HDRCK.checked-unmodified) ]; then \
echo "[HDRCK] Staged or unstaged files=$(HDRCK.checked-unmodified):"; \
$(GIT) diff --name-status HEAD; \
echo "[HDRCK] Error: may check some staged or unstaged file versions" ; \
exit 1; \
fi;
$(eval $(call HDRCK.file-list-filter-with-git-diff,before-push,--cached origin/$(shell git branch --show-current),HDRCK.checked-unmodified-ok))
#### rules for make <headers-target>.unstaged
## looks at unstaged files
$(eval $(call HDRCK.file-list-filter-with-git-diff,unstaged, ))
#### rules for make <headers-target>.before-commit
## looks at staged files and checks that there is no unstaged files
PHONY: HDRCK.checked-unstaged-ok
HDRCK.checked-unstaged-ok:
$(eval HDRCK.checked-unstaged := $(shell $(GIT) diff --name-status | $(WC) -l))
if [ 0 != $(HDRCK.checked-unstaged) ]; then \
echo "[HDRCK] Unstaged files=$(HDRCK.checked-unstaged):"; \
$(GIT) diff --name-status ; \
echo "[HDRCK] Error: may check some unstaged version files version." ; \
exit 1; \
fi;
$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit,--cached HEAD,HDRCK.checked-unstaged-ok))
#### rules for make <headers-target>.before-commit-a
## looks at unstaged and staged files
$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit-a,HEAD,))
#### rules for make <headers-target>.before-commit-a--ammend
## looks at unstaged, staged and previously committed files
$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit-a--ammend,HEAD~1,))
#### rules for make <headers-target>.before-commit--amend
## looks at staged and previously committed files and checks that there is no unstaged files
$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit--ammend,HEAD~1,HDRCK.checked-unstaged-ok))
#### rules for make <headers-target>.previous-commit
## looks at files of the last commit and checks that there is no staged nor unstaged files
$(eval $(call HDRCK.file-list-filter-with-git-diff,previous-commit,HEAD~1,HDRCK.checked-unmodified-ok))
endif # $(HDRCK.HAS_GIT)
.PHONY: check-headers
check-headers: $(FRAMAC_HDRCK)
$(HDRCK_SPEC) | $(HDRCK) $(HDRCK_OPTS) $(HDRCK_EXTRA)
$(HDRCK.SPEC) | $(HDRCK.CMD) $(HDRCK.OPTS) $(HDRCK_EXTRA)
.PHONY: headers
headers: $(FRAMAC_HDRCK)
$(HDRCK_SPEC) | $(HDRCK) -update $(HDRCK_OPTS) $(HDRCK_EXTRA)
$(HDRCK.SPEC) | $(HDRCK.CMD) -update $(HDRCK.OPTS) $(HDRCK_EXTRA)
endif # $(HDRCK_SPEC)
endif # $(HDRCK.SPEC)
#################################
.PHONY: headers.info
headers.info:
echo "FRAMAC_HDRCK='$(FRAMAC_HDRCK)'"
echo "HEADER_HAS_GIT='$(HEADER_HAS_GIT)'"
echo "HEADER_OPEN_SOURCE='$(HEADER_OPEN_SOURCE)'"
echo "HEADER_STRICT='$(HEADER_STRICT)'"
echo "HEADER_DIRS='$(HEADER_STRICT)'"
......@@ -215,9 +308,10 @@ headers.info:
echo "HEADER_EXCEPTIONS='$(HEADER_EXCEPTIONS)'"
echo "HEADER_REPO='$(HEADER_REPO)'"
echo "HEADER_SPEC='$(HEADER_SPEC)'"
echo "HDRCK='$(HDRCK)'"
echo "HDRCK_SPEC='$(HDRCK_SPEC)'"
echo "HDRCK_OPTS='$(HDRCK_OPTS)'"
echo "HDRCK.HAS_GIT='$(HDRCK.HAS_GIT)'"
echo "HDRCK.CMD='$(HDRCK.CMD)'"
echo "HDRCK.SPEC='$(HDRCK.SPEC)'"
echo "HDRCK.OPTS='$(HDRCK.OPTS)'"
###############################################################################
......
share/Makefile.linting
+ 3
− 3
View file @ 477ef0e4
......@@ -217,8 +217,8 @@ LINT.$(1)-filter-targets=$$(addsuffix .$(1),$$(LINT.main-targets))
$$(LINT.$(1)-filter-targets):: LINT.FILE_LIST=$$(call LINT.file-list-from-git-diff,$(2))
$$(LINT.$(1)-filter-targets):: %.$(1) : $(3) %
@echo [LINT] Done: LINT_DIFF=\"$(2)\" make $$(basename $$@)
@echo [LINT] git diff --name-status
$$(GIT) diff --name-status HEAD
@echo [LINT] checked file list:
$$(GIT) diff --name-status $(2)
endef
ifeq ($(LINT_DIFF),)
......@@ -262,7 +262,7 @@ LINT.checked-unstaged-ok:
exit 1; \
fi;
$(eval $(call LINT.file-list-filter-with-git-diff,staged,--cached HEAD,LINT.checked-unstaged-ok))
$(eval $(call LINT.file-list-filter-with-git-diff,before-commit,--cached HEAD,LINT.checked-unstaged-ok))
#### rules for make <lint-target>.before-commit-a
## looks at unstaged and staged files
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment