diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 5f32c25ff70a79ad3d17b9d9df41260a9067a9df..9013c1219ce5776dd6678c2e0e0edb62ddaa9127 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -8,7 +8,7 @@ There are several ways to participate in the Frama-C project:
- Asking questions and discussing at
[StackOverflow](https://stackoverflow.com/tags/frama-c) and through
the
- [Frama-C-discuss mailing list](https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss);
+ [Frama-C-discuss mailing list](https://groupes.renater.fr/sympa/info/frama-c-discuss);
- Reporting bugs via
[Gitlab issues](https://git.frama-c.com/pub/frama-c/issues);
@@ -65,9 +65,14 @@ The detailed steps to submit a contribution to Frama-C are:
discussion and we will integrate it.
7. Check for unexpected changes.
- Use the command `make lint`
+ Use the command `make check-lint`
in your terminal from the Frama-C root directory to detect trailing spaces,
- tabulations or incorrect indentation (ocp-ident >= 1.7.0 is needed).
+ tabulations or incorrect indentation (ocp-ident >= 1.8.1, camomile and
+ clang-format are needed), and `make lint` to fix problems if any.
+
+ Use the command `make check-headers` in your terminal from the Frama-C root
+ directory to detect bad file license (headache is needed), and `make headers`
+ to fix them.
8. Locally run the test framework of Frama-C by typing
`make tests`
diff --git a/INSTALL.md b/INSTALL.md
index c96417803dc89bc93d8e8536eb03b88c6f5dda00..d43839feeee8aae83f3d24275806e3ca1f925211 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -21,6 +21,7 @@
- [Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)](#plugin-files-in-install_dirlibframa-cplugins)
- [Man files: (in `/INSTALL_DIR/share/man/man1`)](#man-files-in-install_dirsharemanman1)
- [Installing Additional Frama-C Plugins](#installing-additional-frama-c-plugins)
+- [Frama-C additional tools](#frama-c-additional-tools)
- [HAVE FUN WITH FRAMA-C!](#have-fun-with-frama-c)
## Installing Frama-C via opam
@@ -484,5 +485,31 @@ The standard way for installing them should be:
Plugins may have their own custom installation procedures.
Consult their specific documentation for details.
+# Frama-C additional tools
+
+A few additional tools that are unnecessary for most users might be useful for
+plugin developers. These tools are:
+- `frama-c-lint`, used for checking coding conventions
+- `frama-c-hdrck`, used for checking file license headers
+
+They can be installed either by pinning them via Opam:
+
+```
+opam pin tools/lint
+opam pin tools/hdrck
+```
+
+Or by compiling/installing Frama-C manually in developer mode:
+```
+FRAMAC_DEVELOPER=yes make
+FRAMAC_DEVELOPER=yes make install
+
+# Or:
+make -C tools/<the-tool>
+make -C tools/<the-tool> install
+```
+
+For convenience, `FRAMAC_DEVELOPER` can be exported globally.
+
# HAVE FUN WITH FRAMA-C!
diff --git a/Makefile b/Makefile
index 81cce48e4319a4f780159c3f53c6d3c9c442931a..55b3564f36a7eca0495d2fa51df230736cc8e2c8 100644
--- a/Makefile
+++ b/Makefile
@@ -23,6 +23,7 @@
# This file is the main makefile of Frama-C.
MAKECONFIG_DIR=share
+FRAMAC_DEVELOPER?=
include $(MAKECONFIG_DIR)/Makefile.common
@@ -42,7 +43,11 @@ FRAMAC_LINTCK_SRC:=tools/lint
.PHONY: all
-all:
+all::
+ifeq (${FRAMAC_DEVELOPER},yes)
+ dune build --no-print-directory --root ${FRAMAC_LINTCK_SRC}
+ dune build --no-print-directory --root ${FRAMAC_HDRCK_SRC}
+endif
ifneq ($(DISABLED_PLUGINS),)
dune clean
rm -rf _build .merlin
@@ -51,9 +56,11 @@ endif
dune build $(DUNE_BUILD_OPTS) @install
clean:: purge-tests # to be done before a "dune" command
+ifeq (${FRAMAC_DEVELOPER},yes)
+ dune clean --no-print-directory --root ${FRAMAC_LINTCK_SRC}
+ dune clean --no-print-directory --root ${FRAMAC_HDRCK_SRC}
+endif
dune clean
- dune clean --root $(FRAMAC_PTESTS_SRC)
- dune clean --root $(FRAMAC_HDRCK_SRC)
rm -rf _build .merlin
##############################################################################
@@ -71,9 +78,26 @@ help::
# INSTALL/UNINSTALL
################################
+install:: all
+
+INSTALL_TARGET=Frama-C
include share/Makefile.installation
include ivette/Makefile.installation
+ifeq (${FRAMAC_DEVELOPER},yes)
+
+install::
+ @echo "Installing frama-c-hdrck and frama-c-lint"
+ dune install --root ${FRAMAC_HDRCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+ dune install --root ${FRAMAC_LINTCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+
+uninstall::
+ @echo "Uninstalling frama-c-hdrck and frama-c-lint"
+ dune uninstall --root ${FRAMAC_HDRCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+ dune uninstall --root ${FRAMAC_LINTCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+
+endif
+
###############################################################################
# HEADER MANAGEMENT
################################
diff --git a/nix/plugin-checkers-shell.nix b/nix/plugin-checkers-shell.nix
index dfb0113011f38d97e8bd6d935846c3837132083f..d64816338da7d7eac446892378de4787df1d1d90 100644
--- a/nix/plugin-checkers-shell.nix
+++ b/nix/plugin-checkers-shell.nix
@@ -1,6 +1,9 @@
{ lib
, stdenv
+, clang_10
, frama-c
+, frama-c-hdrck
+, frama-c-lint
, git
, gnumake
, headache
@@ -9,7 +12,10 @@
stdenv.mkDerivation rec {
name = "plugin-checkers-shell";
buildInputs = [
+ clang_10
frama-c
+ frama-c-hdrck
+ frama-c-lint
git
gnumake
headache
diff --git a/opam b/opam
index 85ed6fb6bb1ed98ff70c82bcadfd925c56d1fd1b..11c84d7213e597d6adba571ca92991676a1bb1b2 100644
--- a/opam
+++ b/opam
@@ -124,10 +124,6 @@ depends: [
"yojson" {>= "1.6.0" & (< "2.0.0" | !with-test)}
"zarith" { >= "1.5" }
- # To be removed when frama-c-lint/hdrck are in separate opam packages
- "camomile"
- "ocp-indent"
-
# PPXs
"ppx_deriving"
"ppx_deriving_yojson"
diff --git a/share/Makefile.installation b/share/Makefile.installation
index ffd7336353df46971e2b780e26722b328ea5203b..d89e9d704eeb06ac9ebacab50ed7b421a6cc69e6 100644
--- a/share/Makefile.installation
+++ b/share/Makefile.installation
@@ -24,6 +24,8 @@
# INSTALLATION #
################
+INSTALL_TARGET?=
+
################################
## Help
@@ -50,22 +52,26 @@ endif
.PHONY: install uninstall
+ifneq ($(INSTALL_TARGET),)
+INSTALL_TARGET:="$(INSTALL_TARGET) "
+endif
+
install::
ifndef PREFIX
- @echo "Warning: cannot install Frama-C: no PREFIX defined"
+ @echo "Warning: cannot install: no PREFIX defined"
@echo " (recommendation: include FRAMAC/share/Makefile.common)"
@exit 1
else
ifeq ($(PREFIX),$(OPAM_SWITCH_PREFIX))
- @echo "Installing Frama-C to current Opam switch"
- @echo " (copying and relocating files...)"
+ @echo "Installing $(INSTALL_TARGET)to current Opam switch"
+ @echo -n " Copying and relocating files..."
dune install ${MANDIR_OPT} 2> /dev/null
- @echo " (done)"
+ @echo " (done)"
else
- @echo "Installing Frama-C to ${PREFIX}"
- @echo " (copying and relocating files...)"
+ @echo "Installing $(INSTALL_TARGET)to ${PREFIX}"
+ @echo -n " Copying and relocating files..."
dune install --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
- @echo " (done)"
+ @echo " (done)"
@echo 'DO NOT FORGET TO EXPAND YOUR OCAMLPATH VARIABLE:'
@echo ' export OCAMLPATH="${PREFIX}/lib:$$OCAMLPATH"'
endif
@@ -73,6 +79,6 @@ endif
ifdef PREFIX
uninstall::
- @echo "Uninstalling Frama-C"
+ @echo "Uninstalling $(INSTALL_TARGET)"
dune uninstall --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
endif
diff --git a/tools/dune b/tools/dune
new file mode 100644
index 0000000000000000000000000000000000000000..fac95f8e3514e644de583e6f230db084e163a6c8
--- /dev/null
+++ b/tools/dune
@@ -0,0 +1,24 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; Note: here we *ignore* other tools, that are not for casual users
+(dirs ptests)
diff --git a/tools/hdrck/Makefile b/tools/hdrck/Makefile
index 9ac5878d11e189c580ee42dbfc4ae58ac7778de1..09aa3c0dc4b6b0aeeb0273f9a40e4da3b37b7ca8 100644
--- a/tools/hdrck/Makefile
+++ b/tools/hdrck/Makefile
@@ -20,15 +20,17 @@
# #
##########################################################################
-.PHONY: all
-all: hdrck.exe
+FRAMAC_SHARE?=../../share
-.PHONY: hdrck.exe
-ptests.exe:
- dune build --root . hdrck.exe
+all:
+ dune build --root .
.PHONY: clean
clean:
dune clean --root .
+INSTALL_TARGET=frama-c-hdrck
+include ${FRAMAC_SHARE}/Makefile.common
+include ${FRAMAC_SHARE}/Makefile.installation
+
##########################################################################
diff --git a/tools/hdrck/frama-c-hdrck.opam b/tools/hdrck/frama-c-hdrck.opam
new file mode 100644
index 0000000000000000000000000000000000000000..95cd527fb24a67755af49e542304e628191bedea
--- /dev/null
+++ b/tools/hdrck/frama-c-hdrck.opam
@@ -0,0 +1,27 @@
+opam-version: "2.0"
+name: "frama-c-hdrck"
+synopsis: "Frama-C header check tool"
+version: "26.0+dev"
+description:"""
+Performs all checks related to file headers as required by the Frama-C
+continuous integration.
+"""
+maintainer: "allan.blanchard@cea.fr"
+authors: [
+ "Patrick Baudin"
+ "Richard Bonichon"
+]
+homepage: "https://frama-c.com/"
+license: "LGPL-2.1-only"
+dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
+bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
+build: [
+ "dune" "build" "-j%{jobs}%" "--release"
+]
+install: [
+ "dune" "install" "-j%{jobs}%" "--prefix=%{prefix}%"
+]
+depends: [
+ "dune" { > "3.2.0" }
+ "headache"
+]
diff --git a/tools/lint/Makefile b/tools/lint/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..aefe5bcc60e3120baec7667cacec4831b29037cc
--- /dev/null
+++ b/tools/lint/Makefile
@@ -0,0 +1,36 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
+FRAMAC_SHARE?=../../share
+
+all:
+ dune build --root .
+
+.PHONY: clean
+clean:
+ dune clean --root .
+
+INSTALL_TARGET=frama-c-lint
+include ${FRAMAC_SHARE}/Makefile.common
+include ${FRAMAC_SHARE}/Makefile.installation
+
+##########################################################################
diff --git a/tools/lint/frama-c-lint.opam b/tools/lint/frama-c-lint.opam
new file mode 100644
index 0000000000000000000000000000000000000000..d7c1d0324a45a9fc6d1733f46d7654b865ca3233
--- /dev/null
+++ b/tools/lint/frama-c-lint.opam
@@ -0,0 +1,29 @@
+opam-version: "2.0"
+name: "frama-c-lint"
+synopsis: "Frama-C lint tool"
+version: "26.0+dev"
+description:"""
+Performs all checks related to source code formatting as required by the Frama-C
+continuous integration. Namely: OCP-indent for ML files, clang-format for E-ACSL
+C files, UTF8 for all text files, newline at EOF, no trailing whitespaces.
+"""
+maintainer: "allan.blanchard@cea.fr"
+authors: [
+ "Allan Blanchard"
+]
+homepage: "https://frama-c.com/"
+license: "LGPL-2.1-only"
+dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
+bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
+build: [
+ "dune" "build" "-j%{jobs}%" "--release"
+]
+install: [
+ "dune" "install" "-j%{jobs}%" "--prefix=%{prefix}%"
+]
+depends: [
+ "dune" { > "3.2.0" }
+ "camomile"
+ "conf-clang-format"
+ "ocp-indent" { = "1.8.1" }
+]
diff --git a/tools/lint/lint.ml b/tools/lint/lint.ml
index 645fdf437ee74eedc963d2940d30fcc81cea7c3a..c850d068c80c5c6144dcf004ebd554d6613d3c17 100644
--- a/tools/lint/lint.ml
+++ b/tools/lint/lint.ml
@@ -306,19 +306,13 @@ 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" ;
+let argspec = [
+ "-u", Arg.Set update, " update ill-formed files (does not handle UTF8 update)" ;
+ "-v", Arg.Set verbose, " verbose mode" ;
]
-and sort argspec =
+let 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 *)
@@ -329,7 +323,7 @@ let () =
Arg.parse
(Arg.align (sort argspec))
(fun s -> Printf.eprintf "Unknown argument: %s" s)
- "";
+ ("Usage: git ls-files -z | git check-attr --stdin -z -a | " ^ exec_name ^ " [options]");
collect @@ lines_from_in stdin ;
Hashtbl.iter (check ~verbose:!verbose ~update:!update) table ;
if not !res then exit 1