diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 400fac41e1ec0022607abf2af7e00e1bb077fd4c..2a1d7c1365562310c3ccd48d2b053d6bc62245c5 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -49,6 +49,14 @@ frama-c: tags: - nix +lint: + stage: build + script: + - nix-build nix/pkgs.nix -A ocamlPackages.lint + coverage: '/lint coverage: \d+\.\d+/' + tags: + - nix + ################################################################################ ### TESTS @@ -72,14 +80,6 @@ plugins-tests: ################################################################################ ### PUBLIC -# lint: -# stage: build -# script: -# - nix/frama-ci.sh build -A frama-c.lint -# coverage: '/lint coverage: \d+\.\d+/' -# tags: -# - nix - # wp-qualif: # stage: tests # script: diff --git a/nix/lint.nix b/nix/lint.nix new file mode 100644 index 0000000000000000000000000000000000000000..6f79ef2ff81350c5d295e72f36ac5ed7fc57b125 --- /dev/null +++ b/nix/lint.nix @@ -0,0 +1,41 @@ +# TODO: +# - enable lint E-ACSL C files +# - enable check-headers + +{ lib +, stdenv +, bc +# , clang_10 +, frama-c +# , headache +, ocp-indent +} : + +stdenv.mkDerivation rec { + pname = "lint"; + version = frama-c.version; + slang = frama-c.slang; + + src = frama-c.src; + + nativeBuildInputs = frama-c.nativeBuildInputs; + + buildInputs = frama-c.buildInputs ++ [ + bc + # headache + ocp-indent + # clang_10 + ]; + + preConfigure = frama-c.preConfigure; + + buildPhase = '' + make lint + make stats-lint + # STRICT_HEADERS=yes make check-headers + ''; + + installPhase = '' + touch $out + ''; +} diff --git a/nix/pkgs.nix b/nix/pkgs.nix index b14ed53562f5b07908058f171db159d7afc32416..a36dae2d38ba4a13c5e468cbf5f9248b222761a2 100644 --- a/nix/pkgs.nix +++ b/nix/pkgs.nix @@ -9,6 +9,7 @@ let why3 = oself.callPackage ./why3.nix {}; # Builds frama-c = oself.callPackage ./frama-c.nix {}; + lint = oself.callPackage ./lint.nix {}; # Tests main-tests = oself.callPackage ./main-tests.nix {}; plugins-tests = oself.callPackage ./plugins-tests.nix {};