diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix index a9322dcc9fdb25fd705d915f4b2930cd130139fe..9ccc398534f01b7848d92fdb420313ba38e8ffc8 100644 --- a/nix/frama-c-checkers-shell.nix +++ b/nix/frama-c-checkers-shell.nix @@ -1,5 +1,6 @@ { lib , stdenv +, clang_10 , frama-c-hdrck , git , gnumake @@ -9,6 +10,7 @@ stdenv.mkDerivation rec { name = "frama-c-checkers-shell"; buildInputs = [ + clang_10 frama-c-hdrck git gnumake diff --git a/share/Makefile.linting b/share/Makefile.linting index f22e52a19904ae005b929704a521debee43381e8..ae695f837e5eeec5639b28c4423467f1414f9460 100644 --- a/share/Makefile.linting +++ b/share/Makefile.linting @@ -103,6 +103,13 @@ endif $(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 -p $(dir $@) + ############### ## Main target @@ -135,8 +142,10 @@ clean:: clean-lint #### clean-check-XXX targets LINT.clean-targets= \ - clean-check-eoleof clean-check-utf8 clean-check-syntax clean-check-ident -.PHONY: clean-check-eoleof clean-check-utf8 clean-check-syntax clean-check-ident + clean-check-eoleof clean-check-utf8 clean-check-syntax \ + clean-check-indent clean-check-clang-format +.PHONY: clean-check-eoleof clean-check-utf8 clean-check-syntax \ + clean-check-indent clean-check-clang-format # Generic rule $(LINT.clean-targets): @@ -154,8 +163,8 @@ LINT.dir=$(wildcard $(LINT_DIR)) #### check-XXX targets LINT.check-targets= \ - check-syntax check-indent check-eoleof check-utf8 -.PHONY: check-syntax check-indent check-eoleof check-utf8 + check-syntax check-indent check-clang-format check-eoleof check-utf8 +.PHONY: check-syntax check-indent check-clang-format check-eoleof check-utf8 # Generic rule $(LINT.check-targets): @@ -168,8 +177,8 @@ $(LINT.check-targets): #### fix-XXX targets LINT.fix-targets= \ - fix-eoleof fix-utf8 fix-syntax fix-ident -.PHONY: fix-eoleof fix-utf8 fix-syntax fix-ident + fix-eoleof fix-utf8 fix-syntax fix-indent fix-clang-format +.PHONY: fix-eoleof fix-utf8 fix-syntax fix-indent fix-clang-format # Generic rule $(LINT.fix-targets): @@ -190,11 +199,13 @@ 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.check-clang-format= $(addsuffix .check-clang-format,$(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)) +LINT_FILE.fix-clang-format= $(addsuffix .fix-clang-format,$(LINT_FILE.list)) ## check-XXX targets @@ -210,6 +221,9 @@ check-syntax: $(LINT_FILE.check-syntax) .PHONY: check-indent check-indent: $(LINT_FILE.check-indent) +.PHONY: check-clang-format +check-clang-format: $(LINT_FILE.check-clang-format) + ## fix-XXX targets .PHONY: fix-utf8 @@ -224,6 +238,9 @@ fix-syntax: $(LINT_FILE.fix-syntax) .PHONY: fix-indent fix-indent: $(LINT_FILE.fix-indent) +.PHONY: fix-clang-format +fix-clang-format: $(LINT_FILE.fix-clang-format) + endif ############################### @@ -262,7 +279,7 @@ $(LINT_FILE.fix-utf8): .lint/%.fix-utf8: % .lint/check-ocp-indent-version endif # LINT_FROM_ENCODING ############################### -## INDENTATION ASPECT +## ML INDENTATION ASPECT $(LINT_FILE.check-indent): .lint/%.check-indent: % .lint/check-ocp-indent-version echo "Check indent: $<" @@ -285,6 +302,22 @@ $(LINT_FILE.fix-indent): .lint/%.fix-indent: % .lint/check-ocp-indent-version $(MKDIR) $(dir $@) $(TOUCH) .lint/$<.check-indent # no more need of check-indent +############################### +## C INDENTATION ASPECT + +$(LINT_FILE.check-clang-format): .lint/%.check-clang-format: % .lint/check-clang-format-installed + echo "Check clang-format: $<" + clang-format --dry-run -Werror $< + $(MKDIR) $(dir $@) + $(TOUCH) $@ + +.PHONY: $(LINT_FILE.fix-clang-format) +$(LINT_FILE.fix-clang-format): .lint/%.fix-clang-format: % .lint/check-clang-format-installed + echo "Fixes clang-format: $<" + clang-format -i $< + $(MKDIR) $(dir $@) + $(TOUCH) .lint/$<.check-indent # no more need of check-indent + ############################### ## EOL EOF ASPECT (included by check-syntax target) diff --git a/src/plugins/e-acsl/.gitattributes b/src/plugins/e-acsl/.gitattributes index 0533773bd46873ec670467867e58c6aad19971f5..e69c6c626ef5aa224cf2bee26a2ab4c594e63cd0 100644 --- a/src/plugins/e-acsl/.gitattributes +++ b/src/plugins/e-acsl/.gitattributes @@ -23,6 +23,13 @@ Makefile.in header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /scripts/e-acsl-gcc.sh.comp header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /scripts/e-acsl-gcc.sh.comp header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +########################################### +# CHECK-INDENT # +########################################### + +/tests/*/*.c check-syntax check-clang-format +/share/**/*.c check-syntax check-clang-format + ######################## # HEADER_SPEC: .ignore # ######################## @@ -69,4 +76,3 @@ README header_spec=.ignore /tests/E_ACSL_test.ml header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /contrib/libdlmalloc/dlmalloc.* header_spec=MODIFIED_DLMALLOC /share/e-acsl/internals/e_acsl_rtl_io.* header_spec=MODIFIED_SPARETIMELABS - 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 608c3bf745430f67205aadd40206e6f869dace2a..9e5dd8f5f57cc7ae8befa78281fae1ec6a13849a 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 @@ -167,7 +167,7 @@ void validate_shadow_layout() { # endif /* Each segment has 3 partitions: - - application memory + - application memory - primary/secondary shadows */ int num_partitions = sizeof(mem_partitions) / sizeof(memory_partition *); int num_seg_in_part = 3; diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c index 3878a97a1d6a1b319cf5893a152b6d3b65d85b7e..d8a64368f3045c94265d674bcbc21036a24d6192 100644 --- a/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c @@ -1,5 +1,5 @@ /* run.config - COMMENT: frama-c/e-acsl#105, test for delete block before exiting the + COMMENT: frama-c/e-acsl#105, test for delete block before exiting the function in the presence of early return. */