diff --git a/Makefile b/Makefile
index 7a62602f3aef3a28b0419d968f24f9bf2d31f629..81cce48e4319a4f780159c3f53c6d3c9c442931a 100644
--- a/Makefile
+++ b/Makefile
@@ -27,16 +27,14 @@ MAKECONFIG_DIR=share
include $(MAKECONFIG_DIR)/Makefile.common
##############################################################################
-# PTESTS SRC
+# TOOLS CONFIG
################################
-FRAMAC_PTESTS_SRC:=tools/ptests
-
-##############################################################################
-# HDRCK SRC
-################################
+IN_FRAMAC:=yes
+FRAMAC_PTESTS_SRC:=tools/ptests
FRAMAC_HDRCK_SRC:=tools/hdrck
+FRAMAC_LINTCK_SRC:=tools/lint
##############################################################################
# Frama-C
@@ -80,9 +78,6 @@ include ivette/Makefile.installation
# HEADER MANAGEMENT
################################
-# HDRCK is internal
-FRAMAC_HDRCK:=headers/hdrck.exe
-
# Part that can be shared for external plugins
include share/Makefile.headers
@@ -112,8 +107,6 @@ include share/Makefile.testing
# Linters
################################
-###############################################################################
-
# Code prettyfication and lint
include share/Makefile.linting
diff --git a/dev/check-files.sh b/dev/check-files.sh
new file mode 100755
index 0000000000000000000000000000000000000000..60cb4899acf926f7457a17a351b32eb3506d4a19
--- /dev/null
+++ b/dev/check-files.sh
@@ -0,0 +1,120 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+THIS_SCRIPT="$0"
+LINT=check-lint
+HDRCK=check-headers
+DO_LINT="yes"
+DO_HDRCK="yes"
+REFERENCE=
+MODE="all"
+
+while [ "$1" != "" ]
+do
+ case "$1" in
+ "-h"|"-help"|"--help")
+ echo "${THIS_SCRIPT} [OPTIONS]"
+ echo "OPTIONS"
+ echo " -h|-help|--help print this message and exit"
+ echo " -f|--fix fix files"
+ echo " -c|--commit check modified files to be commited only"
+ echo " -p|--push check modified files to be pushed only"
+ echo " --no-headers do not check headers"
+ echo " --no-lint do not check lint"
+ exit 0
+ ;;
+ "-f"|"--fix")
+ LINT=lint
+ HDRCK=headers
+ ;;
+ "-p"|"--push")
+ REFERENCE="origin/$(git rev-parse --abbrev-ref HEAD)"
+ MODE="push"
+ ;;
+ "-c"|"--commit")
+ MODE="commit"
+ ;;
+ "--no-headers")
+ DO_HDRCK="no"
+ ;;
+ "--no-lint")
+ DO_LINT="no"
+ ;;
+ *)
+ echo "Unknown option '$1'"
+ exit 2
+ ;;
+ esac
+ shift
+done
+
+if [ "$MODE" = "all" ]; then
+ if [ $DO_LINT = "yes" ] ; then
+ make $LINT || exit 1
+ fi
+ if [ $DO_HDRCK = "yes" ] ; then
+ make $HDRCK HDRCK_EXTRA="-quiet" || exit 1
+ fi
+else
+ STAGED=$(git diff --diff-filter ACMR --name-only --cached $REFERENCE | sort)
+ UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
+
+ if [ "$STAGED" = "" ];
+ then
+ echo "No staged modification since last $MODE, nothing to do."
+ exit 0
+ fi
+
+ if [ "$UNSTAGED" != "" ];
+ then
+ INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
+
+ if [ "$INTER" != "" ];
+ then
+ echo "Cannot validate push."
+ echo "The following staged files have been modified, renamed or deleted."
+ for file in $INTER ; do
+ echo "- $file"
+ done
+ exit 1
+ fi
+ fi
+
+ STAGED=$(echo $STAGED | tr '\n' ' ')
+
+ TMP=$(mktemp)
+
+ cleanup () {
+ rm "$TMP"
+ }
+ trap cleanup exit
+
+ git check-attr -za $STAGED > "$TMP"
+ if [ $DO_LINT = "yes" ] ; then
+ make $LINT LINTCK_FILES_INPUT="$TMP" || exit 1
+ fi
+ git check-attr -z header_spec $STAGED > "$TMP"
+ if [ $DO_HDRCK = "yes" ] ; then
+ make $HDRCK HDRCK_FILES_INPUT="$TMP" HDRCK_EXTRA="-quiet" || exit 1
+ fi
+fi
diff --git a/dev/git-hooks/pre-commit.sh b/dev/git-hooks/pre-commit.sh
index 3f376ce71e3bb85da9bb1c3ca551bfd4905875f3..0f460288e035b37a0005579ac86f16db4524ea5f 100755
--- a/dev/git-hooks/pre-commit.sh
+++ b/dev/git-hooks/pre-commit.sh
@@ -21,26 +21,20 @@
# #
##########################################################################
-# Examples of installation of this pre-commit hook (client side):
-# - cp ./dev/git-hooks/pre-commit.sh .git/hooks/pre-commit
+# Example of installation of this pre-commit hook (client side):
# - (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.
+# Note: if you decide to copy the file, the `SCRIPT_DIR` variable must be
+# fixed accordingly.
echo "Pre-commit Hook..."
-# 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."
+STAGED=$(git diff --diff-filter ACMR --name-only --cached | sort)
+
+if [ "$STAGED" = "" ];
+then
+ echo "Empty commit, nothing to do"
+ exit 0
fi
-# Verifies the current version of the files
-make lint.before-commit-a || exit 1
-make check-headers.before-commit-a || exit 1
+SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
+"$SCRIPT_DIR/../check-files.sh" -c || exit 1
diff --git a/dev/git-hooks/pre-push.sh b/dev/git-hooks/pre-push.sh
new file mode 100755
index 0000000000000000000000000000000000000000..d06723672d1f370c970b72816d144b073419231d
--- /dev/null
+++ b/dev/git-hooks/pre-push.sh
@@ -0,0 +1,40 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Example of installation of this pre-push hook (client side):
+# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-push.sh pre-push)
+# Note: if you decide to copy the file, the `SCRIPT_DIR` variable must be
+# fixed accordingly.
+
+echo "Pre-push Hook..."
+
+STAGED=$(git diff --diff-filter ACMR --name-only --cached origin/$(git rev-parse --abbrev-ref HEAD) | sort)
+
+if [ "$STAGED" = "" ];
+then
+ echo "No diff since last push, nothing to do"
+ exit 0
+fi
+
+SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
+"$SCRIPT_DIR/../check-files.sh" -p || exit 1
diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix
index de0483335050f1ba782ec032815c3c65804e1f3b..40a0406a77685de48266658d19caeb00488df77f 100644
--- a/nix/frama-c-checkers-shell.nix
+++ b/nix/frama-c-checkers-shell.nix
@@ -2,6 +2,7 @@
, stdenv
, clang_10
, frama-c-hdrck
+, frama-c-lint
, git
, git-lfs
, gnumake
@@ -13,6 +14,7 @@ stdenv.mkDerivation rec {
buildInputs = [
clang_10
frama-c-hdrck
+ frama-c-lint
git
git-lfs
gnumake
diff --git a/nix/frama-c-lint.nix b/nix/frama-c-lint.nix
new file mode 100644
index 0000000000000000000000000000000000000000..d33b25870079d5d24d2ba1a685ac8b1b3a203d82
--- /dev/null
+++ b/nix/frama-c-lint.nix
@@ -0,0 +1,40 @@
+{ lib
+, stdenv
+, camomile
+, dune_3
+, findlib
+, gitignoreSource
+, ocaml
+, ocp-indent
+} :
+
+stdenv.mkDerivation rec {
+ pname = "frama-c-lint";
+ version =
+ lib.strings.replaceStrings ["~"] ["-"]
+ (lib.strings.removeSuffix "\n"
+ (builtins.readFile ../VERSION));
+ slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
+
+ src = gitignoreSource ./../tools/lint ;
+
+ buildInputs = [
+ camomile
+ dune_3
+ findlib
+ ocaml
+ ocp-indent
+ ];
+
+ configurePhase = ''
+ true
+ '';
+
+ buildPhase = ''
+ dune build --root .
+ '';
+
+ installPhase = ''
+ dune install --prefix $out --root .
+ '';
+}
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index ac981c7f92d2b247dec972d682a52d2ee7086a9d..29f6fac278d81b7afa32f749aeee2d3f91a3694f 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -12,6 +12,7 @@
# Frama-C build
, apron
, camlzip
+, camomile
, dune_3
, dune-configurator
, dune-site
@@ -25,6 +26,7 @@
, ocaml
, ocamlgraph
, ocamlgraph_gtk
+, ocp-indent
, ppx_deriving
, ppx_deriving_yojson
, ppx_import
@@ -63,6 +65,7 @@ stdenvNoCC.mkDerivation rec {
buildInputs = [
apron
camlzip
+ camomile
dune_3
dune-configurator
dune-site
@@ -77,6 +80,7 @@ stdenvNoCC.mkDerivation rec {
ocaml
ocamlgraph
ocamlgraph_gtk
+ ocp-indent
ppx_deriving
ppx_deriving_yojson
ppx_import
diff --git a/nix/ocp-indent.nix b/nix/ocp-indent.nix
index 089d6ac9b6dc8049477d520e8fbfc8a5fba391e9..395c663ae31eda896f4d25b91ddd035d071b5134 100644
--- a/nix/ocp-indent.nix
+++ b/nix/ocp-indent.nix
@@ -1,5 +1,6 @@
{ lib
, fetchFromGitHub
+, findlib
, buildDunePackage
, cmdliner
}:
@@ -18,7 +19,7 @@ buildDunePackage rec {
minimumOCamlVersion = "4.02";
useDune2 = true;
- buildInputs = [ cmdliner ];
+ buildInputs = [ cmdliner findlib ];
meta = with lib; {
homepage = http://typerex.ocamlpro.com/ocp-indent.html;
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 522be707e117795dfd820ffac5c6b68f8cbf030d..113c31eac7b511a4c92b08d322069ab4042b8940 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -28,6 +28,7 @@ let
# Builds
frama-c = oself.callPackage ./frama-c.nix {};
frama-c-hdrck = oself.callPackage ./frama-c-hdrck.nix {};
+ frama-c-lint = oself.callPackage ./frama-c-lint.nix {};
lint = oself.callPackage ./lint.nix {};
# Tests
diff --git a/share/Makefile.headers b/share/Makefile.headers
index 7e0beb06fc8fee2a3626bc86f3c1c9e892fc600a..5afbe5a533a97eba7aaee60396db746ed39b46ab 100644
--- a/share/Makefile.headers
+++ b/share/Makefile.headers
@@ -28,7 +28,7 @@
# Parameters
# Must be unset (for external plugins) and set (for FRAMA-C kernel)
-FRAMAC_HDRCK?=
+IN_FRAMAC?=
HDRCK?=frama-c-hdrck
@@ -50,22 +50,15 @@ HEADER_OPEN_SOURCE?=yes
# - <dir>: directory containing the files to manage
HEADER_REPO?=
-# Can be set to a file
-# - <file>: file containing the list of the files to manage
-HEADER_DISTRIB_FILE?=
+# Can be set to a
+# - <file> containing files to check/update and their attributes, with 0
+# separators (like 'git ls-files -z | git check-attr --stdin -z header_spec').
+HDRCK_FILES_INPUT?=
# Can be set to a file
# - <file>: file containing the list of the files to ignore any way
HEADER_EXCEPTIONS?=
-# Can be set to a file
-# - <files>: input file containing, for each file to manage, the "header_spec" attribute value
-HEADER_SPEC?=
-
-# Can be set to a file
-# - yes: save the "header_spec" attribute specification into the file "HEADER_SPEC"
-HEADER_SAVE_SPEC?=no
-
# Extra parameters for "frama-c-hdrck"
HDRCK_EXTRA?=
@@ -74,82 +67,19 @@ HDRCK_EXTRA?=
GIT ?= git
DUNE ?= dune
-TEE ?= tee
##########################################################################
## Command used to execute hdrck
-# Note: the public name of hdrck.exe is frama-c-hdrck
-ifeq ($(FRAMAC_HDRCK),)
-
-# HDRCK is external
+ifneq ($(IN_FRAMAC),yes)
HDRCK.CMD:= $(HDRCK)
-
else
-
-# HDRCK is internal
-HDRCK.CMD:= $(DUNE) exec --root $(FRAMAC_HDRCK_SRC) -- $(HDRCK)
-
-$(FRAMAC_HDRCK): tools/hdrck/hdrck.ml
- $(DUNE) build --root $(FRAMAC_HDRCK_SRC) hdrck.exe
-
+HDRCK.CMD:= $(DUNE) exec --no-print-directory --root $(FRAMAC_HDRCK_SRC) -- $(HDRCK)
endif
-HDRCK.OPTS:= --stdin
-
-######################################################################
-## Identifies how to get the header specification (from git/find/cat)
-## 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),)
-
-HDRCK.HAS_GIT:=$(shell git rev-parse --is-inside-work-tree 2> /dev/null)
-ifeq ($(HDRCK.HAS_GIT),true)
-
-# From git (including git work-trees)
-HDRCK.SPEC:=$(HDRCK.FILE_LIST) | $(HDRCK.FILE_ATTR)
-HDRCK.OPTS+= -z
-
-else
+HDRCK.OPTS:= --stdin -z -spec-format 3-zeros
-# Note: in such a case, GIT is required...
-HDRCK.SPEC:=
-
-endif # HDRCK.HAS_GIT
-
-else # HEADER_SPEC
-
-ifeq ($(HEADER_SAVE_SPEC),yes)
-
-HDRCK.HAS_GIT:=$(shell git rev-parse --is-inside-work-tree 2> /dev/null)
-ifeq ($(HDRCK.HAS_GIT),true)
-
-# From git (including git work-trees)
-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:=
-
-endif # HDRCK.HAS_GIT
-
-else # HEADER_SAVE_SPEC
-
-# From a file
-HDRCK.SPEC:= cat $(HEADER_SPEC)
-
-# The file format can be overloaded in using the var HDRCK_EXTRA
-HDRCK.OPTS+= -spec-format 3-zeros
-
-endif # HEADER_SAVE_SPEC
-endif # HEADER_SPEC
-
-################################
+##########################################################################
## Updates HDRCK.OPTS variable
ifneq ($(HEADER_DISTRIB_FILE),)
@@ -172,9 +102,8 @@ ifeq ($(HEADER_STRICT),yes)
HDRCK.OPTS+= -exit-on-warning
endif
-#####################################
-## Identifies where are the headers
-## and updates HDRCK.OPTS variable
+##########################################################################
+## Identifies where are the headers and updates HDRCK.OPTS variable
ifeq ($(HEADER_OPEN_SOURCE),yes)
HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /open-source,$(HEADER_DIRS)))
@@ -190,134 +119,61 @@ endif
endif
endif
-#################################
-
-ifeq ($(HDRCK.SPEC),)
-
-.PHONY: check-headers
-check-headers: $(FRAMAC_HDRCK)
- $(error "Please set HEADER_SPEC variable to a file containing the header specification.")
+##########################################################################
+## HDRCK
+HDRCK.HAS_GIT:=$(shell git rev-parse --is-inside-work-tree 2> /dev/null)
+HDRCK.ENABLED=yes
+ifneq ($(HDRCK.HAS_GIT),true)
+ifeq ($(HDRCK_FILES_INPUT),)
+HDRCK.ENABLED=no
+endif
+endif
-.PHONY: headers
-headers: $(FRAMAC_HDRCK)
- $(error "Please set HEADER_SPEC variable to a file containing the header specification.")
+ifeq ($(HDRCK_FILES_INPUT),)
+HDRCK.COLLECT=$(GIT) ls-files -z | $(GIT) check-attr --stdin -z header_spec
else
+HDRCK.COLLECT=cat $(HDRCK_FILES_INPUT)
+endif
-ifneq ($(HDRCK.HAS_GIT),)
-
-define HDRCK.file-list-from-git-diff-info
-$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) -e "s/^[CR][0-9]\+[ \t]\+[^ \t]\+[ \t]\+//" -e "s/^[AM][ \t]*//"
-endef
-
-define HDRCK.file-list-from-git-diff
- $(call HDRCK.file-list-from-git-diff-info,$(1)) | $(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:
- $$(call HDRCK.file-list-from-git-diff-info,$(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 rev-parse --abbrev-ref HEAD) 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 rev-parse --abbrev-ref HEAD),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))
+ifeq ($(HDRCK.ENABLED),yes)
-#### rules for make <headers-target>.previous-commit
-## looks at files of the last commit and checks that there is no staged nor unstaged files
+.PHONY: check-headers
+check-headers:
+ $(HDRCK.COLLECT) | $(HDRCK.CMD) $(HDRCK.OPTS) $(HDRCK_EXTRA)
-$(eval $(call HDRCK.file-list-filter-with-git-diff,previous-commit,HEAD~1,HDRCK.checked-unmodified-ok))
+.PHONY: headers
+headers:
+ $(HDRCK.COLLECT) | $(HDRCK.CMD) -update $(HDRCK.OPTS) $(HDRCK_EXTRA)
-endif # $(HDRCK.HAS_GIT)
+else
.PHONY: check-headers
-check-headers: $(FRAMAC_HDRCK)
- $(HDRCK.SPEC) | $(HDRCK.CMD) $(HDRCK.OPTS) $(HDRCK_EXTRA)
+check-headers:
+ $(error "Cannot check-headers: not a Git repository, \
+ you should specify HDRCK_FILES_INPUT")
.PHONY: headers
-headers: $(FRAMAC_HDRCK)
- $(HDRCK.SPEC) | $(HDRCK.CMD) -update $(HDRCK.OPTS) $(HDRCK_EXTRA)
+headers:
+ $(error "Cannot make headers: not a Git repository, \
+ you should specify HDRCK_FILES_INPUT")
-endif # $(HDRCK.SPEC)
+endif
#################################
.PHONY: headers.info
headers.info:
- echo "FRAMAC_HDRCK='$(FRAMAC_HDRCK)'"
echo "HEADER_OPEN_SOURCE='$(HEADER_OPEN_SOURCE)'"
echo "HEADER_STRICT='$(HEADER_STRICT)'"
echo "HEADER_DIRS='$(HEADER_STRICT)'"
- echo "HEADER_DISTRIB_FILE='$(HEADER_DISTRIB_FILE)'"
echo "HEADER_EXCEPTIONS='$(HEADER_EXCEPTIONS)'"
echo "HEADER_REPO='$(HEADER_REPO)'"
- echo "HEADER_SPEC='$(HEADER_SPEC)'"
+ echo "HDRCK_FILES_INPUT='$(HDRCK_FILES_INPUT)'"
echo "HDRCK.HAS_GIT='$(HDRCK.HAS_GIT)'"
echo "HDRCK.CMD='$(HDRCK.CMD)'"
- echo "HDRCK.SPEC='$(HDRCK.SPEC)'"
echo "HDRCK.OPTS='$(HDRCK.OPTS)'"
-
###############################################################################
# Local Variables:
# compile-command: "make"
diff --git a/share/Makefile.linting b/share/Makefile.linting
index 7b64a553d86b2040061ef647d4e27c4f61184df0..caf1c36f0dfb1f26a98c7e106231251652d35b66 100644
--- a/share/Makefile.linting
+++ b/share/Makefile.linting
@@ -20,555 +20,88 @@
# #
##########################################################################
+##########################################################################
+# Parameters
-################################
-# Code prettyfication and lint #
-################################
-
-# make lint includes:
-# - make check-utf8: valid UTF-8 encoding
-# - make check-eoleof: EOF preceded by an EOL
-# - make check-syntax: EOF preceded by an EOL + no TAB + no BLANK at the end
-# - make check-indent: valid indentation
-#
-# For all these targets (and the corresponding fix-XXX), it is possible to restrict the search to a sub-directory:
-# - make LINT_DIR=<subdir> <lint-target>
-# It is possible to force the action to given files:
-# - make LINT_FILE=<file> <lint-target>
-# or to the files modified between HEAD and a specific branch/commit:
-# - make LINT_DIFF=<branch/commit> <lint-target>
-#
-# Notes:
-# - when LINT_FILE is given, .gitattributes, LINT_DIFF and LINT_DIR are ignored;
-# - when LINT_DIFF is given, LINT_DIR is ignored (but .gitattributes is used);
-# - to use fix-utf8 target, the variable LINT_FROM_ENCODING=<from-encoding-name>
-# has to be set.
-#
-# Advanced targets when LINT_FILE is undefined
-# - make <lint-target>.unstaged
-# looks at unstaged files
-# - make <lint-target>.before-commit-a
-# looks at unstaged and staged files
-# - make <lint-target>.before-commit-a--ammend
-# looks at unstaged, staged and previously committed files
-# - make <lint-target>.before-commit--ammend
-# looks at staged and previously committed files and checks that there is no unstaged files
-# - make <lint-target>.before-commit
-# looks at staged files and checks that there is no unstaged files
-# - make <lint-target>.previous-commit
-# looks at files of the last commit and checks that there is no staged nor unstaged files
-# - make <lint-target>.before-push:
-# looks at files modified from origin/$(git rev-parse --abbrev-ref HEAD) and checks that there is no staged nor unstaged files
+# Must be unset (for external plugins) and set (for FRAMA-C kernel)
+IN_FRAMAC?=
-# make clean-lint (removing linting targets) includes
-# - make clean-utf8
-# - make clean-eoleof
-# - make clean-syntax
-# - make clean-indent
+# Note: DO NOT rename this variable "LINT", this name is defined in GNU Makefile
+LINTCK?=frama-c-lint
-# make clean-lint (removing linting targets) includes
-# - make clean-utf8
-# - make clean-eoleof
-# - make clean-syntax
-# - make clean-indent
+# Can be set to a
+# - <file> containing files to check/update and their attributes, with 0
+# separators (like 'git ls-files -z | git check-attr --stdin -za').
+LINTCK_FILES_INPUT?=
-################################
-## Default variables
+# Extra parameters for the lint command
+LINTCK_EXTRA?=
-IS_UTF8 ?= iconv -f UTF-8 -t UTF-8
-TO_UTF8 ?= iconv -t UTF-8 -f
+##########################################################################
+## Tools
-OCP_INDENT ?= ocp-indent
-CLANG_FORMAT ?= clang-format
-# wc, tail, head, cmp
+GIT ?= git
+DUNE ?= dune
-# Default values necessary for
-# LINT_MAKEFILE=<this-makefile> make -f <this-makefile> <lint-target>`
-# Otherwise theses variables are defined into share/Makefile.common
-GREP ?= grep
-TR ?= tr
-SED ?= LC_ALL=C sed
-ISED ?= sed -i
-FIND ?= find
-GIT ?= git
-MKDIR ?= mkdir -p
-MV ?= mv
-RM ?= rm -f
-RMDIR ?= rm -rf
-TOUCH ?= touch
-WC ?= wc
+##########################################################################
+## Command used to execute lint
-ifeq ($(PLATFORM),Darwin)
-XARGS ?= xargs
+ifneq ($(IN_FRAMAC),yes)
+LINTCK.CMD:= $(LINTCK)
else
-# Unix, Cygwin
-XARGS ?= xargs --no-run-if-empty
+LINTCK.CMD:= $(DUNE) exec --no-print-directory --root $(FRAMAC_LINTCK_SRC) -- $(LINTCK)
endif
-############
-
-# Can be set to the path of that makefile
-LINT_MAKEFILE ?=
-
-# Can be set to a sub-directory to restrict the checking
-LINT_DIR ?= .
-
-################################
-
-LINT.makefile=$(wildcard $(LINT_MAKEFILE))
-ifeq ($(LINT.makefile),)
-
-LINT.make?=$(MAKE) --quiet
-else
+##########################################################################
+## LINT
-LINT.make?=$(MAKE) --quiet -f $(LINT.makefile)
+LINTCK.HAS_GIT:=$(shell git rev-parse --is-inside-work-tree 2> /dev/null)
+LINTCK.ENABLED=yes
+ifneq ($(LINTCK.HAS_GIT),true)
+ifeq ($(LINTCK_FILES_INPUT),)
+LINTCK.ENABLED=no
endif
-
-################################
-## CHECK ocp-indent VERSION
-
-.lint/check-ocp-indent-version:
- if command -v $(OCP_INDENT) >/dev/null; then \
- if [ -z "$(shell $(OCP_INDENT) --version)" ]; then echo "warning: $(OCP_INDENT) returned an empty string, assuming it is the correct version"; \
- else \
- $(eval ocp_version_major := $(shell $(OCP_INDENT) --version | $(SED) -E "s/^([0-9]+)\.[0-9]+\..*/\1/")) \
- $(eval ocp_version_minor := $(shell $(OCP_INDENT) --version | $(SED) -E "s/^[0-9]+\.([0-9]+)\..*/\1/")) \
- if [ "$(ocp_version_major)" -lt 1 -o "$(ocp_version_minor)" -lt 7 ]; then \
- echo "error: $(OCP_INDENT) 1.7.0 required for linting (got $(ocp_version_major).$(ocp_version_minor))"; \
- exit 1; \
- fi; \
- fi; \
- else \
- exit 1; \
- fi;
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
-
-.lint/check-clang-format-installed:
- if ! command -v $(CLANG_FORMAT) >/dev/null; then \
- echo "error: $(CLANG_FORMAT) must be installed"; \
- exit 1; \
- fi;
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
-
-###############
-## Main target
-
-LINT.check-targets= \
- check-syntax check-indent check-eoleof check-utf8
-
-LINT.fix-targets=$(subst check-,fix-,$(LINT.check-targets))
-LINT.main-targets=lint $(LINT.check-targets) $(LINT.fix-targets)
-
-LINT.HAS_GIT:=$(shell git rev-parse --is-inside-work-tree 2> /dev/null)
-ifneq ($(LINT.HAS_GIT),true)
-
-.PHONY: lint
-lint:
- echo "'make lint' requires a git repository but, that is not"
- echo "the case for example with 'make LINT_FILE=<file> check-syntax'"
- git rev-parse --is-inside-work-tree
-
-else
-
-.PHONY: lint
-lint: $(LINT.check-targets)
-
endif
-###############################
-## Cleaning
-
-# Targets are generated into .lint/ directories
-
-.PHONY: clean-lint
-clean-lint:
- echo "Cleaning LINT targets..."
- $(RMDIR) .lint
-
-clean:: clean-lint
-
-#### clean-check-XXX targets
-
-LINT.clean-targets=$(addprefix clean-,$(LINT.check-targets))
-
-.PHONY: $(LINT.clean-targets)
-# Generic rule
-$(LINT.clean-targets):
- echo "[LINT] Cleaning $(patsubst clean-%,%,$@) targets..."
- $(FIND) .lint -type f -name \*.$(patsubst clean-%,%,$@) | $(XARGS) -n 10 $(RM)
-
-###############################
-
-ifeq ($(LINT_FILE),) ############# No lint file given
-
-######## LINT_DIR filter
-LINT.dir=$(wildcard $(LINT_DIR))
-
-ifeq ($(LINT.HAS_GIT),true) ############# For Git repository
-
-######## LINT_DIFF filter
-
-define LINT.file-list-from-git-diff-info
-$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) -e "s/^[CR][0-9]\+[ \t]\+[^ \t]\+[ \t]\+//" -e "s/^[AM][ \t]*//"
-endef
-
-define LINT.file-list-from-git-diff
-$(call LINT.file-list-from-git-diff-info,$(1)) | $(TR) '\n' '\000'
-endef
-
-define LINT.file-list-filter-with-git-diff
-LINT.$(1)-filter-targets=$$(addsuffix .$(1),$$(LINT.main-targets))
-.PHONY: $(LINT.$(1)-filter-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] checked file list:
- $$(call LINT.file-list-from-git-diff-info,$(2))
-endef
-
-ifeq ($(LINT_DIFF),)
-LINT.FILE_LIST=$(GIT) ls-files $(LINT.dir) -z
+ifeq ($(LINTCK_FILES_INPUT),)
+LINTCK.COLLECT=$(GIT) ls-files -z | $(GIT) check-attr --stdin -z -a
else
-$(info [LINT] Looking at files modified from branch/commit: '$(LINT_DIFF)')
-LINT.FILE_LIST=$(call LINT.file-list-from-git-diff,$(LINT_DIFF))
-$(info $(LINT.FILE_LIST))
-endif
-
-#### rules for make <lint-target>.before-push
-## looks at files modified from origin/$(git rev-parse --abbrev-ref HEAD) and checks that there is no staged nor unstaged files
-
-PHONY: LINT.checked-unmodified-ok
-LINT.checked-unmodified-ok:
- $(eval LINT.checked-unmodified := $(shell $(GIT) diff --name-status HEAD | $(WC) -l))
- if [ 0 != $(LINT.checked-unmodified) ]; then \
- echo "[LINT] Staged or unstaged files=$(LINT.checked-unmodified):"; \
- $(GIT) diff --name-status HEAD; \
- echo "[LINT] Error: may check some staged or unstaged file versions" ; \
- exit 1; \
- fi;
-
-$(eval $(call LINT.file-list-filter-with-git-diff,before-push,--cached origin/$(shell git rev-parse --abbrev-ref HEAD),LINT.checked-unmodified-ok))
-
-#### rules for make <lint-target>.unstaged
-## looks at unstaged files
-
-$(eval $(call LINT.file-list-filter-with-git-diff,unstaged, ))
-
-#### rules for make <lint-target>.before-commit
-## looks at staged files and checks that there is no unstaged files
-
-PHONY: LINT.checked-unstaged-ok
-LINT.checked-unstaged-ok:
- $(eval LINT.checked-unstaged := $(shell $(GIT) diff --name-status | $(WC) -l))
- if [ 0 != $(LINT.checked-unstaged) ]; then \
- echo "[LINT] Unstaged files=$(LINT.checked-unstaged):"; \
- $(GIT) diff --name-status ; \
- echo "[LINT] Error: may check some unstaged version files version." ; \
- exit 1; \
- fi;
-
-$(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
-
-$(eval $(call LINT.file-list-filter-with-git-diff,before-commit-a,HEAD,))
-
-#### rules for make <lint-target>.before-commit-a--ammend
-## looks at unstaged, staged and previously committed files
-
-$(eval $(call LINT.file-list-filter-with-git-diff,before-commit-a--ammend,HEAD~1,))
-
-#### rules for make <lint-target>.before-commit--amend
-## looks at staged and previously committed files and checks that there is no unstaged files
-
-$(eval $(call LINT.file-list-filter-with-git-diff,before-commit--ammend,HEAD~1,LINT.checked-unstaged-ok))
-
-#### rules for make <lint-target>.previous-commit
-## looks at files of the last commit and checks that there is no staged nor unstaged files
-
-$(eval $(call LINT.file-list-filter-with-git-diff,previous-commit,HEAD~1,LINT.checked-unmodified-ok))
-
-#### get attr / filter set attr
-
-LINT.GET_ATTR=$(GIT) check-attr --stdin -z
-LINT.FILTER_FILE_ATTR=$(SED) -zne 'x;n;n;s/^set$$//;t print;b;:print;x;p'
-
-#### check-XXX targets
-
-.PHONY: $(LINT.check-targets)
-# Generic rule
-$(LINT.check-targets):
- echo "[LINT] Checking from GIT attribute $@..."
- $(LINT.FILE_LIST) \
- | $(LINT.GET_ATTR) $@ \
- | $(LINT.FILTER_FILE_ATTR) \
- | $(XARGS) -0 -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
-
-#### fix-XXX targets
-
-# Generic rule
-$(LINT.fix-targets):
- echo "[LINT] Fixing from GIT attribute $(patsubst fix-%,check-%,$@)..."
- $(LINT.FILE_LIST) \
- | $(LINT.GET_ATTR) $(patsubst fix-%,check-%,$@) \
- | $(LINT.FILTER_FILE_ATTR) \
- | $(XARGS) -0 -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
-
-endif ############ For Git repository
-
-else ############# LINT_FILE are given
-
-## Internal targets from the recursive make
-
-LINT_FILE.list=$(addprefix .lint/,$(wildcard $(LINT_FILE)))
-
-LINT_FILE.check-utf8= $(addsuffix .check-utf8,$(LINT_FILE.list))
-LINT_FILE.check-eoleof= $(addsuffix .check-eoleof,$(LINT_FILE.list))
-LINT_FILE.check-syntax= $(addsuffix .check-syntax,$(LINT_FILE.list))
-LINT_FILE.check-indent= $(addsuffix .check-indent,$(LINT_FILE.list))
-
-LINT_FILE.fix-utf8= $(addsuffix .fix-utf8,$(LINT_FILE.list))
-LINT_FILE.fix-eoleof= $(addsuffix .fix-eoleof,$(LINT_FILE.list))
-LINT_FILE.fix-syntax= $(addsuffix .fix-syntax,$(LINT_FILE.list))
-LINT_FILE.fix-indent= $(addsuffix .fix-indent,$(LINT_FILE.list))
-
-## Filters for the extension for check/fix-indent
-
-# ML filter
-LINT_FILE.ml-indent = $(filter $(addsuffix .ml,$(basename $(LINT_FILE.list))),$(LINT_FILE.list))
-LINT_FILE.ml-indent+= $(filter $(addsuffix .mli,$(basename $(LINT_FILE.list))),$(LINT_FILE.list))
-LINT_FILE.check-ml-indent= $(addsuffix .check-indent,$(LINT_FILE.ml-indent))
-LINT_FILE.fix-ml-indent= $(addsuffix .fix-indent,$(LINT_FILE.ml-indent))
-
-# C filter
-LINT_FILE.c-indent =$(filter $(addsuffix .c,$(basename $(LINT_FILE.list))),$(LINT_FILE.list))
-LINT_FILE.c-indent+= $(filter $(addsuffix .h,$(basename $(LINT_FILE.list))),$(LINT_FILE.list))
-LINT_FILE.check-c-indent= $(addsuffix .check-indent,$(LINT_FILE.c-indent))
-LINT_FILE.fix-c-indent= $(addsuffix .fix-indent,$(LINT_FILE.c-indent))
-
-
-LINT_FILE.check-unknown-indent=$(filter-out $(LINT_FILE.check-ml-indent) \
- $(LINT_FILE.check-c-indent),$(LINT_FILE.check-indent))
-LINT_FILE.fix-unknown-indent=$(patsusbt %.check-indent,%.fix-indent,LINT_FILE.check-unknown-indent)
-
-## check-XXX targets
-
-.PHONY: check-utf8
-check-utf8: $(LINT_FILE.check-utf8)
-
-.PHONY: check-eoleof
-check-eoleof: $(LINT_FILE.check-eoleof)
-
-.PHONY: check-syntax
-check-syntax: $(LINT_FILE.check-syntax)
-
-# ML and C format
-.PHONY: check-indent
-check-indent: $(LINT_FILE.check-indent)
-
-## fix-XXX targets
-
-.PHONY: fix-utf8
-fix-utf8: $(LINT_FILE.fix-utf8)
-
-.PHONY: fix-eoleof
-fix-eoleof: $(LINT_FILE.fix-eoleof)
-
-.PHONY: fix-syntax
-fix-syntax: $(LINT_FILE.fix-syntax)
-
-# ML and C format
-.PHONY: fix-indent
-fix-indent: $(LINT_FILE.fix-indent)
-
+LINTCK.COLLECT=cat $(LINTCK_FILES_INPUT)
endif
-###############################
-## UTF8 ASPECT
-
-$(LINT_FILE.check-utf8): .lint/%.check-utf8: %
- echo "Check UTF8: $<"
- if ! $(IS_UTF8) $< > /dev/null; \
- then \
- echo "File $< uses an invalid UTF-8 encoding."; \
- echo "Please fixe it manualy or in running: make LINT_FROM_ENCODING=<ENCODING-NAME> LINT_FILE=$< fix-utf8";\
- echo "The next command may help you to find that <ENCODING-NAME>: file $<";\
- exit 1; \
- fi
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
+ifeq ($(LINTCK.ENABLED),yes)
-ifneq ($(LINT_FROM_ENCODING),)
+.PHONY: check-lint
+check-lint:
+ $(LINTCK.COLLECT) | $(LINTCK.CMD) $(LINTCK_EXTRA)
-.PHONY: $(LINT_FILE.fix-utf8)
-$(LINT_FILE.fix-utf8): .lint/%.fix-utf8: %
- if ! $(IS_UTF8) $< > /dev/null 2> /dev/null; \
- then \
- echo "Fixes UTF8 (from $(LINT_FROM_ENCODING)): $<"; \
- if ! $(TO_UTF8) $(LINT_FROM_ENCODING) $< > $<.tmp; then exit 1; fi; \
- $(MV) $<.tmp $<; \
- fi
- $(MKDIR) $(dir $@)
- $(TOUCH) .lint/$<.check-utf8 # no more need of check-indent
+.PHONY: lint
+lint:
+ $(LINTCK.COLLECT) | $(LINTCK.CMD) -u $(LINTCK_EXTRA)
else
-$(LINT_FILE.fix-utf8): .lint/%.fix-utf8: % .lint/check-ocp-indent-version
- $(error "Target fix-utf8 requires to define LINT_FROM_ENCODING variable")
-
-endif # LINT_FROM_ENCODING
+.PHONY: check-lint
+check-lint:
+ $(error "Cannot lint: not a Git repository, \
+ you should specify LINTCK_FILES_INPUT")
-###############################
-## UNKNOWN INDENTATION FORMATER
-
-ifneq ($(LINT_FILE.check-unknown-indent),)
-.PHONY: $(LINT_FILE.check-unknown-indent)
-$(LINT_FILE.check-unknown-indent): .lint/%.check-indent: %
- $(error "Check indent with an unknown formater: $<")
-endif
+.PHONY: lint
+lint:
+ $(error "Cannot fix-lint: not a Git repository, \
+ you should specify LINTCK_FILES_INPUT")
-ifneq ($(LINT_FILE.fix-unknown-indent),)
-.PHONY: $(LINT_FILE.fix-unknown-indent)
-$(LINT_FILE.check-unknown-indent): .lint/%.fix-indent: %
- $(error "Check indent with an unknown formater: $<")
endif
-###############################
-## ML INDENTATION ASPECT
-
-$(LINT_FILE.check-ml-indent): .lint/%.check-indent: % .lint/check-ocp-indent-version
- echo "Check ML indent: $<"
- $(OCP_INDENT) $< > $<.tmp
- if cmp -s $< $<.tmp; \
- then $(RM) $<.tmp; \
- else \
- echo "File $< is not indented correctly."; \
- echo "Please run: make LINT_FILE=$< fix-indent";\
- $(RM) $<.tmp; \
- exit 1; \
- fi
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
-
-.PHONY: $(LINT_FILE.fix-ml-indent)
-$(LINT_FILE.fix-ml-indent): .lint/%.fix-indent: % .lint/check-ocp-indent-version
- echo "Fixes ML indent: $<"
- $(OCP_INDENT) -i $<
- $(MKDIR) $(dir $@)
- $(TOUCH) .lint/$<.check-indent # no more need of check-indent
-
-###############################
-## C INDENTATION ASPECT
-
-$(LINT_FILE.check-c-indent): .lint/%.check-indent: % .lint/check-clang-format-installed
- echo "Check C indent: $<"
- $(CLANG_FORMAT) --dry-run -Werror $<
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
-
-.PHONY: $(LINT_FILE.fix-c-indent)
-$(LINT_FILE.fix-c-indent): .lint/%.fix-indent: % .lint/check-clang-format-installed
- echo "Fixes C indent: $<"
- $(CLANG_FORMAT) -i $<
- $(MKDIR) $(dir $@)
- $(TOUCH) .lint/$<.check-indent # no more need of check-indent
-
-###############################
-## EOL EOF ASPECT (included by check-syntax target)
-
-$(LINT_FILE.check-eoleof): .lint/%.check-eoleof: %
- # See SO 1825552 on mixing grep and \t (and cry)
- # For OK_NL, we have three cases:
- # - for empty files, the computation boils down to 0 - 0 == 0
- # - for non-empty files with a proper \n at the end, to 1 - 1 == 0
- # - for empty files without \n, to 1 - 0 == 1 that will be catched
- echo "Check EOL EOF: $<"
- OK_NL=$$(($$(tail -c -1 $< | wc -c) - $$(tail -n -1 $< | wc -l))) ; \
- if test $$OK_NL -gt 0; then \
- echo "File $< does not pass syntactic checks:"; \
- echo "No newline at end of file"; \
- echo "Please run: make LINT_FILE=$< fix-eoleof"; \
- exit 1 ; \
- fi
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
-
-# The real target is a check-XXX one
-.PHONY: $(LINT_FILE.fix-eoleof)
-$(LINT_FILE.fix-eoleof): .lint/%.fix-eoleof: %
- echo "Fixes EOL EOF: $<"
- $(ISED) -e '$$a\' $<
- $(MKDIR) $(dir $@)
- $(TOUCH) .lint/$<.check-eoleof # no more need of this checking
-
-%.fix-eoleof: LC_ALL = C
-
-###############################
-## SYNTACTICAL ASPECT
-
-$(LINT_FILE.check-syntax): .lint/%.check-syntax: %
- # See SO 1825552 on mixing grep and \t (and cry)
- # For OK_NL, we have three cases:
- # - for empty files, the computation boils down to 0 - 0 == 0
- # - for non-empty files with a proper \n at the end, to 1 - 1 == 0
- # - for empty files without \n, to 1 - 0 == 1 that will be catched
- echo "Check syntax: $<"
- OK_TAB=$$(grep -c -e "$$(printf '^ *\t')" $<) ; \
- OK_SPACE=$$(grep -c -e '[[:blank:]]$$' $<) ; \
- OK_NL=$$(($$(tail -c -1 $< | wc -c) - $$(tail -n -1 $< | wc -l))) ; \
- OK_EMPTY=$$(tail -n -1 $< | grep -c -e '^[[:blank:]]*$$') ; \
- ERROR=$$(($$OK_TAB + $$OK_SPACE + $$OK_NL + $$OK_EMPTY)) ; \
- if test $$ERROR -gt 0; then \
- echo "File $< does not pass syntactic checks:"; \
- echo "$$OK_TAB lines indented with tabulation instead of spaces"; \
- echo "$$OK_SPACE lines with spaces at end of line"; \
- test $$OK_NL -eq 0 || echo "No newline at end of file"; \
- test $$OK_EMPTY -eq 0 || echo "Empty line(s) at end of file"; \
- echo "Please run: make LINT_FILE=$< fix-syntax"; \
- exit 1 ; \
- fi
- $(MKDIR) $(dir $@)
- $(TOUCH) $@
-
-# The real target is a check-XXX one
-.PHONY: $(LINT_FILE.fix-syntax)
-$(LINT_FILE.fix-syntax): .lint/%.fix-syntax: %
- echo "Fixes syntax: $<"
- $(ISED) -e 's/^ *\t\+/ /' $<
- $(ISED) -e 's/\(.*[^[:blank:]]\)[[:blank:]]\+$$/\1/' $<
- $(ISED) -e 's/^[ \t]\+$$//' $<
- if test \( $$(tail -n -1 $< | wc -l) -eq 0 \) -a \( $$(wc -c $< | cut -d " " -f 1) -gt 0 \) ; then \
- echo "" >> $<; \
- else \
- while tail -n -1 $< | grep -l -e '^[ \t]*$$'; do \
- head -n -1 $< > $<.tmp; \
- $(MV) $<.tmp $<; \
- done; \
- fi
- $(MKDIR) $(dir $@)
- $(TOUCH) .lint/$<.check-syntax # no more need of check-syntax
-
-# Avoid a UTF-8 locale at all cost: in such setting, sed does not work
-# reliably if you happen to have latin-1 encoding somewhere,
-# which is still unfortunately the case in some dark corners of the platform
-%.fix-syntax: LC_ALL = C
-
-###############################
-## Info
+##########################################################################
+.PHONY: lint.info
lint.info:
- echo "LINT.HAS_GIT='$(LINT.HAS_GIT)'"
- echo "LINT.make='$(LINT.make)'"
- echo "LINT_FILE.list='$(LINT_FILE.list)'"
- echo "LINT_FILE.check-syntax='$(LINT_FILE.check-syntax)'"
- echo "LINT_FILE.check-indent='$(LINT_FILE.check-indent)'"
- echo "LINT_FILE.fix-syntax='$(LINT_FILE.fix-syntax)'"
- echo "LINT_FILE.fix-indent='$(LINT_FILE.fix-indent)'"
+ echo "LINTCK_FILES_INPUT='$(LINTCK_FILES_INPUT)'"
+ echo "LINTCK.HAS_GIT='$(LINTCK.HAS_GIT)'"
+ echo "LINTCK.CMD='$(LINTCK.CMD)'"
-###############################################################################
+##########################################################################
# Local Variables:
# compile-command: "make"
# End:
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 46c82aeca51a4f89ebbc231346f44927c49b4da1..26eba1a5c8a2c268a1dde6583886f0e9582e12e7 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -1142,43 +1142,43 @@ module Consolidation = struct
consolidate_of_local_when_cycle ppt
(* [JS 2011/11/04] use the following code (to be tested) as soon as WP uses the
new function [legal_dependency_cycle] *)
- (* match e with
- | Not_yet -> assert false
- | Single e ->
- if Valid_cycles.mem e path then
- consolidate_of_local_when_cycle ppt
- else
- Kernel.fatal
- "illegal dependency cycle for emitter %a"
- Usable_emitter.pretty e
- | Several ->
- (* cycle because the proof of [ppt] with emitter [E1] depends
- on another [ppt'] which is proven with another emitter [E2]
- by using [ppt] itself: it is not inconsistent by itself, but we
- cannot use it as a proof. *)
- consolidate ppt
- (fun _ ->
- Unknown
- (Usable_emitter.Map.add
- usable_kernel_emitter
- (Usable_emitter.Map.add
- usable_kernel_emitter
- (List.fold_left
- (fun acc p -> Property.Set.add p acc)
- Property.Set.empty
- path)
- Usable_emitter.Map.empty)
- Usable_emitter.Map.empty))*)
+ (* match e with
+ | Not_yet -> assert false
+ | Single e ->
+ if Valid_cycles.mem e path then
+ consolidate_of_local_when_cycle ppt
+ else
+ Kernel.fatal
+ "illegal dependency cycle for emitter %a"
+ Usable_emitter.pretty e
+ | Several ->
+ (* cycle because the proof of [ppt] with emitter [E1] depends
+ on another [ppt'] which is proven with another emitter [E2]
+ by using [ppt] itself: it is not inconsistent by itself, but we
+ cannot use it as a proof. *)
+ consolidate ppt
+ (fun _ ->
+ Unknown
+ (Usable_emitter.Map.add
+ usable_kernel_emitter
+ (Usable_emitter.Map.add
+ usable_kernel_emitter
+ (List.fold_left
+ (fun acc p -> Property.Set.add p acc)
+ Property.Set.empty
+ path)
+ Usable_emitter.Map.empty)
+ Usable_emitter.Map.empty))*)
end else begin
Property.Hashtbl.add visited_ppt ppt ();
consolidate ppt (consolidated_emitters ppt e (ppt :: path))
(* [JS 2011/11/04] think about that when uncommenting the code above *)
- (* try
- (* was previously added during its own calculus
- in case of inconsistent mutual dependency *)
- Consolidated_status.find ppt
- with Not_found ->*)
- (* consolidated_status*)
+ (* try
+ (* was previously added during its own calculus
+ in case of inconsistent mutual dependency *)
+ Consolidated_status.find ppt
+ with Not_found ->*)
+ (* consolidated_status*)
end)
ppt
@@ -1432,15 +1432,15 @@ module Consolidation_graph = struct
(distinct_tuning_parameters emitter)
g
in
- (* let g =
- (* adding the correctness parameters *)
- Datatype.String.Set.fold
- (fun p g ->
- let s = get_parameter_string ~tuning:false emitter p in
- G.add_edge g v_e (Correctness_parameter s); g)
- (distinct_correctness_parameters emitter)
- g
- in*)
+ (* let g =
+ (* adding the correctness parameters *)
+ Datatype.String.Set.fold
+ (fun p g ->
+ let s = get_parameter_string ~tuning:false emitter p in
+ G.add_edge g v_e (Correctness_parameter s); g)
+ (distinct_correctness_parameters emitter)
+ g
+ in*)
(* adding the hypotheses *)
let g, truncated =
List.fold_left
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index df68d08f1229c4946c3e9aa197e3e30028c4ce9b..c727f7c578c8468876beca8ae4492ef585e01a2e 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5289,7 +5289,7 @@ let rec constFoldTermNodeAtTop = function
end
| TSizeOfE { term_type= Ctype typ } -> constFoldTermNodeAtTop (TSizeOf typ)
| TAlignOfE { term_type= Ctype typ }
- -> constFoldTermNodeAtTop (TAlignOf typ)
+ -> constFoldTermNodeAtTop (TAlignOf typ)
| TSizeOfE _ | TAlignOfE _ ->
assert false (* sizeof/alignof of logic types are rejected
by typing anyway. *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 05129394522bc88c3537442082d1ca52890276dc..005bc7a063469332ff0ab80f24dbf8ad3778d501 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1752,14 +1752,14 @@ class type cilVisitor = object
method vfrees:
identified_term list -> identified_term list visitAction
- (** @since Oxygen-20120901 *)
+ (** @since Oxygen-20120901 *)
method vallocates:
identified_term list -> identified_term list visitAction
- (** @since Oxygen-20120901 *)
+ (** @since Oxygen-20120901 *)
method vallocation: allocation -> allocation visitAction
- (** @since Oxygen-20120901 *)
+ (** @since Oxygen-20120901 *)
method vloop_pragma: loop_pragma -> loop_pragma visitAction
method vslice_pragma: slice_pragma -> slice_pragma visitAction
@@ -1950,18 +1950,15 @@ val visitCilFrom: cilVisitor -> from -> from
val visitCilAssigns: cilVisitor -> assigns -> assigns
-(** @since Oxygen-20120901
-*)
+(** @since Oxygen-20120901 *)
val visitCilFrees:
cilVisitor -> identified_term list -> identified_term list
-(** @since Oxygen-20120901
-*)
+(** @since Oxygen-20120901 *)
val visitCilAllocates:
cilVisitor -> identified_term list -> identified_term list
-(** @since Oxygen-20120901
-*)
+(** @since Oxygen-20120901 *)
val visitCilAllocation: cilVisitor -> allocation -> allocation
val visitCilFunspec: cilVisitor -> funspec -> funspec
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 9de89b3bbd52faf2f891fa3e459652c61145fa1e..d91eced84818a70794632819757dfae6d9a80ee9 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -600,7 +600,7 @@ let type_of_array_elem =
let rec ctype_of_array_elem t =
match unroll_type t with
- | Ctype ty when isArrayType ty -> Cil.typeOf_array_elem ty
+ | Ctype ty when isArrayType ty -> Cil.typeOf_array_elem ty
| Ltype ({lt_name = "set"},[t]) -> ctype_of_array_elem t
| _ ->
Kernel.fatal ~current:true "type %a is not a pointer type"
@@ -2726,7 +2726,7 @@ struct
let ty1 = t1.term_type in
let t2 = term env t2 in
let ty2 = t2.term_type in
- let binop op tr = TBinOp (op, mk_cast t1 tr, mk_cast t2 tr),
+ let binop op tr = TBinOp (op, mk_cast t1 tr, mk_cast t2 tr),
logic_arithmetic_promotion tr
in
begin match op with
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 15622103b2b1eb7dffe642f3b5f38e8bae4f9c60..b1fff81fcd0702622895d473cd5717a959edf906 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -999,7 +999,7 @@ struct
| Branch(p, m, s0, s1, _) ->
try
let result = Hashtbl.find table t in
- (* Format.printf "find %s %d@." name !counter; *)
+ (* Format.printf "find %s %d@." name !counter; *)
result
with Not_found ->
let result0 = traverse s0 in
@@ -1008,11 +1008,11 @@ struct
incr counter;
if !counter >= cache
then begin
- (* Format.printf "Clearing %s fold table@." name;*)
+ (* Format.printf "Clearing %s fold table@." name;*)
Hashtbl.clear table;
counter := 0;
end;
- (* Format.printf "add %s %d@." name !counter; *)
+ (* Format.printf "add %s %d@." name !counter; *)
Hashtbl.add table t result;
result
in
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 9e5dd8f5f57cc7ae8befa78281fae1ec6a13849a..57d0faa6e0ce920640004927792c79e94747facd 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -1086,7 +1086,7 @@ void print_heap_shadows(uintptr_t addr) {
DLOG(" | === Block Shadow ======================================\n");
DLOG(" | Access addr: %a\n", addr);
DLOG(" | Block Shadow: %a\n", block_shadow);
- DLOG(" | Init Shadow: %a\n", init_shadow);
+ DLOG(" | Init Shadow: %a\n", init_shadow);
DLOG(" | Segments: %lu\n", segments);
DLOG(" | Actual size: %lu bytes\n", alloc_size);
DLOG(" | Tracked Length: %lu bytes\n", length);
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 1b0830126927676e793b79ea589dc27bde37cdb4..d6fec703a3d1f0e02084364627157e058fbd3c66 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -364,7 +364,7 @@ module rec Transfer
| Pvalid(_, t) | Pvalid_read(_, t)
| Pobject_pointer(_, t) | Pvalid_function t
| Pinitialized(_, t) | Pfreeable(_, t) ->
- (* Options.feedback "REGISTER %a" Cil.d_term t;*)
+ (* Options.feedback "REGISTER %a" Cil.d_term t;*)
state_ref := register_term kf !state_ref t;
Cil.DoChildren
| Pseparated tlist ->
diff --git a/src/plugins/eva/utils/eva_perf.ml b/src/plugins/eva/utils/eva_perf.ml
index 84655c882771e48a75fb4a3583555b72d37441ae..7db82e63fe48003fa5b5a2b4dff1d81bf200e2ef 100644
--- a/src/plugins/eva/utils/eva_perf.ml
+++ b/src/plugins/eva/utils/eva_perf.ml
@@ -94,7 +94,7 @@ module Call_info = struct
let list = ref [] in
iter (fun elt ->
let ci = get_ci elt in
- if total_duration current_time ci > threshold
+ if total_duration current_time ci > threshold
then list := elt::!list);
let sorted_list = List.fast_sort
(fun elt1 elt2 -> (cmp current_time) (get_ci elt1) (get_ci elt2)) !list
diff --git a/tools/hdrck/dune-project b/tools/hdrck/dune-project
index c96c6067e4897c2cefb0a05d9d8219bca7602eb9..a7877e55264bccb1fe5bc7d216b0395c59971b38 100644
--- a/tools/hdrck/dune-project
+++ b/tools/hdrck/dune-project
@@ -22,5 +22,5 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(package
- (name frama-c-hdchk)
+ (name frama-c-hdrck)
)
diff --git a/tools/hdrck/hdrck.ml b/tools/hdrck/hdrck.ml
index e8fd61024ec531b223e662b26ccf70d4aac4ae5d..c65802c97ed37153ee18d8e752ff96f0cab20b44 100644
--- a/tools/hdrck/hdrck.ml
+++ b/tools/hdrck/hdrck.ml
@@ -60,7 +60,7 @@ and headache_config_file = ref [] (* empty -> headache_config_file_default *)
and headache_config_file_default = "headers/headache_config.txt"
and exit_on_warning = ref false
and exit_on_error = ref true (* only settable to false for debugging purposes *)
-
+and quiet = ref false
type mode =
| Check
@@ -84,7 +84,8 @@ let job_head fmt =
Format.printf fmt
let job_done () =
- Format.printf "done@."
+ if not !quiet then
+ Format.printf "done@."
let pp_job_first_line () =
if !is_first_job_line then
@@ -258,7 +259,8 @@ let add_spec_entry (ignored_files: StringSet.t ref) (spec_tab: (string, string)
let read_specs spec_format (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t) (spec_file : string option) =
let spec_fname = match spec_file with None -> "--stdin" | Some filename -> filename in
debug "Specification file: %s@." spec_fname ;
- job_head "Checking format of specification file %s... @?" spec_fname;
+ if not !quiet then
+ job_head "Checking format of specification file %s... @?" spec_fname;
let sub_dir = extract_sub_dir spec_fname in
let add_spec, get_line =
let add_spec_item i ~file_name ~license_name =
@@ -337,7 +339,8 @@ let get_header_files ?directories:(dirs=(get_header_dirs ())) () :
let license_path_tbl = Hashtbl.create 23 in
List.iter
(fun dir ->
- job_head "Reading license header definition files from directory %s... @?" dir;
+ if not !quiet then
+ job_head "Reading license header definition files from directory %s... @?" dir;
if Sys.file_exists dir && Sys.is_directory dir then begin
Array.iter
(fun filename ->
@@ -373,7 +376,8 @@ let get_header_files ?directories:(dirs=(get_header_dirs ())) () :
@requires ignored files have been filtered out the specifications
*)
let check_declared_headers specification headers =
- job_head "Checking license specifications are defined... @?" ;
+ if not !quiet then
+ job_head "Checking license specifications are defined... @?" ;
Hashtbl.iter
(fun file header_type ->
if not (Hashtbl.mem headers header_type) then begin
@@ -429,7 +433,8 @@ let check_spec_discrepancies
if ret <> 0 && !debug_flag then extract_header orig_file template_hdr ;
ret = 0
in
- job_head "Checking specification discrepancies... @?";
+ if not !quiet then
+ job_head "Checking specification discrepancies... @?";
let n = ref 0 in
let discrepancies = ref [] in
Hashtbl.iter
@@ -459,7 +464,8 @@ let check_spec_discrepancies
let check_forbidden_headers (forbidden_headers:StringSet.t) header_specifications (distributed_files:StringSet.t) =
if not (StringSet.is_empty forbidden_headers) then begin
- job_head "Checking that all distributed files have no forbidden header specification... @?";
+ if not !quiet then
+ job_head "Checking that all distributed files have no forbidden header specification... @?";
let forbidden = ref [] in
let n = ref 0 in
StringSet.iter
@@ -492,7 +498,8 @@ let check_forbidden_headers (forbidden_headers:StringSet.t) header_specification
* @param exceptions a set of files distributed but that should not be checked
*)
let check files_ignored header_specifications distributed_files exceptions =
- job_head "Checking that all distributed files do exist... @?";
+ if not !quiet then
+ job_head "Checking that all distributed files do exist... @?";
let nonexistent_files =
StringSet.filter (fun f -> not (Sys.file_exists f)) distributed_files
in
@@ -501,7 +508,8 @@ let check files_ignored header_specifications distributed_files exceptions =
"@[<v 2># Non-existing files listed as distributed:@ %a@]@."
StringSet.pp nonexistent_files;
job_done ();
- job_head "Checking that distributed exception files have no license header specification... @?";
+ if not !quiet then
+ job_head "Checking that distributed exception files have no license header specification... @?";
let files_licencied =
Hashtbl.fold
(fun file _ set -> StringSet.add file set)
@@ -518,7 +526,8 @@ let check files_ignored header_specifications distributed_files exceptions =
"@[<v 2># Files distributed with an header exception (even having to be ignored):@ %a@]@."
StringSet.pp ignored_exceptions;
job_done ();
- job_head "Checking that other distributed files have a license header specification... @?";
+ if not !quiet then
+ job_head "Checking that other distributed files have a license header specification... @?";
let files_to_check = StringSet.diff distributed_files exceptions in
let files_specified = StringSet.union files_licencied files_ignored in
let distributed_unspecified = StringSet.diff files_to_check files_specified in
@@ -527,7 +536,8 @@ let check files_ignored header_specifications distributed_files exceptions =
"@[<v 2># Files distributed without specified header:@ %a@]@."
StringSet.pp distributed_unspecified;
job_done ();
- job_head "Checking presence of source files having an header specification... @?" ;
+ if not !quiet then
+ job_head "Checking presence of source files having an header specification... @?" ;
StringSet.iter
(fun filename ->
if not (Sys.file_exists filename) then
@@ -565,7 +575,8 @@ let update_headers ~config_file_opts header_specifications =
else
debug "%s : error updating header" filename
in
- job_head "Updating header files ... @?";
+ if not !quiet then
+ job_head "Updating header files ... @?";
Hashtbl.iter
(fun filename header_name ->
if Sys.file_exists filename then begin
@@ -620,6 +631,8 @@ let rec argspec = [
" print this option list and exits";
"-debug", Arg.Set debug_flag,
" enable debug messages";
+ "-quiet", Arg.Set quiet,
+ "disable most messages";
"-forbidden-headers", Arg.String (fun set -> set_cumulative ~name:"-forbidden-headers" forbidden_headers ~set) ,
"<license name>,... \t none of the checked files may have one of the <license name> []";
@@ -679,7 +692,8 @@ let _ =
let ignored_files = ref StringSet.empty in
if !from_stdin then read_specs (if !zero_stdin then Zero3 else !spec_format) ignored_files specified_files None;
List.iter (fun f -> read_specs !spec_format ignored_files specified_files (Some f)) spec_files;
- Format.printf "- ignored=%d@.- specified=%d@." (StringSet.cardinal !ignored_files) (Hashtbl.length specified_files);
+ if not !quiet then
+ Format.printf "- ignored=%d@.- specified=%d@." (StringSet.cardinal !ignored_files) (Hashtbl.length specified_files);
match !mode with
| Check ->
let stringset_from_opt_file = function
@@ -692,7 +706,8 @@ let _ =
in
let distributed_files = stringset_from_opt_file distrib_file_opt in
let header_exception_files = stringset_from_opt_file header_except_opt in
- Format.printf "- excepted=%d@.- distributed=%d@." (StringSet.cardinal header_exception_files) (StringSet.cardinal distributed_files);
+ if not !quiet then
+ Format.printf "- excepted=%d@.- distributed=%d@." (StringSet.cardinal header_exception_files) (StringSet.cardinal distributed_files);
check ~config_file_opts !ignored_files specified_files distributed_files header_exception_files
| Update ->
update_headers ~config_file_opts specified_files;
diff --git a/tools/lint/dune b/tools/lint/dune
new file mode 100644
index 0000000000000000000000000000000000000000..9240fe33ae0b3204e2c656aab00ac80e037a1518
--- /dev/null
+++ b/tools/lint/dune
@@ -0,0 +1,28 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(executable
+ (public_name frama-c-lint)
+ (name lint)
+ (modules lint)
+ (libraries unix camomile ocp-indent.lexer ocp-indent.lib ocp-indent.dynlink)
+)
diff --git a/tools/lint/dune-project b/tools/lint/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..485c7a1837dfaa1e25cf4340dc66c5d64d82bdb9
--- /dev/null
+++ b/tools/lint/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.2)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(package
+ (name frama-c-lint)
+)
diff --git a/tools/lint/lint.ml b/tools/lint/lint.ml
new file mode 100644
index 0000000000000000000000000000000000000000..645fdf437ee74eedc963d2940d30fcc81cea7c3a
--- /dev/null
+++ b/tools/lint/lint.ml
@@ -0,0 +1,335 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open CamomileLibrary
+
+(**************************************************************************)
+(* Utils *)
+
+let read_buffered channel =
+ let buffer = Buffer.create 0 in
+ let size = 4096 in
+ let load = Bytes.create size in
+ let read = ref @@ input channel load 0 size in
+ while !read <> 0 do
+ Buffer.add_subbytes buffer load 0 !read ;
+ read := input channel load 0 size
+ done ;
+ Buffer.to_bytes buffer
+
+let rec lines_from_buffer acc buffer start =
+ if start = Bytes.length buffer then acc
+ else
+ let line_end = Bytes.index_from buffer start '\000' in
+ let len = line_end - start in
+ let line = Bytes.sub_string buffer start len in
+ lines_from_buffer (line :: acc) buffer (line_end + 1)
+
+let lines_from_in channel =
+ let content = read_buffered channel in
+ let acc = lines_from_buffer [] content 0 in
+ List.rev acc
+
+(**************************************************************************)
+(* Available Checks and corresponding attributes *)
+
+type checks =
+ { eoleof : bool
+ ; indent : bool
+ ; syntax : bool
+ ; utf8 : bool
+ }
+
+let no_checks =
+ { eoleof = false
+ ; indent = false
+ ; syntax = false
+ ; utf8 = false
+ }
+
+let add_attr checks attr value =
+ let value = value = "set" in
+ match attr with
+ | "check-eoleof" -> { checks with eoleof = value }
+ | "check-indent" -> { checks with indent = value }
+ | "check-syntax" -> { checks with syntax = value }
+ | "check-utf8" -> { checks with utf8 = value }
+ | _ -> failwith (Printf.sprintf "Unknown attr %s" attr)
+
+let handled_attr s =
+ s = "check-eoleof" || s = "check-indent" ||
+ s = "check-syntax" || s = "check-utf8"
+
+let ignored_attr s =
+ not (handled_attr s)
+
+(**************************************************************************)
+(* Table of the files to control *)
+
+let table = Hashtbl.create 1031
+
+let get file =
+ try Hashtbl.find table file
+ with Not_found -> no_checks
+
+let rec collect = function
+ | _file :: attr :: _value :: tl when ignored_attr attr ->
+ collect tl
+ | file :: attr :: value :: tl ->
+ let checks = get file in
+ Hashtbl.replace table file (add_attr checks attr value) ;
+ collect tl
+ | [] -> ()
+ | l -> List.iter (Printf.eprintf "Could not load file list %s\n") l
+
+(**************************************************************************)
+(* Functions used to check lint *)
+
+(* UTF8 *)
+
+let is_utf8 content =
+ try UTF8.validate (Bytes.to_string content) ; true
+ with UTF8.Malformed_code -> false
+
+(* Syntax *)
+
+let check_syntax ~update content =
+ let size = Bytes.length content in
+ let out = Buffer.create 0 in
+ let exception Bad_syntax in
+ try
+ let i = ref 0 in
+ let blank = ref (-1) in
+ while !i < size do
+ let byte = Bytes.get content !i in
+ if byte = '\t' then begin
+ if not update then raise Bad_syntax ;
+ if !blank = -1 then blank := Buffer.length out ;
+ Buffer.add_string out " "
+ end
+ else if byte = ' ' then begin
+ if !blank = -1 then blank := Buffer.length out ;
+ Buffer.add_char out ' '
+ end
+ else if byte = '\n' && !blank <> -1 then begin
+ if not update then raise Bad_syntax ;
+ Buffer.truncate out !blank ;
+ Buffer.add_char out '\n' ;
+ blank := -1
+ end
+ else begin
+ Buffer.add_char out byte ;
+ blank := -1
+ end ;
+ incr i
+ done ;
+ if !blank <> -1 then
+ Buffer.truncate out !blank ;
+ let out = Buffer.to_bytes out in
+ if not @@ Bytes.equal out content
+ then out, false
+ else content, true
+ with Bad_syntax ->
+ content, false
+
+(* EOL/EOF *)
+
+let check_eoleof ~update content =
+ let length = Bytes.length content in
+ if length = 0 then content, true
+ else if '\n' = Bytes.get content (length - 1) then content, true
+ else if update then begin
+ let new_content = Bytes.extend content 0 1 in
+ Bytes.set new_content length '\n' ;
+ new_content, false
+ end else
+ content,false
+
+(* Indentation *)
+
+(* ML(I) *)
+
+(* Basically this is OCP-Indent main where all elements related to options have
+ been removed and the printer changed so that it prints into a buffer and not
+ a file.
+*)
+
+let global_config = ref None
+let config () =
+ match !global_config with
+ | None ->
+ let config, syntaxes, dlink = IndentConfig.local_default () in
+ IndentLoader.load ~debug:false dlink ;
+ Approx_lexer.disable_extensions ();
+ List.iter
+ (fun stx ->
+ try Approx_lexer.enable_extension stx
+ with IndentExtend.Syntax_not_found name ->
+ Format.eprintf "Warning: unknown syntax extension %S@." name)
+ syntaxes ;
+ global_config := Some config ;
+ config
+ | Some config -> config
+
+let ocp_indent channel =
+ let config = config () in
+ let buffer = Buffer.create 0 in
+ let out = IndentPrinter.{
+ debug = false; config = config; indent_empty = false; adaptive = true;
+ in_lines = (fun _ -> true);
+ kind = Print (fun s b -> Buffer.add_string b s ; b);
+ }
+ in
+ let stream = Nstream.of_channel channel in
+ Buffer.to_bytes (IndentPrinter.proceed out stream IndentBlock.empty buffer)
+
+let check_ml_indent ~update file =
+ let input = open_in file in
+ let original = read_buffered input in
+ seek_in input 0 ;
+ let modified = ocp_indent input in
+ close_in input ;
+ let result = Bytes.equal original modified in
+ if update && not result then
+ let output = open_out file in
+ output_bytes output modified ;
+ close_out output ;
+ true
+ else
+ result
+
+(* C/H *)
+
+let clang_format_available = ref None
+let clang_format_available () =
+ match !clang_format_available with
+ | None ->
+ clang_format_available :=
+ Some (0 = Sys.command "clang-format --version > /dev/null") ;
+ Option.get !clang_format_available
+ | Some available -> available
+
+let check_c_indent ~update file =
+ if not @@ clang_format_available () then true
+ else
+ let opt = if update then "-i" else "--dry-run -Werror" in
+ 0 = Sys.command (Printf.sprintf "clang-format %s \"%s\"" opt file)
+
+exception Bad_ext
+
+let check_indent ~update file =
+ match Filename.extension file with
+ | ".c" | ".h" -> check_c_indent ~update file
+ | ".ml" | ".mli" -> check_ml_indent ~update file
+ | _ -> raise Bad_ext
+
+let res = ref true
+
+(* Main checks *)
+
+let check ~verbose ~update file params =
+ if verbose then
+ Printf.printf "Checking %s\n" file ;
+ if Sys.is_directory file then ()
+ else begin
+ let in_chan = open_in file in
+ let content = read_buffered in_chan in
+ close_in in_chan ;
+ (* UTF8 *)
+ if params.utf8 then
+ if not @@ is_utf8 content then begin
+ Printf.eprintf "Bad encoding (not UTF8) for %s\n" file ;
+ res := false
+ end ;
+ (* Blanks *)
+ let rewrite = ref false in
+ let syntactic_check checker content message =
+ let new_content, was_ok = checker ~update content in
+ if update && not was_ok
+ then begin rewrite := true ; new_content end
+ else if not was_ok then begin
+ Printf.eprintf "%s for %s\n" message file ;
+ res := false ; new_content
+ end
+ else new_content
+ in
+ let content =
+ if params.syntax
+ then syntactic_check check_syntax content "Bad syntax"
+ else content
+ in
+ let content =
+ if params.eoleof || params.syntax
+ then syntactic_check check_eoleof content "Bad EOF"
+ else content
+ in
+ if !rewrite then begin
+ let out_chan = open_out file in
+ output_bytes out_chan content ;
+ close_out out_chan
+ end ;
+ (* Indentation *)
+ try
+ if params.indent then
+ if not @@ check_indent ~update file then begin
+ Printf.eprintf "Bad indentation for %s\n" file ;
+ res := false
+ end ;
+ with Bad_ext ->
+ Printf.eprintf "Don't know how to (check) indent %s\n" file ;
+ res := false
+ end
+
+(**************************************************************************)
+(* Options *)
+
+let exec_name = Sys.argv.(0)
+let update = ref false
+let verbose = ref false
+
+let rec argspec = [
+ "--help", Arg.Unit print_usage, "print this option list and exits" ;
+ "-u", Arg.Set update, "update ill-formed files (does not handle UTF8 update)" ;
+ "-v", Arg.Set verbose, "verbose mode" ;
+]
+and sort argspec =
+ List.sort (fun (name1, _, _) (name2, _, _) -> String.compare name1 name2)
+ argspec
+and print_usage () =
+ Arg.usage
+ (Arg.align (sort argspec))
+ (Printf.sprintf "Usage: %s [-u]" exec_name) ;
+ exit 0
+
+(**************************************************************************)
+(* Main *)
+
+let () =
+ if not @@ clang_format_available () then
+ Printf.eprintf "clang-format unavailable, I will not check C files" ;
+ Arg.parse
+ (Arg.align (sort argspec))
+ (fun s -> Printf.eprintf "Unknown argument: %s" s)
+ "";
+ collect @@ lines_from_in stdin ;
+ Hashtbl.iter (check ~verbose:!verbose ~update:!update) table ;
+ if not !res then exit 1