From a5f0e4d908a9bcacb256a508e048f67e34518510 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 10 Jun 2022 11:30:13 +0200
Subject: [PATCH] [ci] check headers
---
.gitlab-ci.yml | 9 +++++++++
nix/frama-c-checkers-shell.nix | 18 ++++++++++++++++++
nix/frama-c-hdrck.nix | 34 ++++++++++++++++++++++++++++++++++
nix/pkgs.nix | 11 +++++++++++
share/Makefile.headers | 5 ++---
5 files changed, 74 insertions(+), 3 deletions(-)
create mode 100644 nix/frama-c-checkers-shell.nix
create mode 100644 nix/frama-c-hdrck.nix
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 997066588ac..a68bd7abb73 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -44,6 +44,15 @@ frama-c:
tags:
- nix
+header-check:
+ stage: build
+ script:
+ - ls -la
+ - nix-shell nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.frama-c-checkers-shell
+ --run 'FRAMAC_HDRCK="" make -f share/Makefile.headers check-headers'
+ tags:
+ - nix
+
# ivette:
# stage: build
# image: node:lts-gallium
diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix
new file mode 100644
index 00000000000..a9322dcc9fd
--- /dev/null
+++ b/nix/frama-c-checkers-shell.nix
@@ -0,0 +1,18 @@
+{ lib
+, stdenv
+, frama-c-hdrck
+, git
+, gnumake
+, headache
+, ocp-indent
+} :
+stdenv.mkDerivation rec {
+ name = "frama-c-checkers-shell";
+ buildInputs = [
+ frama-c-hdrck
+ git
+ gnumake
+ headache
+ ocp-indent
+ ];
+}
diff --git a/nix/frama-c-hdrck.nix b/nix/frama-c-hdrck.nix
new file mode 100644
index 00000000000..5c65409ca3e
--- /dev/null
+++ b/nix/frama-c-hdrck.nix
@@ -0,0 +1,34 @@
+{ lib
+, stdenv
+, dune_3
+, gitignoreSource
+, ocaml
+} :
+
+stdenv.mkDerivation rec {
+ pname = "frama-c-hdrck";
+ version =
+ lib.strings.replaceStrings ["~"] ["-"]
+ (lib.strings.removeSuffix "\n"
+ (builtins.readFile ../VERSION));
+ slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
+
+ src = gitignoreSource ./../headers ;
+
+ buildInputs = [
+ dune_3
+ ocaml
+ ];
+
+ configurePhase = ''
+ true
+ '';
+
+ buildPhase = ''
+ dune build --root .
+ '';
+
+ installPhase = ''
+ dune install --prefix $out --root .
+ '';
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 360ab1a15c9..2c28472fde4 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -10,12 +10,21 @@ let
odoc = oself.callPackage ./odoc.nix {};
psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
why3 = oself.callPackage ./why3.nix {};
+
# Helpers
mk_tests = oself.callPackage ./mk_tests.nix {};
mk_plugin = oself.callPackage ./mk_plugin.nix {};
+
+ # Shell containing checkers (hdrck, ocp-indent)
+ frama-c-checkers-shell = oself.callPackage ./frama-c-checkers-shell.nix {
+ git = pkgs.git ;
+ };
+
# Builds
frama-c = oself.callPackage ./frama-c.nix {};
+ frama-c-hdrck = oself.callPackage ./frama-c-hdrck.nix {};
lint = oself.callPackage ./lint.nix {};
+
# Tests
default-config-tests = oself.callPackage ./default-config-tests.nix {};
e-acsl-tests = oself.callPackage ./e-acsl-tests.nix {};
@@ -24,8 +33,10 @@ let
kernel-tests = oself.callPackage ./kernel-tests.nix {};
plugins-tests = oself.callPackage ./plugins-tests.nix {};
wp-tests = oself.callPackage ./wp-tests.nix {};
+
# Internal tests
internal-tests = oself.callPackage ./internal-tests.nix {};
+
# Release
api-doc = oself.callPackage ./api-doc.nix {};
manuals = oself.callPackage ./manuals.nix {};
diff --git a/share/Makefile.headers b/share/Makefile.headers
index a391f4c1994..288edf2e868 100644
--- a/share/Makefile.headers
+++ b/share/Makefile.headers
@@ -67,7 +67,7 @@ HDRCK_EXTRA?=
## Command used to execute hdrck
# Note: the public name of hdrck.exe is frama-c-hdrck
-ifeq ($(FRAMAC_HDRCK),"")
+ifeq ($(FRAMAC_HDRCK),)
# HDRCK is external
HDRCK:= frama-c-hdrck
@@ -101,7 +101,7 @@ $(error "Please set HEADER_SPEC variable to a file containing the header specifi
endif # HEADER_HAS_GIT_FILE
-HDRCK_OPTS+= -z
+HDRCK_OPTS+= -z
else
@@ -185,4 +185,3 @@ headers.info:
# Local Variables:
# compile-command: "make"
# End:
-
--
GitLab