From 8d71165db45200d93c1695722ee411a73c01d74e Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 13 Jun 2022 08:54:17 +0200
Subject: [PATCH] [headers] allows to save header spec into a file

---
 share/Makefile.headers | 35 +++++++++++++++++++++++++++++++----
 1 file changed, 31 insertions(+), 4 deletions(-)

diff --git a/share/Makefile.headers b/share/Makefile.headers
index aee2daf602d..74392e03e34 100644
--- a/share/Makefile.headers
+++ b/share/Makefile.headers
@@ -56,10 +56,14 @@ HEADER_DISTRIB_FILE?=
 # - <file>: file containing the list of the files to ignore any way
 HEADER_EXCEPTIONS?=
 
-# Can be set to a list of files
-# - <files>: files containing, for each file to manage, the "header_spec" attribute value
+# 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?=
 
@@ -95,20 +99,42 @@ ifneq ($(HEADER_HAS_GIT),)
 
 # From git (including git work-trees)
 HDRCK_SPEC:= git ls-files -z | git check-attr --stdin -z header_spec
+HDRCK_OPTS+= -z
+
 else
 
+# Note: in such a case, GIT is required...
 HDRCK_SPEC:=
 
-endif # HEADER_HAS_GIT_FILE
+endif # HEADER_HAS_GIT
 
+else # HEADER_SPEC
+
+ifeq ($(HEADER_SAVE_SPEC),yes)
+
+HEADER_HAS_GIT:=$(wildcard .git)
+ifneq ($(HEADER_HAS_GIT),)
+
+# From git (including git work-trees)
+HDRCK_SPEC:= git ls-files -z | git check-attr --stdin -z header_spec | tee $(HEADER_SPEC)
 HDRCK_OPTS+= -z
 
 else
 
+# Note: in such a case, GIT is required...
+HDRCK_SPEC:=
+
+endif # HEADER_HAS_GIT
+
+else # HEADER_SAVE_SPEC
+
 # From a file
-# note: The file  format has to be specified into the var HDRCK_EXTRA
 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
 
 ################################
@@ -198,3 +224,4 @@ headers.info:
 # Local Variables:
 # compile-command: "make"
 # End:
+
-- 
GitLab