diff --git a/.gitattributes b/.gitattributes
index 6a0f88f21cc3f5ddec2179e4435d38f98499eb6d..6cda6f9c55b63eaec3772a1c1f01bb441e6410a0 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,3 +1,284 @@
+################
+# MERGE: union #
+################
+
Changelog merge=union
+###############
+# BINARY: set #
+###############
+# built-in macro that also unsets the "text" and "diff" attributes
+
+*.eps binary
+*.ps binary
+
*.pdf binary
+
+#########################
+# HEADER_SPEC: CEA_LGPL #
+#########################
+
+config* header_spec=CEA_LGPL
+
+makefile* header_spec=CEA_LGPL
+Make* header_spec=CEA_LGPL
+*.mk header_spec=CEA_LGPL
+
+*.c header_spec=CEA_LGPL
+*.h header_spec=CEA_LGPL
+
+*.htm header_spec=CEA_LGPL
+*.html header_spec=CEA_LGPL
+
+*.js header_spec=CEA_LGPL
+
+*.ml header_spec=CEA_LGPL
+*.ml.in header_spec=CEA_LGPL
+*.mli header_spec=CEA_LGPL
+*.mli.in header_spec=CEA_LGPL
+*.mll header_spec=CEA_LGPL
+*.mly header_spec=CEA_LGPL
+
+*.pl header_spec=CEA_LGPL
+
+*.py header_spec=CEA_LGPL
+
+*.rc header_spec=CEA_LGPL
+
+*.sh header_spec=CEA_LGPL
+*.zsh header_spec=CEA_LGPL
+
+*.css header_spec=CEA_LGPL
+
+*.ts header_spec=CEA_LGPL
+*.tsx header_spec=CEA_LGPL
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+.gitattributes header_spec=.ignore
+.gitignore header_spec=.ignore
+.gitkeep header_spec=.ignore
+.git-blame-ignore-revs header_spec=.ignore
+
+.merlin header_spec=.ignore
+
+Changelog header_spec=.ignore
+opam header_spec=.ignore
+
+README* header_spec=.ignore
+*.README* header_spec=.ignore
+
+*.dot header_spec=.ignore
+*.fig header_spec=.ignore
+
+*.eps header_spec=.ignore
+*.ps header_spec=.ignore
+
+*.gif header_spec=.ignore
+*.ico header_spec=.ignore
+*.jpg header_spec=.ignore
+*.jpeg header_spec=.ignore
+*.png header_spec=.ignore
+*.svg header_spec=.ignore
+
+*.nix header_spec=.ignore
+*.md header_spec=.ignore
+*.opam header_spec=.ignore
+
+*.pdf header_spec=.ignore
+
+.tex header_spec=.ignore
+*.sty header_spec=.ignore
+*.bib header_spec=.ignore
+
+*.odoc header_spec=.ignore
+
+/.for_devel header_spec=.ignore
+/.force-reconfigure header_spec=.ignore
+/.gitlab-ci.yml header_spec=.ignore
+/.make-clean* header_spec=.ignore
+/.mailmap header_spec=.ignore
+/.ocp-indent header_spec=.ignore
+/ALL_VERSIONS header_spec=.ignore
+/LICENSE header_spec=.ignore
+/VERSION header_spec=.ignore
+/VERSION_CODENAME header_spec=.ignore
+
+/bin/sed_get_* header_spec=.ignore
+
+/devel_tools/docker/*.template header_spec=.ignore
+
+# TODO: header_spec=JCF_LGPL_2_only
+/devel_tools/size.mli header_spec=.ignore
+/devel_tools/size.ml header_spec=.ignore
+/devel_tools/size_states.ml header_spec=.ignore
+/devel_tools/size_states.mli header_spec=.ignore
+
+/doc/CC-BY-SA-4.0 header_spec=.ignore
+/doc/CHANGES.obfuscator header_spec=.ignore
+/doc/LICENSE header_spec=.ignore
+/doc/MakeLaTeXModern header_spec=.ignore
+/doc/acsl_tutorial_slides/script header_spec=.ignore
+/doc/developer/METADOC.txt header_spec=.ignore
+/doc/qualification/testing header_spec=.ignore
+/doc/release/periodic-elements.txt header_spec=.ignore
+/doc/value/watchpoints header_spec=.ignore
+/doc/scope/M.v header_spec=.ignore
+
+/doc/aorai/example/example* header_spec=.ignore
+/doc/frama-c-book.* header_spec=.ignore
+/doc/*.hva header_spec=.ignore
+
+/doc/training/**/* header_spec=.ignore
+/doc/value/examples/parametrizing/*.log header_spec=.ignore
+/doc/**/make* header_spec=.ignore
+/doc/**/TODO header_spec=.ignore
+/doc/**/*.bnf header_spec=.ignore
+/doc/**/*.c header_spec=.ignore
+/doc/**/*.graphml header_spec=.ignore
+/doc/**/*.h header_spec=.ignore
+/doc/**/*.html header_spec=.ignore
+/doc/**/*.lua header_spec=.ignore
+/doc/slicing/algo.ml header_spec=.ignore
+/doc/*/*/**/*.ml header_spec=.ignore
+/doc/**/*.mli header_spec=.ignore
+/doc/**/*.mll header_spec=.ignore
+/doc/**/*.oracle header_spec=.ignore
+/doc/**/*.tex header_spec=.ignore
+/doc/*/*/**/*.txt header_spec=.ignore
+/doc/**/*.sh header_spec=.ignore
+
+/headers/open-source/* header_spec=.ignore
+/headers/close-source/* header_spec=.ignore
+
+/licenses/* header_spec=.ignore
+
+/man/frama-c.1 header_spec=.ignore
+
+/nix/empty header_spec=.ignore
+/nix/frama-c-public/known_hosts header_spec=.ignore
+
+/share/framac.vim header_spec=.ignore
+/share/META.frama-c header_spec=.ignore
+/share/analysis-scripts/readme-graph.graphml header_spec=.ignore
+/share/analysis-scripts/pyproject.toml header_spec=.ignore
+/share/win32_installer.iss header_spec=.ignore
+/share/win32_manual_installation_step.txt header_spec=.ignore
+/share/compliance/*.json header_spec=.ignore
+
+/tests/**/* header_spec=.ignore
+
+#######################
+# HEADER_SPEC: others #
+#######################
+
+/configure.in header_spec=CEA_INRIA_LGPL
+
+/doc/aorai/Makefile header_spec=AORAI_LGPL
+
+/share/analysis-scripts/flamegraph.pl header_spec=CDDL
+/share/emacs/acsl.el header_spec=CEA_PR_LGPL
+/share/libc/argz.h header_spec=CEA_FSF_LGPL
+/share/libc/argz.c header_spec=CEA_FSF_LGPL
+/share/machdep.c header_spec=CIL
+
+/src/kernel_internals/parsing/clexer.mli header_spec=CIL
+/src/kernel_internals/parsing/clexer.mll header_spec=CIL
+/src/kernel_internals/parsing/cparser.mly header_spec=CIL
+/src/kernel_internals/parsing/errorloc.ml header_spec=CIL
+/src/kernel_internals/parsing/errorloc.mli header_spec=CIL
+/src/kernel_internals/parsing/lexerhack.ml header_spec=CIL
+/src/kernel_internals/parsing/lexerhack.mli header_spec=CIL
+/src/kernel_internals/parsing/logic_lexer.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_lexer.mll header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_parser.mly header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_preprocess.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_preprocess.mll header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/runtime/machdeps.ml header_spec=CIL
+/src/kernel_internals/runtime/machdeps.mli header_spec=CIL
+/src/kernel_internals/typing/alpha.ml header_spec=CIL
+/src/kernel_internals/typing/alpha.mli header_spec=CIL
+/src/kernel_internals/typing/cabs2cil.ml header_spec=CIL
+/src/kernel_internals/typing/cabs2cil.mli header_spec=CIL
+/src/kernel_internals/typing/cfg.ml header_spec=CIL
+/src/kernel_internals/typing/cfg.mli header_spec=CIL
+/src/kernel_internals/typing/frontc.ml header_spec=CIL
+/src/kernel_internals/typing/frontc.mli header_spec=CIL
+/src/kernel_internals/typing/logic_builtin.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/typing/logic_builtin.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/typing/mergecil.ml header_spec=CIL
+/src/kernel_internals/typing/mergecil.mli header_spec=CIL
+/src/kernel_internals/typing/oneret.ml header_spec=CIL
+/src/kernel_internals/typing/oneret.mli header_spec=CIL
+/src/kernel_internals/typing/rmtmps.ml header_spec=CIL
+/src/kernel_internals/typing/rmtmps.mli header_spec=CIL
+/src/kernel_internals/typing/translate_lightweight.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/typing/translate_lightweight.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/analysis/dataflows.ml header_spec=CIL
+/src/kernel_services/analysis/dataflows.mli header_spec=CIL
+/src/kernel_services/ast_data/cil_types.mli header_spec=CIL
+/src/kernel_services/ast_printing/cprint.ml header_spec=CIL
+/src/kernel_services/ast_printing/cprint.mli header_spec=CIL
+/src/kernel_services/ast_printing/logic_print.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_printing/logic_print.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/cil.ml header_spec=CIL
+/src/kernel_services/ast_queries/cil.mli header_spec=CIL
+/src/kernel_services/ast_queries/cil_builtins.ml header_spec=CIL
+/src/kernel_services/ast_queries/cil_builtins.mli header_spec=CIL
+/src/kernel_services/ast_queries/cil_const.ml header_spec=CIL
+/src/kernel_services/ast_queries/cil_const.mli header_spec=CIL
+/src/kernel_services/ast_queries/logic_const.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_const.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_env.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_env.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_typing.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_typing.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_utils.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_utils.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/parsetree/cabs.mli header_spec=CIL
+/src/kernel_services/parsetree/cabshelper.ml header_spec=CIL
+/src/kernel_services/parsetree/cabshelper.mli header_spec=CIL
+/src/kernel_services/parsetree/logic_ptree.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/visitors/cabsvisit.ml header_spec=CIL
+/src/kernel_services/visitors/cabsvisit.mli header_spec=CIL
+/src/kernel_services/visitors/visitor_behavior.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/visitors/visitor_behavior.mli header_spec=CEA_INRIA_LGPL
+
+/src/libraries/datatype/unmarshal.ml header_spec=INRIA_BSD
+/src/libraries/datatype/unmarshal.mli header_spec=INRIA_BSD
+/src/libraries/datatype/unmarshal_hashtbl_test.ml header_spec=INRIA_BSD
+/src/libraries/datatype/unmarshal_test.ml header_spec=INRIA_BSD
+/src/libraries/project/state_topological.ml header_spec=MODIFIED_OCAMLGRAPH
+/src/libraries/project/state_topological.mli header_spec=MODIFIED_OCAMLGRAPH
+/src/libraries/utils/cilconfig.ml header_spec=CIL
+/src/libraries/utils/cilconfig.mli header_spec=CIL
+/src/libraries/utils/escape.ml header_spec=CIL
+/src/libraries/utils/escape.mli header_spec=CIL
+/src/libraries/utils/hptmap.ml header_spec=MODIFIED_MENHIR
+/src/libraries/utils/hptmap.mli header_spec=MODIFIED_MENHIR
+/src/libraries/utils/hptmap_sig.mli header_spec=MODIFIED_MENHIR
+/src/libraries/utils/rangemap.ml header_spec=OCAML_STDLIB
+/src/libraries/utils/rangemap.mli header_spec=OCAML_STDLIB
+/src/libraries/utils/utf8_logic.ml header_spec=CEA_INRIA_LGPL
+/src/libraries/utils/utf8_logic.mli header_spec=CEA_INRIA_LGPL
+
+#########################
+# HEADER_SPEC: CEA_LGPL #
+#########################
+
+/bin/frama-c* header_spec=CEA_LGPL
+
+/doc/code/*.txt header_spec=CEA_LGPL
+/devel_tools/git-hooks/pre-commit header_spec=CEA_LGPL
+
+/headers/headache_config.txt header_spec=CEA_LGPL
+/headers/*.sh header_spec=CEA_LGPL_OR_PROPRIETARY
+
+/share/autocomplete_frama-c header_spec=CEA_LGPL
+/share/emacs/frama-c-*.el header_spec=CEA_LGPL
+/share/_frama-c header_spec=CEA_LGPL
+
+/src/kernel_internals/runtime/fc_config.ml.in header_spec=CEA_LGPL
+/src/libraries/stdlib/transitioning.ml.in header_spec=CEA_LGPL
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index efda42643c9bf1b79817c11114274f15e70b74a6..bb1682475f5153d6f94ce3bc27e397080fe732ce 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -1,4 +1,25 @@
#! /usr/bin/env bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
set -u
diff --git a/bin/check-reference-configuration.sh b/bin/check-reference-configuration.sh
index e91365642881b711352f863c119deecc00de901e..6095ffc385bf0c6f31ae5a25dd1ec3f32844e3fc 100755
--- a/bin/check-reference-configuration.sh
+++ b/bin/check-reference-configuration.sh
@@ -1,4 +1,25 @@
#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# Displays the current working configuration of OCaml dependencies of Frama-C,
# comparing them with the one in `reference-configuration.md`.
diff --git a/bin/check_newlines.ml b/bin/check_newlines.ml
index 4524bdc80d9d1e14edd919acb4de2e4db746a7eb..29e3c5a2dadb2f66097b57bb68010435ce1bf968 100644
--- a/bin/check_newlines.ml
+++ b/bin/check_newlines.ml
@@ -1,3 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
module StringSet = Set.Make(String)
(* returns true for empty files *)
diff --git a/bin/git.sh b/bin/git.sh
index 18e931bd054a7e66969122c00a9def62d2048bf9..f5b81e49bcf8b17404963987b204acb9cddf47e1 100755
--- a/bin/git.sh
+++ b/bin/git.sh
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
ACTION="$*"
if [ "$ACTION" == "" ]
diff --git a/bin/indent.sh b/bin/indent.sh
index 9c402daacff0384024c5a86f412f0a8169488007..68ad76654dd84b51ad583c3d28f218d0c47513e6 100755
--- a/bin/indent.sh
+++ b/bin/indent.sh
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# Help
case "$1" in
diff --git a/bin/isutf8.ml b/bin/isutf8.ml
index 5950a0c6b826126676304be8212ae28b53c0cfdb..0e775f13502710afea395fa9aadb2686ca72b40d 100644
--- a/bin/isutf8.ml
+++ b/bin/isutf8.ml
@@ -1,3 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
module StringSet = Set.Make(String)
exception False
diff --git a/bin/lint.sh b/bin/lint.sh
index 797b61e433cb7aa56eac155c2bb4f704e16eb866..e1cb6e6a76f901ee553413d435145dde4ca2722d 100755
--- a/bin/lint.sh
+++ b/bin/lint.sh
@@ -1,4 +1,26 @@
#!/bin/sh
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
set -e
# --------------------------------------------------------------------------
diff --git a/bin/merge-master.sh b/bin/merge-master.sh
index 5664dbaeb74bd486648594e7817332a9d3e27f15..28ae15023e585ccbe7228f98f8f563eb106403ea 100755
--- a/bin/merge-master.sh
+++ b/bin/merge-master.sh
@@ -1,4 +1,25 @@
#!/bin/sh
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
if test -z "$1"; then
echo "Syntax: $0 <release name>";
diff --git a/bin/migration_scripts/git-replace.sh b/bin/migration_scripts/git-replace.sh
index d32b5d6bb15c50f59e013b9479ba0d06837bebe8..cf96d73698372ae449f7e54b85954ab29aa3dabd 100755
--- a/bin/migration_scripts/git-replace.sh
+++ b/bin/migration_scripts/git-replace.sh
@@ -1,4 +1,26 @@
#!/bin/sh -u
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
git replace fbe13264f29d59b5388096281f98f05116b17f76 8e6afe71d01b1bc4f4d778a5326d0a2e1f2998b3
git replace cef5bf08946dccaf6b51e515eea76443976e6550 8bd30e2d47ffab72507d5ea291bdbd9f0fea0384
git replace 32d8c505805a060e5112c104ea0ffe06c6df308d 3fb543f7adaac4c2942c45f0244f270c86c23605
diff --git a/bin/rebuild.sh b/bin/rebuild.sh
index f8d3346fab80481cfd8a6eaa73f3f1d92765a6eb..f50cecdb02c21de5dcabda7ec3df1ad1655cabe2 100755
--- a/bin/rebuild.sh
+++ b/bin/rebuild.sh
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
make -k clean
find src \( -name "*.cm*" -or -name "*.o" \) -delete -print
rm -fr config.status autom4te.cache/
diff --git a/bin/shift_oracles.sh b/bin/shift_oracles.sh
index 1a8cba4f5da6526ab0a05fd6050b8ac3afb0efc9..0b9ea6cd135d8506fcfe381021c58bd616db2051 100755
--- a/bin/shift_oracles.sh
+++ b/bin/shift_oracles.sh
@@ -1,4 +1,25 @@
#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# [shift_oracles.sh [commit] source.c -- test1.oracle test2.oracle ...]
# modifies the set of oracles w.r.t. [source.c], using `git diff` to
diff --git a/bin/update_api_doc.sh b/bin/update_api_doc.sh
index 80313ff753fa109745439f24d9dd21e856834089..9601c2544f152459bbfb8af60514b3a2bb8c489a 100755
--- a/bin/update_api_doc.sh
+++ b/bin/update_api_doc.sh
@@ -1,4 +1,25 @@
#!/bin/sh
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
next=$1
diff --git a/bin/wp-qualif.sh b/bin/wp-qualif.sh
index ae239fbadbe2bcd440bac1a4cd149dcc391e1d13..418cabf7b371c8ac91a44196bdcf23d68fab7af3 100644
--- a/bin/wp-qualif.sh
+++ b/bin/wp-qualif.sh
@@ -1,2 +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). #
+# #
+##########################################################################
+
export FRAMAC_WP_CACHE=update
export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile
index 04d1c97261bf1c50ddebd680e3f9f7458ddffaca..c6cae592a0f241287c37ea2fba3a5c897463c8ff 100644
--- a/devel_tools/docker/Makefile
+++ b/devel_tools/docker/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
.PHONY: *-stripped *-gui push-*
help:
diff --git a/devel_tools/duplicates.pl b/devel_tools/duplicates.pl
index ba91fcccfdd869819e6ed19491723f03f9af9cfa..019ac1e21d113b188e988f92d3aedecaa287521b 100755
--- a/devel_tools/duplicates.pl
+++ b/devel_tools/duplicates.pl
@@ -1,4 +1,25 @@
#!/usr/bin/env perl
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# Finds duplicate adjacent words.
diff --git a/devel_tools/frama-c-callgrind b/devel_tools/frama-c-callgrind
deleted file mode 100755
index 3e23c01dbd87bf413615791fa3681d2bb16cab40..0000000000000000000000000000000000000000
--- a/devel_tools/frama-c-callgrind
+++ /dev/null
@@ -1,31 +0,0 @@
-#!/bin/bash
-
-# Script for profiling Frama-C with callgrind (a valgrind tool).
-# Note: execution time with valgrind is about 15x-20x slower.
-#
-# Use this script at the root of the repository, so local_export.sh can be found
-# in bin.
-# For more focused results, you can activate the profiling only after entering
-# a specific function. For instance, to only profile Eva, add
-#
-# --toggle-collect='*Eva__Analysis__force_compute*'
-#
-# to the command line below.
-#
-# Example of invocation :
-#
-# devel_tools/frama-c-callgrind tests/idct/*.c -eva -float-normal -no-warn-signed-overflow
-#
-# This creates a 'callgrind.out' file (Callgrind format), which can be viewed
-# with a tool such as kcachegrind:
-#
-# kcachegrind callgrind.out
-
-BASH_ARGV0="bin/frama-c" # hackish way to tell local_export that its dir is bin
-
-. bin/local_export.sh
-
-valgrind \
- --tool=callgrind --callgrind-out-file=callgrind.out --dump-instr=yes \
- --separate-callers=2 --collect-jumps=yes --fn-skip='caml_*' \
- $BINDIR/toplevel.opt "$@"
diff --git a/devel_tools/frama-c-callgrind.sh b/devel_tools/frama-c-callgrind.sh
new file mode 100755
index 0000000000000000000000000000000000000000..1de367e65fed348a0bc008856f2979d3d31f5ab0
--- /dev/null
+++ b/devel_tools/frama-c-callgrind.sh
@@ -0,0 +1,52 @@
+#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
+# Script for profiling Frama-C with callgrind (a valgrind tool).
+# Note: execution time with valgrind is about 15x-20x slower.
+#
+# Use this script at the root of the repository, so local_export.sh can be found
+# in bin.
+# For more focused results, you can activate the profiling only after entering
+# a specific function. For instance, to only profile Eva, add
+#
+# --toggle-collect='*Eva__Analysis__force_compute*'
+#
+# to the command line below.
+#
+# Example of invocation :
+#
+# devel_tools/frama-c-callgrind tests/idct/*.c -eva -float-normal -no-warn-signed-overflow
+#
+# This creates a 'callgrind.out' file (Callgrind format), which can be viewed
+# with a tool such as kcachegrind:
+#
+# kcachegrind callgrind.out
+
+BASH_ARGV0="bin/frama-c" # hackish way to tell local_export that its dir is bin
+
+. bin/local_export.sh
+
+valgrind \
+ --tool=callgrind --callgrind-out-file=callgrind.out --dump-instr=yes \
+ --separate-callers=2 --collect-jumps=yes --fn-skip='caml_*' \
+ $BINDIR/toplevel.opt "$@"
diff --git a/devel_tools/git-hooks/pre-commit b/devel_tools/git-hooks/pre-commit
index fec935b5fc0ca5d771f4b43bbd2a137789f76287..36353a8d1a7c53153e9482ef9e40fc4510f1f3cf 100755
--- a/devel_tools/git-hooks/pre-commit
+++ b/devel_tools/git-hooks/pre-commit
@@ -1,6 +1,26 @@
#!/bin/bash
-
# -*- mode: bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
if git rev-parse --verify HEAD >/dev/null 2>&1
then
diff --git a/devel_tools/ocamldep_transitive_closure.ml b/devel_tools/ocamldep_transitive_closure.ml
index 9f7e383573055866bf377d20dd4fd2aaccb0fb92..363d14205bb5a6ff0829e739abfe61e7015a2429 100644
--- a/devel_tools/ocamldep_transitive_closure.ml
+++ b/devel_tools/ocamldep_transitive_closure.ml
@@ -1,3 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
let depend_files = ref []
let add_deps s = depend_files:= s :: !depend_files
diff --git a/devel_tools/size.mli b/devel_tools/size.mli
index 1146e6da562d9c897324a476d9d9b1f19d08b820..037d5b4a707c50988c444da0c7179ff193cc5a3a 100644
--- a/devel_tools/size.mli
+++ b/devel_tools/size.mli
@@ -4,13 +4,16 @@
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
-(* License version 2, with the special exception on linking *)
+(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
+(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
+(* énergies alternatives). *)
+(* *)
(**************************************************************************)
(*i $Id: size.mli,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*)
diff --git a/doc/aorai/Makefile b/doc/aorai/Makefile
index 515b0938ec06b9de1bd34f5ad8c4e9f97b161cca..750c6c23f14ea14be2145c360c8613e03c85f89c 100644
--- a/doc/aorai/Makefile
+++ b/doc/aorai/Makefile
@@ -1,3 +1,28 @@
+##########################################################################
+# #
+# This file is part of Aorai plug-in of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# INRIA (Institut National de Recherche en Informatique et en #
+# Automatique) #
+# INSA (Institut National des Sciences Appliquees) #
+# #
+# 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). #
+# #
+##########################################################################
+
.PHONY: all clean
DWNLDDIR=../manuals
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index eb5f0c6b5a53b6139548bf6d9ca0565bf0d57c2d..80c5b48ec69a2e9504a09bdda30be81a32f50d47 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -2,12 +2,21 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2021 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
# #
##########################################################################
diff --git a/doc/developer/Makefile.config b/doc/developer/Makefile.config
index 3554aba0cc6eb7bbd749f8060ca8c2c9d60a53a2..54e28963937a89d7a9fb1bc3f76bedadbd78417c 100644
--- a/doc/developer/Makefile.config
+++ b/doc/developer/Makefile.config
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
MAKECONFIG_DIR=../../share
include $(MAKECONFIG_DIR)/Makefile.common
MAKEPDF ?= latexmk -pdf -quiet
diff --git a/doc/developer/check_api/Makefile b/doc/developer/check_api/Makefile
index e2219705a5916e3457881ef319d1a7be13d26059..ac8885a77293456c23af39bb71fcfd03a516cbf9 100644
--- a/doc/developer/check_api/Makefile
+++ b/doc/developer/check_api/Makefile
@@ -2,12 +2,21 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2021 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
# #
##########################################################################
diff --git a/doc/developer/check_api/check_index_grammar.mly b/doc/developer/check_api/check_index_grammar.mly
index 3db1a867b460006aeba5f6b15d8e91ae5b59c960..26b5b76ac8f08841cbc98cd63664b34fd675213b 100644
--- a/doc/developer/check_api/check_index_grammar.mly
+++ b/doc/developer/check_api/check_index_grammar.mly
@@ -2,12 +2,21 @@
/* */
/* This file is part of Frama-C. */
/* */
-/* Copyright (C) 2007-2021 */
+/* Copyright (C) 2007-2022 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
-/* All rights reserved. */
-/* Contact CEA LIST for licensing. */
+/* 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). */
/* */
/**************************************************************************/
diff --git a/doc/developer/hello_world/Makefile b/doc/developer/hello_world/Makefile
index 47732363b835d3e3e579a6d5227467d31b4f2377..8da55444dd6af8bc17c26bab7a8864a18dd8e11f 100644
--- a/doc/developer/hello_world/Makefile
+++ b/doc/developer/hello_world/Makefile
@@ -2,12 +2,21 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2020 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
# #
##########################################################################
diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile
index cdeaa65fbabc6fdcbcd072b58387dd47bd62029c..97d6a65afab8dbba4c43b9e0db587fcd5d842fd8 100644
--- a/doc/developer/tutorial/hello/Makefile
+++ b/doc/developer/tutorial/hello/Makefile
@@ -2,12 +2,21 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2021 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
# #
##########################################################################
diff --git a/doc/developer/tutorial/hello/src/Makefile.multiple-files b/doc/developer/tutorial/hello/src/Makefile.multiple-files
index 4e97b5ed2dddd86b660daadfbd6a5dd9c70232b4..0a63c0353f0e895d0bd27db61c9d2599f4e53dd8 100644
--- a/doc/developer/tutorial/hello/src/Makefile.multiple-files
+++ b/doc/developer/tutorial/hello/src/Makefile.multiple-files
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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 := $(shell frama-c-config -print-share-path)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_options hello_print hello_run
diff --git a/doc/developer/tutorial/hello/src/Makefile.single-file b/doc/developer/tutorial/hello/src/Makefile.single-file
index 9b1b558bcba37d7831e1fee860903bef0e7bef1d..b99d50a1dce2c0cd3b11a5bb15f5b87821b6b52f 100644
--- a/doc/developer/tutorial/hello/src/Makefile.single-file
+++ b/doc/developer/tutorial/hello/src/Makefile.single-file
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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 := $(shell frama-c-config -print-share-path)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_world
diff --git a/doc/developer/tutorial/hello/src/Makefile.test b/doc/developer/tutorial/hello/src/Makefile.test
index 2ab6fb6a70cbd4d1e697ebe0d65248dddc3028ab..7ff38b3f00bd36c277dd4f889afb323b8ceeec55 100644
--- a/doc/developer/tutorial/hello/src/Makefile.test
+++ b/doc/developer/tutorial/hello/src/Makefile.test
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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 := $(shell frama-c-config -print-share-path)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_options hello_print hello_run
diff --git a/doc/developer/tutorial/viewcfg/Makefile b/doc/developer/tutorial/viewcfg/Makefile
index a143ee77a73cdb3b65f71e5c0323664f7444f931..67918576782a6915848671cabc6c6808eebba8d5 100644
--- a/doc/developer/tutorial/viewcfg/Makefile
+++ b/doc/developer/tutorial/viewcfg/Makefile
@@ -2,12 +2,21 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2021 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
# #
##########################################################################
diff --git a/doc/developer/tutorial/viewcfg/src/Makefile.split b/doc/developer/tutorial/viewcfg/src/Makefile.split
index ee56b8cad49061542f416bac73f901bb8ce4c325..fc1aebbdf00c7a55a6339fa0514f2b87a62c8e5e 100644
--- a/doc/developer/tutorial/viewcfg/src/Makefile.split
+++ b/doc/developer/tutorial/viewcfg/src/Makefile.split
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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 := $(shell frama-c-config -print-share-path)
PLUGIN_NAME = ViewCfg
PLUGIN_CMO = cfg_options cfg_core cfg_register
diff --git a/doc/hevea.css b/doc/hevea.css
index c549e52ced4e470e2dc4385c745aa71969e2f95b..fe81db6e64960b94032e68a422f3f16176b4a649 100644
--- a/doc/hevea.css
+++ b/doc/hevea.css
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
html{
background: darkgrey;
padding: 24px;
diff --git a/doc/metrics/Makefile b/doc/metrics/Makefile
index cf7cd6b60d7c1453e281bc04785fe05a439d2de6..e998a3da92f4dcf793ed28aba1ad6f50b38d49fb 100644
--- a/doc/metrics/Makefile
+++ b/doc/metrics/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
.PHONY: default all clean
TARGET = metrics.pdf
diff --git a/doc/pandoc/style.css b/doc/pandoc/style.css
index f32fd1e16621cfeb8f7367a3d83a1bf29570181b..18398ee443a0dce7d08bfcafeca107288b2b1423 100644
--- a/doc/pandoc/style.css
+++ b/doc/pandoc/style.css
@@ -2,7 +2,7 @@
/* */
/* This file is part of Frama-C. */
/* */
-/* Copyright (C) 2007-2021 */
+/* Copyright (C) 2007-2022 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/doc/pdg/Makefile b/doc/pdg/Makefile
index de8bc6307421bec04bd8fab929978e1191a8f78e..74b8af4e70b48417b982ac3781490c8ccad5418e 100644
--- a/doc/pdg/Makefile
+++ b/doc/pdg/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
.PHONY: all clean
all: main.pdf
diff --git a/doc/release/Makefile b/doc/release/Makefile
index 0c698b87a884f92a6cbfceb457a287f2f690fd7e..7797c93e029f967707f40d3cf89fe92f858326de 100644
--- a/doc/release/Makefile
+++ b/doc/release/Makefile
@@ -2,12 +2,21 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2021 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# 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). #
# #
##########################################################################
diff --git a/doc/rte/Makefile b/doc/rte/Makefile
index c3d71f538c537d4c9ccc072d7786205621c94034..2c6a25c25ee9686ed17cc8c56dee151223019b2b 100644
--- a/doc/rte/Makefile
+++ b/doc/rte/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
.PHONY: all clean
all: main.pdf
diff --git a/doc/scope/Makefile b/doc/scope/Makefile
index 3e14c50237d6411697cad872bdff9a1878a9c1a5..ac55e30f1991ffdb38612fdfcb1ee248d6e01ce8 100644
--- a/doc/scope/Makefile
+++ b/doc/scope/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
#vide : pour ne pas utiliser de règles implicites
.SUFFIXE:
.PHONY: clean all debug
diff --git a/doc/slicing/Makefile b/doc/slicing/Makefile
index b09932ac72db4cf6512927e70d60debfe827927c..673e0ac1c9ae83a3294e668d0c6c00c92a20a7f6 100644
--- a/doc/slicing/Makefile
+++ b/doc/slicing/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
.PHONY: all clean
all: main.pdf
diff --git a/doc/userman/Makefile b/doc/userman/Makefile
index 433971360454eaafc0c43dccfe11c4a15f044b5e..0b98372bc4d1250d4113ea4827edf80d636b4edf 100644
--- a/doc/userman/Makefile
+++ b/doc/userman/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# Require texi2pdf
.DEFAULT_GOAL := all
diff --git a/doc/userman/Makefile.config b/doc/userman/Makefile.config
index b1c187535803f92702c052d5b49f58f212ccfeca..7008f1df9dfda02882dd2d8e8043989cb6d11b57 100644
--- a/doc/userman/Makefile.config
+++ b/doc/userman/Makefile.config
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
MAKECONFIG_DIR=../../share
include ../../share/Makefile.common
FRAMAC_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' ../../VERSION)
diff --git a/headers/check-headers.sh b/headers/check-headers.sh
deleted file mode 100755
index 6846de19e9ba7363bba0b0b10a0f671bd7faabcb..0000000000000000000000000000000000000000
--- a/headers/check-headers.sh
+++ /dev/null
@@ -1,265 +0,0 @@
-#!/bin/sh
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2022 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
-# #
-##########################################################################
-
-
-APPLINAME="$0"
-echo $0 $@
-Usage() {
- APPLI=$(basename $APPLINAME)
- echo "Usage: $APPLI <options> <files>"
- echo " $APPLI [--update] --spec-files <spec-files>"
- echo " 1. Checks entries of <spec-files>"
- echo " --update: updates <spec-files> by removing comments and multiple entries"
- echo " $APPLI [--update] [--no-headers <header-file>]* <spec-file> ([--files-from] <file>]*"
- echo " 1. Checks entries of <spec-file>"
- echo " --update: updates <spec-file> by removing comments and multiple entries"
- echo " 2. Checks that every <files> have an entry into the <spec-file>"
- echo " 3. Checks that all the <files> are not attributed to <header-file> in <spec-file>"
- echo " --no-headers <header-file>: cumulative option"
- exit 0
-}
-
-Requires () {
- for File in "$@"
- do
- where=$(which $File)
- if [ "$?" != "0" ] ; then
- echo "Error: executable not found: $File"
- exit 1
- fi
- done
-}
-
-RegExp=""
-Checking () {
-
- Requires sort tr grep diff sed
-
- if [ "$SpecFilesOpt" != "" ] && [ "$HeadersOpt" != "" ] ; then
- echo "Error: given options are exclusives"
- exit 1
- fi
-
- if [ "$1" = "" ] ; then
- echo "Error: missing argument"
- exit 1
- fi
-
- if [ ! -f "$1" ] ; then
- echo "Error: file not found: $file"
- exit 1
- fi
-
- if [ "$SpecFilesOpt" != "" ] ; then
- shift
- for file in $@ ; do
- if [ "$file" != "--files-from" ] && [ ! -f $file ] ; then
- echo "Error: file not found: $file"
- exit 1
- fi
- done
- fi
-
- if [ "$HeadersOpt" != "" ] ; then
- RegExp="("
- for file in $HeadersOpt ; do
- SyntaxOk=$(echo "$file" | tr -d "._[:alnum:]")
- if [ "$SyntaxOk" != "" ] ; then
- echo "Error: invalid header filename: $file"
- exit 1
- fi
- if [ "$RegExp" != "(" ] ; then
- RegExp="${RegExp}|"
- fi
- RegExp="${RegExp}$(echo $file | sed -e 's:\.:\\.:')"
- done
- RegExp="^${RegExp}):"
- fi
-}
-
-Result="0"
-Check () {
- Warn=""
- cat $1 \
- | tr "[:blank:]" " " \
- | sed -e 's: *: :g' \
- | sed -e 's:^ ::g' \
- | sed -e 's: $::g' \
- | sed -e 's/ :/:/g' \
- | sed -e 's/:\([^ ]\)/: \1/g' \
- > $1.$$
- TMP1=$1.$$
- if [ "$?" != "0" ] && [ "$2" = "-step-1" ] ; then
- echo " Warning: some blank characters can be cleaned:"
- diff $1 $TMP1 | grep "^> "
- Warn="Ok"
- fi
- grep -v "^#" $TMP1 > ${TMP1}.$$
- TMP2=${TMP1}.$$
- LC_ALL=C sort -k2 -k1 $TMP2 > $TMP1
- diff -q $TMP1 $TMP2 > /dev/null
- if [ "$?" != "0" ] && [ "$2" = "-step-1" ] ; then
- echo " Warning: some entries are unsorted:"
- diff $TMP1 $TMP2 | grep "^> "
- Warn="Ok"
- fi
- LC_ALL=C sort -u -k2 -k1 $TMP1 > $TMP2
- diff -q $TMP2 $TMP1 > /dev/null
- if [ "$?" != "0" ] ; then
- if [ "$2" = "-step-1" ] ; then
- echo " Warning: some entries are duplicated:"
- else
- echo " Warning: the following given files are duplicated:"
- fi
- diff $TMP2 $TMP1 | sed -n -e "s/^> ~no-entry-for:/ /p"
- Warn="Ok"
- fi
- LC_ALL=C sort -u -k2 $TMP2 > $TMP1
- if [ "$3" != "" ] ; then
- diff $TMP1 $3 > /dev/null
- if [ "$?" != "0" ] ; then
- echo " Error: some files have no entry:"
- diff $3 $TMP1 | sed -n -e "s/^> ~no-entry-for:/ /p"
- Warn="OkOk"
- Result="1"
- fi
- else
- diff -q $TMP1 $TMP2 > /dev/null
- if [ "$?" != "0" ] ; then
- if [ "$2" = "-step-1" ] ; then
- echo " Error: some entries are duplicated."
- echo " removed entries:"
- else
- echo " Error: some checked entries have unwanted headers:"
- fi
- diff $TMP1 $TMP2 | grep "^> "
- Warn="OkOk"
- Result="1"
- fi
- fi
-}
-
-CheckSpecFile () {
- echo " Checking specification file $1..."
- Check "$1" "-step-1"
- if [ "$Warn" = "OkOk" ] ; then
- if [ "$UpdateOpt" != "--update" ] ; then
- rm $TMP1 $TMP2
- echo " Use --update option to update $1 file"
- exit 1
- fi
- fi
- if [ "$UpdateOpt" = "--update" ] ; then
- if [ "$Warn" = "" ] ; then
- diff -q $TMP1 $1 > /dev/null
- if [ "$?" != "0" ] ; then
- Warn="Ok"
- fi
- fi
- if [ "$Warn" = "" ] ; then
- echo "Warning: already up to date"
- else
- echo " Updating file $1"
- mv $TMP1 $1
- fi
- fi
-}
-
-UpdateOpt=""
-HeadersOpt=""
-SpecFilesOpt=""
-while [ "$1" != "" ] ; do
- case "$1" in
- -h) Usage;;
- -help) Usage;;
- --help) Usage;;
- --update) UpdateOpt="$1";;
- --spec-files) SpecFilesOpt="$1";;
- --no-headers) shift; HeadersOpt="${Headers} $1";;
- --files-from) break;;
- --*) echo "Unknown option $1"; exit 1;;
- *) break;;
- esac
- shift
-done
-
-Checking $@
-
-BuildTmpFile() {
- TmpFile="$1"
- shift
- Str="$1"
- shift
- while [ "$1" != "" ]; do
- if [ "$1" = "--files-from" ] ; then
- shift
- cat $1 \
- | tr "[:blank:]" " " \
- | sed -e 's: *: :g' \
- | sed -e 's:^ ::g' \
- | sed -e 's: $::g' \
- | egrep -v '^#' \
- | sed -e "s#^#${Str}: #" >> $TMP
- else
- echo "${Str}: $1" >> $TMP
- fi
- shift
- done
-}
-
-if [ "$SpecFilesOpt" = "" ] ; then
-# echo "Step 1..."
- SpecFile=$1
- shift
- CheckSpecFile $SpecFile
-# echo " Removing temporary files"
- mv $TMP2 $TMP1
- RefStep2=$TMP1
-
- if [ "$1" != "" ]; then
-# echo "Step 2..."
- echo " Checking that all given files have an entry..."
- cat $RefStep2 > $RefStep2.$$
- TMP=$RefStep2.$$
- BuildTmpFile $TMP "~no-entry-for" $@
- Check $TMP "-step-2" $RefStep2
-# echo " Removing temporary files"
- rm -f $TMP $TMP1 $TMP2
- fi
- rm -f $RefStep2
-
- if [ "$RegExp" != "" ] && [ "$1" != "" ]; then
-# echo "Step 3..."
- echo " Checking for files having unwanted headers..."
- egrep -e "$RegExp" $SpecFile > $SpecFile.$$
- TMP=$SpecFile.$$
- BuildTmpFile $TMP "./looking-for" $@
- Check $TMP "-step-3"
-# echo " Removing temporary files"
- rm -f $TMP $TMP1 $TMP2
- fi
-
- if test $Result -eq 0; then
- echo "No issue detected. Great!"
- fi
- exit $Result
-
-else
-# echo "Step 1..."
- for file in $@ ; do
- CheckSpecFile $file
-# echo " Removing temporary files"
- rm -f $TMP1 $TMP2
- done
-fi
\ No newline at end of file
diff --git a/headers/close-source/ACSL_EL b/headers/close-source/CEA_PR_LGPL
similarity index 100%
rename from headers/close-source/ACSL_EL
rename to headers/close-source/CEA_PR_LGPL
diff --git a/headers/close-source/XL_COMPCERT b/headers/close-source/XL_COMPCERT
new file mode 100644
index 0000000000000000000000000000000000000000..e8e6bf9af8871ef73e2d4bafb6aaa5a9af9f2c1f
--- /dev/null
+++ b/headers/close-source/XL_COMPCERT
@@ -0,0 +1,10 @@
+ The Compcert verified compiler
+
+ Xavier Leroy, INRIA Paris-Rocquencourt
+
+ Copyright Institut National de Recherche en Informatique et en
+ Automatique. All rights reserved. This file is distributed
+ under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 2 of the License, or
+ (at your option) any later version. This file is also distributed
+ under the terms of the INRIA Non-Commercial License Agreement.
diff --git a/headers/hdrck.ml b/headers/hdrck.ml
index 3a173a6017d284ee3fdff301ea2f54d6721c54e4..96232626de0c1bfeeeed09e770f345193fa02c73 100755
--- a/headers/hdrck.ml
+++ b/headers/hdrck.ml
@@ -1,6 +1,56 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type spec_format = Sep1Line1 (* <space>* FileName <space>* `:` <space>* HeaderId <space>* <eol> *)
+ | Sep2Line1 (* <space>* FileName <space>* `:` <space>* AttributeName <space>*`:` <space>*HeaderId <space>* <eol> *)
+ | Line3 (* FileName <eol> AttributeName <eol> HeaderId <eol> *)
+ | Zero3 (* FileName <null> AttributeName <null> HeaderId <null> *)
+(* Sep1Line1
+ > cat headers/header_spec.txt | headers/hdrck --stdin -spec-format=2-fields-by-line -header-dirs headers/open-source
+*)
+(* Sep2Line1
+ > cat headers/header_spec.txt | tr ':' '\n' | xargs -n 2 printf " %s : header_spec : %s \n" > x-3-fields-by-line.txt
+ > cat x-3-fields-by-line.txt | headers/hdrck --stdin -spec-format=3-fields-by-line -header-dirs headers/open-source
+*)
+(* Line3
+ > cat headers/header_spec.txt | tr ':' '\n' | xargs -n 2 printf "%s\nheader_spec\n%s\n" > x-3-lines.txt
+ > cat x-3-lines.txt | headers/hdrck --stdin -spec-format=3-lines -header-dirs headers/open-source
+*)
+(* Zero
+ > cat headers/header_spec.txt | tr ':' '\n' | xargs -n 2 printf "%s\nheader_spec\n%s\n" | tr '\n' '\0' > x-3-zeros.txt
+ > cat x-3-zeros.txt | headers/hdrck --stdin -z -header-dirs headers/open-source
+*)
+
+(* From the git archive
+ > git ls-files -z | git check-attr --stdin -z header_spec \
+ | headers/hdrck --stdin -z -header-dirs headers/open-source -header-dirs src/plugins/e-acsl/headers/open-source
+*)
+
(* Parameters settable from command line *)
let debug_flag = ref false
and spec_files = ref []
+and from_stdin = ref false
+and zero_stdin = ref false
+and spec_format = ref Sep1Line1
and header_dirs = ref []
and forbidden_headers = ref []
and root_dir = ref (Sys.getcwd ())
@@ -8,7 +58,8 @@ and distrib_file = ref None
and header_except_file = ref None
and headache_config_file = ref "headers/headache_config.txt"
and exit_on_warning = ref false
-and exit_on_error = ref true (* only set to false for debugging purposes *)
+and exit_on_error = ref true (* only settable to false for debugging purposes *)
+
type mode =
| Check
@@ -96,18 +147,27 @@ let get_tmp_dirname () = match !tmp_dirname with
dirname
| Some dirname -> dirname
+let get_string_null (ic:in_channel) =
+ let rec aux acc =
+ let c = input_char ic in
+ if c <> '\000' then aux (c :: acc) else acc
+ in
+ let tab = Array.of_list (List.rev (aux [])) in
+ String.init (Array.length tab) (Array.get tab)
+
+
(* Reads [nlines] lines of a file named [filename].
*
* Defaults to reading the file entirely since any integer will ever be greater
* or equal than [max_int].
*)
-let read_lines ?nlines:(nlines=max_int) filename =
+let read_lines ?nlines:(nlines=max_int) get_line filename =
let lines = ref [] in
- let ic = open_in filename in
+ let ic = if filename = "--stdin" then stdin else open_in filename in
let n = ref 1 in
try
while !n <= nlines do
- lines := input_line ic :: !lines;
+ lines := get_line ic :: !lines;
incr n
done;
close_in ic;
@@ -123,7 +183,10 @@ let extract_sub_dir filename =
| sub_dir :: _ :: _ -> sub_dir
| _ -> ""
-let colon_reg_exp = Str.regexp ":"
+let split_line_entry =
+ let colon_reg_exp = Str.regexp ":" in
+ fun (line:string) ->
+ List.map String.trim (Str.split colon_reg_exp line)
module StringSet = struct
include Set.Make(struct type t = string let compare = String.compare end)
@@ -143,68 +206,103 @@ end
@param license_name
*)
let add_spec_entry (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t)
- idx (file_name : string) (license_name: string) =
- if license_name <> ".ignore" then begin
- try
- let previous_entry = Hashtbl.find spec_tab file_name in
- if license_name <> previous_entry then
+ idx ~(file_name : string) ~(license_name: string) =
+ match license_name with
+ | ("set" | "unset" | "unspecified") ->
+ warn (* error ~exit_value:9 *)
+ "%s: invalid specification (%d) for that file (git attribute value=%s)@."
+ file_name idx license_name
+ | ".ignore" -> begin
+ try
+ let previous_entry = Hashtbl.find spec_tab file_name in
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
- file_name idx license_name previous_entry
- else if StringSet.mem file_name !ignored_files then
- error ~exit_value:6
- "%s: specification duplicated (%d) with a different license name (%s and %s)@."
- file_name idx license_name ".ignore"
- else warn "%s: specification duplicated (%d)@." file_name idx
- with Not_found -> Hashtbl.add spec_tab file_name license_name
- end
- else begin
- try
- let previous_entry = Hashtbl.find spec_tab file_name in
- error ~exit_value:6
- "%s: specification duplicated (%d) with a different license name (%s and %s)@."
- file_name idx previous_entry ".ignore"
- with Not_found ->
- if StringSet.mem file_name !ignored_files then
- warn "%s: specification duplicated (%d)@." file_name idx
- else ignored_files := StringSet.add file_name !ignored_files
- end
+ file_name idx previous_entry ".ignore"
+ with Not_found ->
+ if StringSet.mem file_name !ignored_files then
+ warn "%s: specification duplicated (%d)@." file_name idx
+ else ignored_files := StringSet.add file_name !ignored_files
+ end
+ | _ -> begin
+ try
+ let previous_entry = Hashtbl.find spec_tab file_name in
+ if license_name <> previous_entry then
+ error ~exit_value:6
+ "%s: specification duplicated (%d) with a different license name (%s and %s)@."
+ file_name idx license_name previous_entry
+ else if StringSet.mem file_name !ignored_files then
+ error ~exit_value:6
+ "%s: specification duplicated (%d) with a different license name (%s and %s)@."
+ file_name idx license_name ".ignore"
+ else warn "%s: specification duplicated (%d)@." file_name idx
+ with Not_found ->
+ if StringSet.mem file_name !ignored_files then
+ error ~exit_value:6
+ "%s: specification duplicated (%d) with a different license name (%s and %s)@."
+ file_name idx license_name ".ignore"
+ else Hashtbl.add spec_tab file_name license_name
+ end
(* Reads the contents of the specification.
- Each line of the file is assumed to contain one association of the form:
- <filename_id>\s+:\s+<license_id>
- where:
- - \s matches any whitespace character
- - identifiers can contain anything but whitespaces.
-
+ Each line of the file using the [spec_format].
Lines that do not match this pattern are ignored.
@param spec_tab (file -> license header name) hashtable to update
@param ignored_files set of ignored files to update.
*)
-let read_specs (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t) (spec_file : string) =
- debug "Specification file: %s@." spec_file;
- job_head "Checking format of specification file %s... @?" spec_file;
- let spec_lines = read_lines spec_file in
- let sub_dir = extract_sub_dir spec_file in
- List.iteri
- (fun i spec_line ->
- match Str.split colon_reg_exp spec_line with
- | filename :: [license_name] ->
- let filename = String.trim filename in
- let filename =
- if sub_dir <> "" then path_concat sub_dir filename else filename
- in
- let filename = path_concat !root_dir filename in
- let license_name = String.trim license_name in
- add_spec_entry ignored_files spec_tab i filename license_name
- | _ ->
- warn "%s (%d): bad line format@." spec_file i
- ) spec_lines;
+let read_specs spec_format (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t) (spec_file : string option) =
+ let spec_fname = match spec_file with None -> "--stdin" | Some filename -> filename in
+ debug "Specification file: %s@." spec_fname ;
+ job_head "Checking format of specification file %s... @?" spec_fname;
+ let sub_dir = extract_sub_dir spec_fname in
+ let add_spec, get_line =
+ let add_spec_item i ~file_name ~license_name =
+ let file_name =
+ if sub_dir <> "" then path_concat sub_dir file_name else file_name
+ in
+ let file_name = path_concat !root_dir file_name in
+ add_spec_entry ignored_files spec_tab i ~file_name ~license_name
+ in
+ let add_spec_Sep1Line1 spec_lines =
+ List.iteri
+ (fun i spec_line ->
+ match split_line_entry spec_line with
+ | file_name :: [license_name] ->
+ add_spec_item i ~file_name ~license_name
+ | _ -> warn "%s (%d): bad line format@." spec_fname (i+1)
+ ) spec_lines
+ and add_spec_Sep2Line1 spec_lines =
+ List.iteri
+ (fun i spec_line ->
+ Format.printf "%s@." spec_line;
+ match split_line_entry spec_line with
+ | file_name :: "header_spec" :: [license_name] ->
+ add_spec_item i ~file_name ~license_name
+ | _ :: attr :: [_] -> warn "%s (%d): bad attribute name: %s@." spec_fname (i+1) attr
+ | _ -> warn "%s (%d): bad line format@." spec_fname (i+1)
+ ) spec_lines
+ and add_spec_Sep0Line3 spec_lines =
+ let rec add_spec i = function
+ | [] -> ()
+ | file_name :: "header_spec" :: license_name :: spec_lines ->
+ add_spec_item i ~file_name ~license_name ;
+ add_spec (i+1) spec_lines
+ | _ :: attr :: _ :: _ ->
+ warn "%s (%d): (3-upplet: %d) attribute name: %s@." spec_fname ((3*i)+1) (i+1) attr
+ | _ -> warn "%s (%d): (3-upplet: %d) bad format@." spec_fname ((3*i)+1) (i+1)
+ in add_spec 0 spec_lines
+ in match spec_format with
+ | Sep1Line1 -> add_spec_Sep1Line1,input_line
+ | Sep2Line1 -> add_spec_Sep2Line1,input_line
+ | Line3 -> add_spec_Sep0Line3,input_line
+ | Zero3 -> add_spec_Sep0Line3, get_string_null
+ in
+ let spec_lines = read_lines get_line spec_fname in
+ add_spec spec_lines;
job_done ()
let coma_reg_exp = Str.regexp ","
-let set_cumulative (name:string) (value: string list ref) (set : string) =
+let set_cumulative ~(name:string) (value: string list ref) ~(set : string) =
debug "Register cumulative %s option: %s" name set;
value := List.fold_left
(fun acc v -> let v = String.trim v in if v="" then acc else v::acc)
@@ -338,7 +436,7 @@ let check_spec_discrepancies
) specs ;
if !n > 0 then begin
error ~exit_value:4 "@[<v 2>%a%d / %d files with bad headers@]@."
- (fun ppf l ->
+ (fun _ppf l ->
List.iter
(fun (file, hdr_type) ->
error_fmt "%s : header differs from spec %s@."
@@ -352,7 +450,7 @@ let check_spec_discrepancies
let check_forbidden_headers (forbidden_headers:StringSet.t) header_specifications (distributed_files:StringSet.t) =
if not (StringSet.is_empty forbidden_headers) then begin
- job_head "Checking that all distributed files have no forbidden header specification @?";
+ job_head "Checking that all distributed files have no forbidden header specification... @?";
let forbidden = ref [] in
let n = ref 0 in
StringSet.iter
@@ -365,7 +463,7 @@ let check_forbidden_headers (forbidden_headers:StringSet.t) header_specification
distributed_files;
if !forbidden <> [] then
error ~exit_value:4 "@[<v 2>%a%d / %d files with bad headers@]@."
- (fun ppf l ->
+ (fun _ppf l ->
List.iter
(fun (file, hdr_type) ->
error_fmt "%s : forbidden header %s@."
@@ -488,42 +586,59 @@ let executable_name = Sys.argv.(0)
let umsg =
Format.sprintf "Usage: %s [options] <header spec files>@.%s"
executable_name
- ("The line format of each <header spec files> is:\n" ^
- " <source file> ':' <license definition>\n" ^
+ ("The default format of each <header spec files> is \"2-fields-by-line\".\n" ^
+ "The different formats are:\n" ^
+ "- \"2-fields-by-line\" format:\n\t<space>* <source file> <space>* ':' <space>* <license definition> <space>* <eol>\n" ^
+ "- \"3-fields-by-line\" format:\n\t<space>* <source file> <space>* ':' <space>* 'header_spec' <space>* ':' <space>* <license definition> <space>* <eol>\n" ^
+ "- \"3-lines\" format:\n\t<source file> <eol> 'header_spec' <eol> <license definition> <eol>\n" ^
+ "- \"3-zeros\" format:\n\t<source file> <zero> 'header_spec' <zero> <license definition> <zero>\n" ^
"where <license definition> is '.ignore' or a license definition file.\n" ^
"The location directory of the license definitions can be specified using the -header-dirs option.\n" ^
- "When the name of a <header spec file> has the form 'path/./header-spec-file',\n"^
- "then the <source file> names that it contains\n" ^
+ "When the name of a <header spec file> has the form 'path/./header-spec-file', "^
+ "then the <source file> names that it contains " ^
"are considered beeing relative to given 'path'.\n" ^
- "That is done before processing the option '-C <dir>'." )
+ "That is done before processing the option '-C <dir>'.'\n" ^
+ "List of the options:")
let rec argspec = [
"--help", Arg.Unit print_usage ,
" print this option list and exits";
+ "--stdin", Arg.Set from_stdin,
+ " extract an header spec from the standard input in addition to the given header spec files";
"-help", Arg.Unit print_usage ,
" print this option list and exits";
"-debug", Arg.Set debug_flag,
" enable debug messages";
- "-forbidden-headers", Arg.String (set_cumulative "-forbidden-headers" forbidden_headers) ,
- " none of the distributed files may have one of these license name";
- "-header-dirs", Arg.String (set_cumulative "-header-dirs" header_dirs),
- " add comma separated list of directories to search for license header definitions [.]";
+
+ "-forbidden-headers", Arg.String (fun set -> set_cumulative ~name:"-forbidden-headers" forbidden_headers ~set) ,
+ "<license name>,... \t none of the checked files may have one of the <license name> []";
+ "-header-dirs", Arg.String (fun set -> set_cumulative ~name:"-header-dirs" header_dirs ~set),
+ "<directory>,... \t list of <directory> to search for license header definitions []";
"-distrib-file", Arg.String (set_opt distrib_file),
- " set filename with a list of files set for distribution";
+ "<filename> \t considers only the files listed into the <filename>";
"-header-except-file", Arg.String (set_opt header_except_file),
- " set filename with a list of files whose headers do not need checking";
+ "<filename> \t does not look at the files listed into the <filename>";
"-headache-config-file", Arg.Set_string headache_config_file,
- Format.sprintf " set headache configuration file [%s]" !headache_config_file;
+ Format.sprintf "<filename> \t set headache configuration file [%s]" !headache_config_file;
"-no-exit-on-error", Arg.Unit (fun () -> exit_on_error := false),
- " do not exit on errors ";
+ " does not exit on errors ";
"-exit-on-warning", Arg.Set exit_on_warning,
" considers warnings as errors (anyway, forces exit on errors too)";
"-update", Arg.Unit (fun () -> mode := Update),
- " update headers w.r.t to the <header spec file>";
+ " updates headers w.r.t to the <header spec file>";
"-C", Arg.Set_string root_dir,
Format.sprintf
- " prepend <dir> to filenames in header specification [%s] "
+ "<dir> \t prepends <dir> to filenames in header specification [%s] "
!root_dir;
+ "-spec-format", Arg.String (function
+ | "2-fields-by-line" -> spec_format := Sep1Line1
+ | "3-fields-by-line" -> spec_format := Sep2Line1
+ | "3-lines" -> spec_format := Line3
+ | "3-zeros" -> spec_format := Zero3
+ | s -> Format.printf "invalid spec format: %s@." s ; print_usage ()),
+ "<format>\t \"2-fields-by-line\"|\"3-fields-by-line\"|\"3-lines\"|\"3-zeros\"";
+ "-z", Arg.Set zero_stdin,
+ " force to use the spec format \"3-zeros\" when reading from stdin";
]
and sort argspec =
@@ -545,25 +660,28 @@ let _ =
check_headache_config_file ();
begin
match !spec_files, !distrib_file, !header_except_file with
- | [], _, _ ->
+ | [], _, _ when not !from_stdin ->
Format.printf "Please set a specification file@\n@.";
print_usage ();
| spec_files, distrib_file_opt, header_except_opt ->
let specified_files = Hashtbl.create 256 in
let ignored_files = ref StringSet.empty in
- List.iter (read_specs ignored_files specified_files) spec_files;
+ if !from_stdin then read_specs (if !zero_stdin then Zero3 else !spec_format) ignored_files specified_files None;
+ List.iter (fun f -> read_specs !spec_format ignored_files specified_files (Some f)) spec_files;
+ Format.printf "- ignored=%d@.- specified=%d@." (StringSet.cardinal !ignored_files) (Hashtbl.length specified_files);
match !mode with
| Check ->
let stringset_from_opt_file = function
| None -> StringSet.empty
| Some file ->
- let lines = read_lines file in
+ let lines = read_lines input_line file in
List.fold_left
(fun s l -> StringSet.add (path_concat !root_dir l) s)
StringSet.empty lines
in
let distributed_files = stringset_from_opt_file distrib_file_opt in
let header_exception_files = stringset_from_opt_file header_except_opt in
+ Format.printf "- excepted=%d@.- distributed=%d@." (StringSet.cardinal header_exception_files) (StringSet.cardinal distributed_files);
check !ignored_files specified_files distributed_files header_exception_files
| Update ->
update_headers specified_files;
diff --git a/headers/headache.sh b/headers/headache.sh
deleted file mode 100755
index 2eb900248cf06073b1f17e19616f80ca800e393e..0000000000000000000000000000000000000000
--- a/headers/headache.sh
+++ /dev/null
@@ -1,55 +0,0 @@
-#!/bin/sh
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2022 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
-# #
-##########################################################################
-
-
-APPLINAME="$0"
-Usage() {
- APPLI=$(basename $APPLINAME)
- echo "Usage: $APPLI -c <headache-config> -h <header-file> <file>"
- echo " Runs headache with the same arguments when <file> exists"
- exit 1
-}
-
- Requires () {
-# Looking for executables
- for File in "$@" ; do
- where=$(which $File)
- if [ "$?" != "0" ] ; then
- echo "Error: executable not found: $File"
- exit 1
- fi
- done
-}
-
-Error() {
- echo "Error: $@"
- exit 1
-}
-
-CheckingVariables () {
- ([ "$1" = "--help" ] || [ "$1" = "-help" ] || [ "$1" = "-h" ]) && Usage
- [ "$6" != "" ] && Error "too much arguments"
- [ "$5" = "" ] && Error "too few arguments: $@"
- [ "$1" != "-c" ] && Error "missing -c as first option"
- [ ! -f "$2" ] && Error "config file not found $2"
- [ "$3" != "-h" ] && Error "missing -h as second option"
- [ ! -f "$4" ] && Error "header file not found $5"
-}
-
-Requires headache
-CheckingVariables $@
-
-if [ -f "$5" ]; then
- headache $@
-fi
diff --git a/headers/headache_config.txt b/headers/headache_config.txt
index 8ca8829fd006a1e0d5bb98d7625dd86a90bb807f..b49598cd666657116586a3a7d7ba105063c9798a 100644
--- a/headers/headache_config.txt
+++ b/headers/headache_config.txt
@@ -1,3 +1,32 @@
+##########################################################################
+# #
+# 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: the skip directive requires a filename starting by ".*"
+
+#############
+# This file #
+#############
+| "headache_config.txt" -> frame open:"#" line:"#" close:"#"
+
##################
# Objective Caml #
##################
@@ -27,13 +56,13 @@
############
# Makefile #
############
+| ".*makefile.*" -> frame open:"#" line:"#" close:"#"
| ".*Make.*" -> frame open:"#" line:"#" close:"#"
| ".*\.mk" -> frame open:"#" line:"#" close:"#"
#################
# Shell scripts #
#################
-#note: the skip directive requires a filename starting by ".*" ???
| "autocomplete_frama-c" -> frame open: "#" line: "#" close: "#"
| "_frama-c" -> frame open: "#" line: "#" close: "#"
| ".*_frama-c" -> skip match:"#compdef.*"
@@ -58,12 +87,29 @@
| "frama-c.debug" -> frame open:"#" line:"#" close:"#"
| ".*frama-c.debug" -> skip match:"#!.*"
+#############
+# Git hooks #
+#############
+| "pre-commit" -> frame open:"#" line:"#" close:"#"
+| ".*pre-commit" -> skip multiline_match: "#!.*" multiline_match: "# -\*-.*"
+
+###############
+# Zsh scripts #
+###############
+| ".*\.zsh" -> frame open:"#" line:"#" close:"#"
+| ".*\.zsh" -> skip match:"#compdef .*"
+| "_frama-c" -> frame open:"#" line:"#" close:"#"
+| ".*_frama-c" -> skip match:"#compdef .*"
+
################
# Perl scripts #
################
| ".*\.perl" -> frame open:"#" line:"#" close:"#"
+| ".*\.perl" -> skip match:"#!.*"
| "flamegraph.pl" -> frame open:"#" line:"#" close:"#"
| ".*flamegraph.pl" -> skip match:"#!.*"
+| "duplicates.pl" -> frame open:"#" line:"#" close:"#"
+| ".*duplicates.pl" -> skip match:"#!.*"
#########################
# MS-Windows Resources #
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index e635e42c3a12a14c3fd985f486d40ecff5b48673..dc4e4537811af57290bad456a08eb235c871ad0a 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -15,7 +15,7 @@ README.md: .ignore
VERSION: .ignore
VERSION_CODENAME: .ignore
bin/.gitignore: .ignore
-bin/build-src-distrib.sh: .ignore
+bin/build-src-distrib.sh: CEA_LGPL
bin/frama-c: CEA_LGPL
bin/frama-c-config: CEA_LGPL
bin/frama-c-script: CEA_LGPL
@@ -66,13 +66,12 @@ doc/code/intro_sparecode.txt: CEA_LGPL
doc/code/style.css: CEA_LGPL
doc/code/toc_head.htm: CEA_LGPL
doc/code/toc_tail.htm: CEA_LGPL
-headers/check-headers.sh: CEA_PROPRIETARY
-headers/close-source/ACSL_EL: .ignore
headers/close-source/AORAI_LGPL: .ignore
headers/close-source/CEA_INRIA_LGPL: .ignore
headers/close-source/CEA_LGPL: .ignore
headers/close-source/CEA_LGPL_OR_PROPRIETARY: .ignore
headers/close-source/CEA_PROPRIETARY: .ignore
+headers/close-source/CEA_PR_LGPL: .ignore
headers/close-source/CEA_WP: .ignore
headers/close-source/CIL: .ignore
headers/close-source/INRIA_BSD: .ignore
@@ -83,15 +82,14 @@ headers/close-source/MODIFIED_OCAMLGRAPH: .ignore
headers/close-source/MODIFIED_WHY3: .ignore
headers/close-source/OCAML_STDLIB: .ignore
headers/close-source/UNMODIFIED_WHY3: .ignore
-headers/headache.sh: CEA_PROPRIETARY
-headers/headache_config.txt: .ignore
+headers/headache_config.txt: CEA_LGPL
headers/header_spec.txt: .ignore
-headers/open-source/ACSL_EL: .ignore
headers/open-source/AORAI_LGPL: .ignore
headers/open-source/CEA_INRIA_LGPL: .ignore
headers/open-source/CEA_LGPL: .ignore
headers/open-source/CEA_LGPL_OR_PROPRIETARY: .ignore
headers/open-source/CEA_PROPRIETARY: .ignore
+headers/open-source/CEA_PR_LGPL: .ignore
headers/open-source/CEA_WP: .ignore
headers/open-source/CIL: .ignore
headers/open-source/INRIA_BSD: .ignore
@@ -102,7 +100,6 @@ headers/open-source/MODIFIED_OCAMLGRAPH: .ignore
headers/open-source/MODIFIED_WHY3: .ignore
headers/open-source/OCAML_STDLIB: .ignore
headers/open-source/UNMODIFIED_WHY3: .ignore
-headers/updates-headers.sh: CEA_PROPRIETARY
lib/plugins/PLUGINS.README: .ignore
licenses/CDDL-1.0: .ignore
licenses/LGPLv2: .ignore
@@ -118,35 +115,35 @@ share/analysis-scripts/analysis.mk: CEA_LGPL
share/analysis-scripts/benchmark_database.py: CEA_LGPL
share/analysis-scripts/build.py: CEA_LGPL
share/analysis-scripts/build_callgraph.py: CEA_LGPL
-share/analysis-scripts/clone.sh: .ignore
+share/analysis-scripts/clone.sh: CEA_LGPL
share/analysis-scripts/creduce.sh: CEA_LGPL
share/analysis-scripts/detect_recursion.py: CEA_LGPL
share/analysis-scripts/epilogue.mk: CEA_LGPL
share/analysis-scripts/estimate_difficulty.py: CEA_LGPL
-share/analysis-scripts/fc_stubs.c: .ignore
+share/analysis-scripts/fc_stubs.c: CEA_LGPL
share/analysis-scripts/frama_c_results.py: CEA_LGPL
-share/analysis-scripts/cmd-dep.sh: .ignore
-share/analysis-scripts/concat-csv.sh: .ignore
+share/analysis-scripts/cmd-dep.sh: CEA_LGPL
+share/analysis-scripts/concat-csv.sh: CEA_LGPL
share/analysis-scripts/find_fun.py: CEA_LGPL
share/analysis-scripts/flamegraph.pl: CDDL
-share/analysis-scripts/function_finder.py: .ignore
+share/analysis-scripts/function_finder.py: CEA_LGPL
share/analysis-scripts/git_utils.py: CEA_LGPL
share/analysis-scripts/heuristic_list_functions.py: CEA_LGPL
share/analysis-scripts/list_files.py: CEA_LGPL
share/analysis-scripts/list_functions.ml: CEA_LGPL
share/analysis-scripts/make_wrapper.py: CEA_LGPL
share/analysis-scripts/normalize_jcdb.py: CEA_LGPL
-share/analysis-scripts/parse-coverage.sh: .ignore
+share/analysis-scripts/parse-coverage.sh: CEA_LGPL
share/analysis-scripts/print_callgraph.py: CEA_LGPL
share/analysis-scripts/prologue.mk: CEA_LGPL
share/analysis-scripts/pyproject.toml: .ignore
share/analysis-scripts/README.md: .ignore
share/analysis-scripts/results_display.py: CEA_LGPL
-share/analysis-scripts/script_for_creduce_fatal.sh: .ignore
-share/analysis-scripts/script_for_creduce_non_fatal.sh: .ignore
+share/analysis-scripts/script_for_creduce_fatal.sh: CEA_LGPL
+share/analysis-scripts/script_for_creduce_non_fatal.sh: CEA_LGPL
share/analysis-scripts/source_filter.py: CEA_LGPL
share/analysis-scripts/summary.py: CEA_LGPL
-share/analysis-scripts/template.mk: .ignore
+share/analysis-scripts/template.mk: CEA_LGPL
share/compliance/c11_functions.json: .ignore
share/compliance/c11_headers.json: .ignore
share/compliance/compiler_builtins.json: .ignore
@@ -165,7 +162,7 @@ share/Makefile.generic: CEA_LGPL
share/Makefile.plugin.template: CEA_LGPL
share/META.frama-c: .ignore
share/configure.ac: CEA_LGPL
-share/emacs/acsl.el: ACSL_EL
+share/emacs/acsl.el: CEA_PR_LGPL
share/emacs/frama-c-dev.el: CEA_LGPL
share/emacs/frama-c-init.el: CEA_LGPL
share/emacs/frama-c-recommended.el: CEA_LGPL
@@ -987,24 +984,24 @@ src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/markdown-report/configure.ac: CEA_LGPL
-src/plugins/markdown-report/eva_info.ml: CEA_LGPL
-src/plugins/markdown-report/eva_info.mli: CEA_LGPL
-src/plugins/markdown-report/Makefile.in: CEA_LGPL
+src/plugins/markdown-report/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/eva_info.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/eva_info.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/META.in: .ignore
-src/plugins/markdown-report/md_gen.ml: CEA_LGPL
-src/plugins/markdown-report/md_gen.mli: CEA_LGPL
-src/plugins/markdown-report/mdr_params.ml: CEA_LGPL
-src/plugins/markdown-report/mdr_params.mli: CEA_LGPL
-src/plugins/markdown-report/mdr_register.ml: CEA_LGPL
-src/plugins/markdown-report/mdr_register.mli: CEA_LGPL
-src/plugins/markdown-report/parse_remarks.ml: CEA_LGPL
-src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL
-src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL
-src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL
-src/plugins/markdown-report/sarif.ml: CEA_LGPL
-src/plugins/markdown-report/sarif.mli: CEA_LGPL
-src/plugins/markdown-report/share/acsl.xml: CEA_LGPL
+src/plugins/markdown-report/md_gen.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/md_gen.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/mdr_params.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/mdr_params.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/mdr_register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/mdr_register.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/parse_remarks.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/sarif.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/sarif.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/share/acsl.xml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/Metrics.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/css_html.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/css_html.mli: CEA_LGPL_OR_PROPRIETARY
@@ -1120,13 +1117,13 @@ src/plugins/postdominators/postdominators_parameters.mli: CEA_LGPL_OR_PROPRIETAR
src/plugins/postdominators/print.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/print.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/.gitignore: .ignore
-src/plugins/print_api/Makefile: CEA_LGPL
-src/plugins/print_api/Print_api.mli: CEA_LGPL
-src/plugins/print_api/grammar.mly: CEA_LGPL
-src/plugins/print_api/lexer.mll: CEA_LGPL
-src/plugins/print_api/lexer.mli: CEA_LGPL
-src/plugins/print_api/print_interface.ml: CEA_LGPL
-src/plugins/print_api/print_interface.mli: CEA_LGPL
+src/plugins/print_api/Makefile: CEA_LGPL_OR_PROPRIETARY
+src/plugins/print_api/Print_api.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/print_api/grammar.mly: CEA_LGPL_OR_PROPRIETARY
+src/plugins/print_api/lexer.mll: CEA_LGPL_OR_PROPRIETARY
+src/plugins/print_api/lexer.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/print_api/print_interface.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/print_api/print_interface.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/qed/.gitignore: .ignore
src/plugins/qed/Makefile: CEA_WP
src/plugins/qed/bvars.ml: CEA_WP
@@ -1335,15 +1332,15 @@ src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/eval.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/eval.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gen-api.sh: .ignore
+src/plugins/value/gen-api.sh: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/self.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/self.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/test.assert.sh: .ignore
-src/plugins/value/test.sh: .ignore
+src/plugins/value/test.assert.sh: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/test.sh: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1844,14 +1841,14 @@ src/plugins/wp/ctypes.ml: CEA_WP
src/plugins/wp/ctypes.mli: CEA_WP
src/plugins/wp/filter_axioms.ml: CEA_WP
src/plugins/wp/filter_axioms.mli: CEA_WP
-src/plugins/wp/doc/MakeDoc: .ignore
-src/plugins/wp/doc/coqdoc/Makefile: .ignore
+src/plugins/wp/doc/MakeDoc: CEA_WP
+src/plugins/wp/doc/coqdoc/Makefile: CEA_WP
src/plugins/wp/doc/coqdoc/coqdoc.sty: .ignore
src/plugins/wp/doc/coqdoc/qed_generated.tex: .ignore
src/plugins/wp/doc/coqdoc/typed_generated.tex: .ignore
src/plugins/wp/doc/coqdoc/wpcoq.tex: .ignore
src/plugins/wp/doc/manual/.gitignore: .ignore
-src/plugins/wp/doc/manual/Makefile: .ignore
+src/plugins/wp/doc/manual/Makefile: CEA_WP
src/plugins/wp/doc/manual/mem.pdf: .ignore
src/plugins/wp/doc/manual/size_base.pdf: .ignore
src/plugins/wp/doc/manual/size_compl.pdf: .ignore
diff --git a/headers/open-source/ACSL_EL b/headers/open-source/CEA_PR_LGPL
similarity index 100%
rename from headers/open-source/ACSL_EL
rename to headers/open-source/CEA_PR_LGPL
diff --git a/headers/open-source/XL_COMPCERT b/headers/open-source/XL_COMPCERT
new file mode 100644
index 0000000000000000000000000000000000000000..e8e6bf9af8871ef73e2d4bafb6aaa5a9af9f2c1f
--- /dev/null
+++ b/headers/open-source/XL_COMPCERT
@@ -0,0 +1,10 @@
+ The Compcert verified compiler
+
+ Xavier Leroy, INRIA Paris-Rocquencourt
+
+ Copyright Institut National de Recherche en Informatique et en
+ Automatique. All rights reserved. This file is distributed
+ under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 2 of the License, or
+ (at your option) any later version. This file is also distributed
+ under the terms of the INRIA Non-Commercial License Agreement.
diff --git a/headers/updates-headers.sh b/headers/updates-headers.sh
deleted file mode 100755
index 9041bac49bea0bda16ac9177961ea4f53bf8e3df..0000000000000000000000000000000000000000
--- a/headers/updates-headers.sh
+++ /dev/null
@@ -1,152 +0,0 @@
-#!/bin/sh
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2022 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
-# #
-##########################################################################
-
-
-APPLINAME="$0"
-HEADACHE=$(dirname $APPLINAME)/headache.sh
-
-Usage() {
- APPLI=$(basename $APPLINAME)
- echo "Usage: $APPLI <option>* <headers-spec> <header-dir> [<target-dir>] [<headache-config>]"
- echo " <option>"
- echo " --dry-run: shows the commands to perform without any file modification"
- echo " --max-procs <N>: runs up to <N> jobs in parallel."
- echo " --parallel: uses 'parallel' software instead of 'xargs'"
- echo " <target-dir>: root pathname to the files to modify"
- echo " default to ."
- echo " <header-dir>: directory that should contents header files"
- echo " <headache-config>: headache config file"
- echo " default to ./headers"
- echo " <headers-spec>: defines header files to apply on files".
- echo " The format of <headers-spec> file is checked before doing anything."
- echo " Syntax:"
- echo " <line format>= <header-file> ':' <file-to-modify> '\n'"
- echo " | '.ignore' ':' <ignored-file> '\n'"
- echo " | '#' <comment-line> '\n'"
- echo " | [':'] '\n'"
- echo " Ignored files are not modified by the script ${APPLI}."
-
- exit 1
-}
-
-Requires () {
-# Looking for executables
- for File in "$@" ; do
- where=$(which $File)
- if [ "$?" != "0" ] ; then
- echo "Error: executable not found: $File"
- exit 1
- fi
- done
-}
-
-SetVariables() {
- FILE=$1
- HEADER_SRC=$2
- TARGET_DIR=${3-.}
- HEADACHE_CONFIG=${4-./headers/headache_config.txt}
- if [ "$5" != "" ] ; then
- echo "Error: too much arguments."
- exit 1
- fi
- if [ "${MAX_PROCS}" = "" ] && [ -f /proc/cpuinfo ] ; then
- # Linux system
- MAX_PROCS=$(cat /proc/cpuinfo | grep -c processor)
- fi
- if [ "${MAX_PROCS}" = "0" ] || [ "${MAX_PROCS}" = "" ] ; then
- MAX_PROCS=""
- else
- MAX_PROCS="-P ${MAX_PROCS}"
- fi
-}
-
-CheckingVariables () {
- if [ "${FILE}" = "" ] ; then
- echo "Error: missing header specification file."
- exit 1
- fi
- if [ ! -f "${FILE}" ] ; then
- echo "Error: header specification file not found: ${FILE}"
- exit 1
- fi
- if [ "${HEADER_SRC}" = "" ] ; then
- echo "Error: missing header directory."
- exit 1
- fi
- if [ ! -d "${HEADER_SRC}" ] ; then
- echo "Error: header directory not found: ${HEADER_SRC}/"
- exit 1
- fi
- if [ ! -d "${TARGET_DIR}" ] ; then
- echo "Error: target directory not found: ${TARGET_DIR}"
- exit 1
- fi
- if [ ! -f "${HEADACHE_CONFIG}" ] ; then
- echo "Error: headache config file not found: ${HEADACHE_CONFIG}"
- exit 1
- fi
-}
-
-PROCESS=""
-MAX_PROCS=""
-PARALLEL=""
-REQUIREMENTS="xargs"
-while [ "$1" != "" ] ; do
- case "$1" in
- -h) Usage;;
- -help) Usage;;
- --help) Usage;;
- --max-procs) shift; MAX_PROCS="$1";;
- --dry-run) PROCESS="echo";;
- --parallel) PARALLEL="parallel"; REQUIREMENTS="${PARALLEL}";;
- *) break;;
- esac
- shift
-done
-
-Requires ${HEADACHE} gawk grep tr ${REQUIREMENTS}
-
-SetVariables $@
-
-CheckingVariables
-
-# Checking the format of the input file and extract line number of the error.
-grep -v "^#" ${FILE} | \
- gawk -F ":" '$1=="" || $1~/[^ ] [^ ]/ || $2==""|| $2~/[^ ] [^ ]/ || $3!="" { print "'${FILE}:'" NR ": " $0 ; exit 2 }'
-if [ "$?" != "0" ] ; then
- echo "Error: wrong line format."
- echo "So, nothing is modified."
- exit 1
-fi
-
-# Ok, go on.
-if [ "${PARALLEL}" != "" ] ; then
-
-# 'parallel' considers the full line as one argument, so
-# 'tr' is used to split the line in two and empty line have to be removed.
- grep -v "^#" $1 \
- | grep -v "\.ignore$" \
- | tr -s ":[:blank:]" "\n" | grep -v '^$' \
- | ${PARALLEL} -n 2 ${MAX_PROCS} ${PROCESS} ${HEADACHE} -c ${HEADACHE_CONFIG} -h ${HEADER_SRC}/{2} ${TARGET_DIR}/{1}
-
-else
-
-# 'xargs' has no support for context replace, so 'gawk" is used to create the arguments.
- grep -v "^#" $1 \
- | grep -v "\.ignore$" \
- | tr -s ":[:blank:]" " " | grep -v '^ *$' \
- | gawk '{ print "'${HEADER_SRC}'/" $2 " '${TARGET_DIR}'/" $1 }' \
- | xargs -n 2 ${MAX_PROCS} ${PROCESS} ${HEADACHE} -c ${HEADACHE_CONFIG} -h
-
-fi
diff --git a/ivette/.gitattributes b/ivette/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..5e72525280e8222807684b346bb654b0796e14db
--- /dev/null
+++ b/ivette/.gitattributes
@@ -0,0 +1,25 @@
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+/configure.js header_spec=.ignore
+/sandboxer.js header_spec=.ignore
+/.babelrc header_spec=.ignore
+/.eslint* header_spec=.ignore
+/doc/**/*.js header_spec=.ignore
+/dome/doc/**/*.js header_spec=.ignore
+/src/dome/doc/template/static/fonts/*-webfont.* header_spec=.ignore
+/src/dome/template/git-ignore header_spec=.ignore
+/src/dome/doc/template/tmpl/*.tmpl header_spec=.ignore
+/src/dome/doc/**/*.js header_spec=.ignore
+/src/dome/doc/**/*.htm header_spec=.ignore
+/src/dome/doc/**/*.txt header_spec=.ignore
+/src/dome/**/*.el header_spec=.ignore
+/tests/*.i header_spec=.ignore
+/**/*.css header_spec=.ignore
+/**/*.html header_spec=.ignore
+/**/*.json header_spec=.ignore
+/**/*.lua header_spec=.ignore
+/*.icns header_spec=.ignore
+/*.lock header_spec=.ignore
+
diff --git a/ivette/Makefile.distrib b/ivette/Makefile.distrib
index 0f933db596ee0febd3157aa739797a507e871fee..aba92d615b478994627ab07a2b5afdf7dae9e98a 100644
--- a/ivette/Makefile.distrib
+++ b/ivette/Makefile.distrib
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
HEADER_SPEC += ivette/./headers/header_spec.txt
DISTRIB_FILES += ivette/.babelrc
DISTRIB_FILES += ivette/.dome-pkg-app.lock
diff --git a/ivette/distrib.sh b/ivette/distrib.sh
index 38012edac621ff293d5ea0b1f3964f68d9adc5a4..bf3f52392ee8af21f0f2d32e441a1dec2d072b6f 100755
--- a/ivette/distrib.sh
+++ b/ivette/distrib.sh
@@ -1,4 +1,26 @@
#!/bin/sh -e
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Generate Files for Ivette Distribution
# --------------------------------------------------------------------------
diff --git a/ivette/headers/header_spec.txt b/ivette/headers/header_spec.txt
index 361c89dfb300142bb207d7bdcf5f4010d130f83b..649ed47c9564883ad2bfdc95277c9831e3a661f3 100644
--- a/ivette/headers/header_spec.txt
+++ b/ivette/headers/header_spec.txt
@@ -9,13 +9,13 @@ INSTALL.md: .ignore
Makefile: CEA_LGPL
README.md: .ignore
configure.js: .ignore
-distrib.sh: .ignore
+distrib.sh: CEA_LGPL
doc/pandoc/href.lua: .ignore
doc/pandoc/index.json: .ignore
doc/pandoc/template.html: .ignore
electron-builder.json: .ignore
electron-webpack.json: .ignore
-ivette-macos.sh: .ignore
+ivette-macos.sh: CEA_LGPL
package.json: .ignore
sandboxer.js: .ignore
src/dome/.gitignore: .ignore
@@ -130,19 +130,19 @@ src/dome/renderer/themes.tsx: CEA_LGPL
src/dome/template/Application.js: CEA_LGPL
src/dome/template/Preferences.js: CEA_LGPL
src/dome/template/babelrc.json: .ignore
-src/dome/template/dome-pull.sh: .ignore
-src/dome/template/dome-push.sh: .ignore
+src/dome/template/dome-pull.sh: CEA_LGPL
+src/dome/template/dome-push.sh: CEA_LGPL
src/dome/template/electron-webpack.json: .ignore
-src/dome/template/export.sh: .ignore
+src/dome/template/export.sh: CEA_LGPL
src/dome/template/git-ignore: .ignore
src/dome/template/main.js: CEA_LGPL
-src/dome/template/makefile: .ignore
-src/dome/template/makefile.app.packages: .ignore
-src/dome/template/makefile.packages: .ignore
-src/dome/template/package.sh: .ignore
+src/dome/template/makefile: CEA_LGPL
+src/dome/template/makefile.app.packages: CEA_LGPL
+src/dome/template/makefile.packages: CEA_LGPL
+src/dome/template/package.sh: CEA_LGPL
src/dome/template/renderer.js: CEA_LGPL
src/dome/template/typescript.el: .ignore
-src/dome/template/update.sh: .ignore
+src/dome/template/update.sh: CEA_LGPL
src/dome/template/webpack.main.js: CEA_LGPL
src/dome/template/webpack.renderer.js: CEA_LGPL
src/frama-c/api_generator.ml: CEA_LGPL
@@ -209,6 +209,6 @@ tests/eva-1.i: .ignore
tests/eva-2.i: .ignore
tsconfig.json: .ignore
tsfmt.json: .ignore
-webpack.main.js: .ignore
-webpack.renderer.js: .ignore
+webpack.main.js: CEA_LGPL
+webpack.renderer.js: CEA_LGPL
yarn.lock: .ignore
diff --git a/ivette/ivette-macos.sh b/ivette/ivette-macos.sh
index 33215a6b10c09231429fca01a2133d77bc18ddad..d96a421f382fbb17dea3f88b637b15f3a199a6c6 100755
--- a/ivette/ivette-macos.sh
+++ b/ivette/ivette-macos.sh
@@ -1,3 +1,24 @@
#!/bin/zsh
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
exec open -na /Applications/Ivette.app --args --working $PWD $*
diff --git a/ivette/src/dome/template/dome-pull.sh b/ivette/src/dome/template/dome-pull.sh
index b579cf35a1a2492f9cbe452e63abbc1a6dcf7244..7bec6736c8a5581a09075f1554fa0161efcb0efa 100755
--- a/ivette/src/dome/template/dome-pull.sh
+++ b/ivette/src/dome/template/dome-pull.sh
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Pulling Dome Updates
# --------------------------------------------------------------------------
diff --git a/ivette/src/dome/template/dome-push.sh b/ivette/src/dome/template/dome-push.sh
index 60816ed9ecb0103ee1206d5c28db7ecada3737e5..94fd495fbb990453016fdc2ad2737e331c6e1bbe 100755
--- a/ivette/src/dome/template/dome-push.sh
+++ b/ivette/src/dome/template/dome-push.sh
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Pulling Dome Updates
# --------------------------------------------------------------------------
diff --git a/ivette/src/dome/template/export.sh b/ivette/src/dome/template/export.sh
index ea5dc39d5fee0fabce5501431253fce3e19bf788..6cdae2a4802e0931935cf2ef7d504c4844b733ae 100755
--- a/ivette/src/dome/template/export.sh
+++ b/ivette/src/dome/template/export.sh
@@ -1,4 +1,25 @@
#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# --------------------------------------------------------------------------
# --- Export Dome API
diff --git a/ivette/src/dome/template/makefile b/ivette/src/dome/template/makefile
index 376d32c4fadf74c1c5bd08d3f8761a1821cb570d..29df4121517ee94ea96a1a9e90a0ea3e559bd768 100644
--- a/ivette/src/dome/template/makefile
+++ b/ivette/src/dome/template/makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Main Makefile for building Dome applications
# --------------------------------------------------------------------------
diff --git a/ivette/src/dome/template/makefile.app.packages b/ivette/src/dome/template/makefile.app.packages
index 58aa6a3ad516168d48315864bfcf57376187f2b0..04b26ffe0ed0ff0757a23a0fc4b805fa32249742 100644
--- a/ivette/src/dome/template/makefile.app.packages
+++ b/ivette/src/dome/template/makefile.app.packages
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Package Template Definitions
# --------------------------------------------------------------------------
diff --git a/ivette/src/dome/template/makefile.packages b/ivette/src/dome/template/makefile.packages
index 72e46b988425f140e03588c687b63acca23b4b39..4b5bbafac90e47fcfbee33487b0339ff7de43452 100644
--- a/ivette/src/dome/template/makefile.packages
+++ b/ivette/src/dome/template/makefile.packages
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Packages Definitions for Dome environment ---
# --------------------------------------------------------------------------
diff --git a/ivette/src/dome/template/package.sh b/ivette/src/dome/template/package.sh
index 58e4428ffb8b421a8c3c99266057dbb0962bc1fe..5cadbb7444030b1dfb0cec0a82f6591554fe1bdd 100755
--- a/ivette/src/dome/template/package.sh
+++ b/ivette/src/dome/template/package.sh
@@ -1,4 +1,25 @@
#!/bin/sh
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# --------------------------------------------------------------------------
# --- Compute mode
diff --git a/ivette/src/dome/template/update.sh b/ivette/src/dome/template/update.sh
index 56d22295ef24fa4f37c19a100797c6005561921d..d48e589170acc09d3e9bbb52e76d377912e51574 100755
--- a/ivette/src/dome/template/update.sh
+++ b/ivette/src/dome/template/update.sh
@@ -1,4 +1,25 @@
#!/bin/sh
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# --------------------------------------------------------------------------
# --- Update Templated File (merge with user modifications)
diff --git a/nix/default.nix b/nix/default.nix
index 6c86751e7bead1dc4fb86db8ac648680528ecd5c..50cdf2558d052fbb1e12d3db53d39ba4df6591a3 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -280,7 +280,7 @@ pkgs.lib.makeExtensible
make clean_share_link
make create_share_link
export CONFIGS="equality bitwise symblocs gauges octagon"
- src/plugins/value/vtests -j 4 -error-code
+ src/plugins/value/vtests.sh -j 4 -error-code
'';
installPhase = ''
true
diff --git a/nix/frama-c-public/ssh.sh b/nix/frama-c-public/ssh.sh
index faeb299c681d47c6abdc79ffafbde0a2b1ec9ad9..55e5887a4070163f5243a49a71377267f8d14f7a 100755
--- a/nix/frama-c-public/ssh.sh
+++ b/nix/frama-c-public/ssh.sh
@@ -1,4 +1,25 @@
#!/bin/sh -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
PWD=$(dirname $0)
diff --git a/nix/frama-ci.sh b/nix/frama-ci.sh
index b4deee0abc1543e01c82d3c6c92d9b0045b26d77..5db2f7357c230c6040e64d3d37d1e315c50e9f8a 100755
--- a/nix/frama-ci.sh
+++ b/nix/frama-ci.sh
@@ -1,4 +1,25 @@
#!/bin/sh -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
DIR=$(dirname $0)
diff --git a/ptests/check_oracles.sh b/ptests/check_oracles.sh
index a7bb568c1f52e01a6a31cc2a0478c30abdb3a003..91e7177f6b99224f6c04c156c8f435e729fd22bc 100755
--- a/ptests/check_oracles.sh
+++ b/ptests/check_oracles.sh
@@ -1,4 +1,25 @@
#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# Checks for extraneous, leftover oracle files that are no longer necessary.
# Only reports files in plugins with a ptests_config file, and in directories
diff --git a/share/_frama-c.zsh b/share/_frama-c.zsh
index 8dda747e2e0f3e1d551c5cc0654e0aec1446eec3..8a4a6b2a743d35e495a3d06bd7f64118662e8b11 100644
--- a/share/_frama-c.zsh
+++ b/share/_frama-c.zsh
@@ -1,4 +1,25 @@
#compdef frama-c
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# -----------------------------------------------------------------------------
# zsh completion for Frama-C
diff --git a/share/analysis-scripts/bench-sqlite.sh b/share/analysis-scripts/bench-sqlite.sh
index 954cb0e9f84226309f3a60a98b542cffd5373fff..17eaa35c3d2ba5027982782c6ac3463da3806ecb 100755
--- a/share/analysis-scripts/bench-sqlite.sh
+++ b/share/analysis-scripts/bench-sqlite.sh
@@ -1,4 +1,25 @@
#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
database="benchmark-results.db"
stats="$1"
diff --git a/share/analysis-scripts/clone.sh b/share/analysis-scripts/clone.sh
index 0ed6b8553c2144fb94fb9cd8f3260f39b65212d9..c8ee9c96ed909f15822a2eb038d676fa067d90c2 100755
--- a/share/analysis-scripts/clone.sh
+++ b/share/analysis-scripts/clone.sh
@@ -1,4 +1,25 @@
#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
git_hash="master"
clone_dir="frama-c-clones"
diff --git a/share/analysis-scripts/cmd-dep.sh b/share/analysis-scripts/cmd-dep.sh
index d045b1cf56304862be02148358550bd8c6cb7dfc..f7ed9168d22dbb0c62fcd658b6b36f341075c304 100755
--- a/share/analysis-scripts/cmd-dep.sh
+++ b/share/analysis-scripts/cmd-dep.sh
@@ -1,4 +1,26 @@
#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
set -eu
if [ $# -lt 1 ]
diff --git a/share/analysis-scripts/concat-csv.sh b/share/analysis-scripts/concat-csv.sh
index 8079d3004553a63ca9b20b93e8330016993bc2dc..96d87aeed87b2f45bf927251e11feffa01bf2e9e 100755
--- a/share/analysis-scripts/concat-csv.sh
+++ b/share/analysis-scripts/concat-csv.sh
@@ -1,4 +1,25 @@
#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
set -o pipefail
diff --git a/share/analysis-scripts/fc_stubs.c b/share/analysis-scripts/fc_stubs.c
index fad866f2160ba5533c8658794a520c2bf0880962..2c9698c18e444f0ebe44055faa0450821faea0bb 100644
--- a/share/analysis-scripts/fc_stubs.c
+++ b/share/analysis-scripts/fc_stubs.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
// Stub for a main function which reads arguments from the command line, to be
// used by the Eva plug-in.
// This stub emulates non-deterministic input of up to 5 arguments, each up
diff --git a/share/analysis-scripts/function_finder.py b/share/analysis-scripts/function_finder.py
index 22af511f79059b026127417874d7509f98a309bb..381dd64b29da58e3660d7fa99ff2d3cfb7fb9bf8 100644
--- a/share/analysis-scripts/function_finder.py
+++ b/share/analysis-scripts/function_finder.py
@@ -1,9 +1,10 @@
+#!/usr/bin/env python3
# -*- coding: utf-8 -*-
##########################################################################
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2021 #
+# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/share/analysis-scripts/parse-coverage.sh b/share/analysis-scripts/parse-coverage.sh
index 13ef4141765c34b099f2d8ae7409f562c788feed..ade4f113bcac226b8747bc589c539c5e612989db 100755
--- a/share/analysis-scripts/parse-coverage.sh
+++ b/share/analysis-scripts/parse-coverage.sh
@@ -1,4 +1,25 @@
#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
log_file=$1
stats_file=$2
diff --git a/share/analysis-scripts/plot.sh b/share/analysis-scripts/plot.sh
index 0db4d1ba284bbdfa2e0ef26e8f6180e231cd2b1c..bc68f1fef0ede3dd8d4e95cda8d98fd810169bde 100755
--- a/share/analysis-scripts/plot.sh
+++ b/share/analysis-scripts/plot.sh
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
target=$1
{
diff --git a/share/analysis-scripts/script_for_creduce_fatal.sh b/share/analysis-scripts/script_for_creduce_fatal.sh
index a0fc2ba7b9574f959ac738261ec7486cc5850c52..4a2e8b9ef3d1273f85e5640e7516a31c9c8fcea0 100644
--- a/share/analysis-scripts/script_for_creduce_fatal.sh
+++ b/share/analysis-scripts/script_for_creduce_fatal.sh
@@ -1,4 +1,25 @@
#!/bin/bash -e
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# Script to reduce a Frama-C crashing test case.
diff --git a/share/analysis-scripts/script_for_creduce_non_fatal.sh b/share/analysis-scripts/script_for_creduce_non_fatal.sh
index d886aeaba29099358e77597529d56ed6ff25dbad..7ad71d593dbb729b76aea893363088a147df8609 100644
--- a/share/analysis-scripts/script_for_creduce_non_fatal.sh
+++ b/share/analysis-scripts/script_for_creduce_non_fatal.sh
@@ -1,4 +1,25 @@
#!/bin/bash -e
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# Script to reduce a Frama-C non-crashing test case.
diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk
index 689b9eab61ccedee46cb8637eaaa9a51e3ad3f09..54cdd1332ac9cc37c6ceaae223ad16f217af1d79 100644
--- a/share/analysis-scripts/template.mk
+++ b/share/analysis-scripts/template.mk
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
diff --git a/src/plugins/.gitattributes b/src/plugins/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..856f653c296e134de64d231bc6fe9342dbc5a1ca
--- /dev/null
+++ b/src/plugins/.gitattributes
@@ -0,0 +1,47 @@
+########################################
+# HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY #
+########################################
+
+config* header_spec=CEA_LGPL_OR_PROPRIETARY
+makefile* header_spec=CEA_LGPL_OR_PROPRIETARY
+Make* header_spec=CEA_LGPL_OR_PROPRIETARY
+*.mk header_spec=CEA_LGPL_OR_PROPRIETARY
+
+
+*.c header_spec=CEA_LGPL_OR_PROPRIETARY
+*.h header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.htm header_spec=CEA_LGPL_OR_PROPRIETARY
+*.html header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.js header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.ml header_spec=CEA_LGPL_OR_PROPRIETARY
+*.ml.in header_spec=CEA_LGPL_OR_PROPRIETARY
+*.mli header_spec=CEA_LGPL_OR_PROPRIETARY
+*.mli.in header_spec=CEA_LGPL_OR_PROPRIETARY
+*.mll header_spec=CEA_LGPL_OR_PROPRIETARY
+*.mly header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.xml header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.pl header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.py header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.rc header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.sh header_spec=CEA_LGPL_OR_PROPRIETARY
+*.zsh header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.css header_spec=CEA_LGPL_OR_PROPRIETARY
+
+*.ts header_spec=CEA_LGPL_OR_PROPRIETARY
+*.tsx header_spec=CEA_LGPL_OR_PROPRIETARY
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+/*/tests/**/* header_spec=.ignore
+
diff --git a/src/plugins/aorai/.gitattributes b/src/plugins/aorai/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..94782b4119b1bf3cc8abf8b3a569b2e12580b692
--- /dev/null
+++ b/src/plugins/aorai/.gitattributes
@@ -0,0 +1,21 @@
+###########################
+# HEADER_SPEC: AORAI_LGPL #
+###########################
+
+/configure.ac header_spec=AORAI_LGPL
+
+/Makefile header_spec=AORAI_LGPL
+/Makefile.in header_spec=AORAI_LGPL
+
+*.ml header_spec=AORAI_LGPL
+*.mli header_spec=AORAI_LGPL
+*.mll header_spec=AORAI_LGPL
+*.mly header_spec=AORAI_LGPL
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+/INSTALL header_spec=.ignore
+/VERSIONS.txt header_spec=.ignore
+/tests/**/* header_spec=.ignore
diff --git a/src/plugins/e-acsl/.gitattributes b/src/plugins/e-acsl/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..cca30ad415b5e0fc3ed4672497b187c825f437bf
--- /dev/null
+++ b/src/plugins/e-acsl/.gitattributes
@@ -0,0 +1,69 @@
+###############################################
+# HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY.E_ACSL #
+###############################################
+
+configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+
+Makefile header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+Makefile.in header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+
+*.c header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+*.h header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+
+*.ml header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+*.mli header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+
+*.sh header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+
+/man/e-acsl-gcc.sh.1 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
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+README header_spec=.ignore
+
+/.clang-format header_spec=.ignore
+/doc/Makefile.common header_spec=.ignore
+/doc/support/MakeLaTeXModern header_spec=.ignore
+/doc/Changelog header_spec=.ignore
+/doc/doxygen/doxygen.cfg.in header_spec=.ignore
+/doc/refman/*.tex header_spec=.ignore
+/doc/userman/*.tex header_spec=.ignore
+
+/examples/demo/TODO header_spec=.ignore
+/examples/ensuresec/push-alerts/.env-example header_spec=.ignore
+
+/headers/close-source/* header_spec=.ignore
+/headers/open-source/* header_spec=.ignore
+
+/license/* header_spec=.ignore
+
+# Becarefull at the order with the previous lines
+/contrib/**/*.c header_spec=.ignore
+
+/doc/**/Makefile header_spec=.ignore
+/doc/**/*.ml header_spec=.ignore
+/doc/**/*.mll header_spec=.ignore
+/doc/**/*.c header_spec=.ignore
+/doc/**/*.i header_spec=.ignore
+
+/examples/**/Makefile header_spec=.ignore
+/examples/**/*.c header_spec=.ignore
+/examples/**/*.i header_spec=.ignore
+/examples/**/*.ml header_spec=.ignore
+/examples/**/*.sh header_spec=.ignore
+/examples/**/*.py header_spec=.ignore
+
+/tests/test_config header_spec=.ignore
+/tests/test_config_dev header_spec=.ignore
+/tests/**/* header_spec
+
+/tests/wrapper.sh header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
+/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/markdown-report/.gitattributes b/src/plugins/markdown-report/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..e558434280b3047d5711facb618b3e374022b52c
--- /dev/null
+++ b/src/plugins/markdown-report/.gitattributes
@@ -0,0 +1,5 @@
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+/META.in header_spec=.ignore
diff --git a/src/plugins/qed/.gitattributes b/src/plugins/qed/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..dae65a33b405a5d049d491de7d2383f21cf79ae1
--- /dev/null
+++ b/src/plugins/qed/.gitattributes
@@ -0,0 +1,8 @@
+*.ml header_spec=CEA_WP
+*.mli header_spec=CEA_WP
+*.mll header_spec=CEA_WP
+
+configure.ac header_spec=CEA_WP
+
+Makefile header_spec=CEA_WP
+Makefile.in header_spec=CEA_WP
diff --git a/src/plugins/value/.gitattributes b/src/plugins/value/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..e62b79b9279d0dae86ee89c3782e8600365bb619
--- /dev/null
+++ b/src/plugins/value/.gitattributes
@@ -0,0 +1,6 @@
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+/Changelog_non_free header_spec=.ignore
+/legacy/TOREMOVE header_spec=.ignore
diff --git a/src/plugins/value/gen-api.sh b/src/plugins/value/gen-api.sh
index d00c16fdd4a1175ff780c5479fbb266043c7ba49..e626fff905e7d6920d563b961cacea3ad7a5166f 100755
--- a/src/plugins/value/gen-api.sh
+++ b/src/plugins/value/gen-api.sh
@@ -1,4 +1,26 @@
#!/usr/bin/env bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
set -eu
printf '(** Eva public API.
diff --git a/src/plugins/value/gen_test_config.sh b/src/plugins/value/gen_test_config.sh
index b1085f0868634319e144ef3549f4518e100638ca..7d2f84316e0bf62436771e4f0af36314a427f049 100755
--- a/src/plugins/value/gen_test_config.sh
+++ b/src/plugins/value/gen_test_config.sh
@@ -1,4 +1,25 @@
#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# This scripts creates the ptests config files for the alternative testing
# configurations of Eva. You must create the tests/test_config and
diff --git a/src/plugins/value/test.assert.sh b/src/plugins/value/test.assert.sh
index 38049b28c4c8d1e44620765127875b5d1773f8db..382cdce643d939134c587a687c763e82f261746c 100755
--- a/src/plugins/value/test.assert.sh
+++ b/src/plugins/value/test.assert.sh
@@ -1,4 +1,26 @@
#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
export GCC3264=-m32
export FRAMAC3264=x86_32
#export GCC3264=
diff --git a/src/plugins/value/test.sh b/src/plugins/value/test.sh
index 1c19540871f090abbdb78f4ee1c4eda1b8f15625..54e88f0a2fb5d1e336be131bdcfc4cd977e576f3 100755
--- a/src/plugins/value/test.sh
+++ b/src/plugins/value/test.sh
@@ -1,4 +1,26 @@
#!/bin/bash
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
export GCC3264=-m32
export FRAMAC3264=x86_32
#export GCC3264=
diff --git a/src/plugins/value/test_config b/src/plugins/value/test_config
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/value/vtests b/src/plugins/value/vtests
deleted file mode 100755
index 14cd7c69237386cfa4f64debc1346bb98744b315..0000000000000000000000000000000000000000
--- a/src/plugins/value/vtests
+++ /dev/null
@@ -1,40 +0,0 @@
-#!/bin/bash -eu
-
-if [ -z ${TARGETS+x} ]; then
- TARGETS="float value idct builtins"
-fi
-if [ -z ${CONFIGS+x} ]; then
- CONFIGS="apron equality bitwise symblocs gauges octagon multidim"
-fi
-ARGS="${@-}"
-
-# has_target returns 0 if at least one of the arguments is a target
-# (i.e. not an option such as "-j 8"). If so, do not run tests
-# for all default targets, only for the specified target(s)
-has_target=0
-# sets has_target=0
-function has_target() {
- local __has_target=1
- for f in $@; do
- __re="\\b$f\\b" # match argument as whole word
- if [[ "$f" =~ \.[ci]$ || \
- ( "$f" =~ ^[A-Za-z] && "${TARGETS[@]}" =~ $__re ) ]]; then
- __has_target=0
- fi
- done
- return $__has_target
-}
-
-if has_target ${ARGS[@]}; then
- TARGETS_AND_ARGS="${ARGS[@]}"
-else
- TARGETS_AND_ARGS="${TARGETS[@]} ${ARGS[@]}"
-fi
-
-echo "CONFIGS: ${CONFIGS[@]}"
-for config in ${CONFIGS[@]}
-do
- set -x
- ./bin/ptests.opt -config $config ${TARGETS_AND_ARGS[@]}
- { set +x; } 2>&-
-done
diff --git a/src/plugins/value/vtests.sh b/src/plugins/value/vtests.sh
new file mode 100755
index 0000000000000000000000000000000000000000..0137eaf4c6a18eac0248af5f9d82b438bbf130ce
--- /dev/null
+++ b/src/plugins/value/vtests.sh
@@ -0,0 +1,61 @@
+#!/bin/bash -eu
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
+
+if [ -z ${TARGETS+x} ]; then
+ TARGETS="float value idct builtins"
+fi
+if [ -z ${CONFIGS+x} ]; then
+ CONFIGS="apron equality bitwise symblocs gauges octagon multidim"
+fi
+ARGS="${@-}"
+
+# has_target returns 0 if at least one of the arguments is a target
+# (i.e. not an option such as "-j 8"). If so, do not run tests
+# for all default targets, only for the specified target(s)
+has_target=0
+# sets has_target=0
+function has_target() {
+ local __has_target=1
+ for f in $@; do
+ __re="\\b$f\\b" # match argument as whole word
+ if [[ "$f" =~ \.[ci]$ || \
+ ( "$f" =~ ^[A-Za-z] && "${TARGETS[@]}" =~ $__re ) ]]; then
+ __has_target=0
+ fi
+ done
+ return $__has_target
+}
+
+if has_target ${ARGS[@]}; then
+ TARGETS_AND_ARGS="${ARGS[@]}"
+else
+ TARGETS_AND_ARGS="${TARGETS[@]} ${ARGS[@]}"
+fi
+
+echo "CONFIGS: ${CONFIGS[@]}"
+for config in ${CONFIGS[@]}
+do
+ set -x
+ ./bin/ptests.opt -config $config ${TARGETS_AND_ARGS[@]}
+ { set +x; } 2>&-
+done
diff --git a/src/plugins/wp/.gitattributes b/src/plugins/wp/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..e40f62d0ebbd58f376caea96817a16640f49650f
--- /dev/null
+++ b/src/plugins/wp/.gitattributes
@@ -0,0 +1,65 @@
+#######################
+# HEADER_SPEC: CEA_WP #
+#######################
+
+*.ml header_spec=CEA_WP
+*.mli header_spec=CEA_WP
+*.mll header_spec=CEA_WP
+
+*.mlw header_spec=CEA_WP
+*.driver header_spec=CEA_WP
+*.v header_spec=CEA_WP
+*.css header_spec=CEA_WP
+
+configure.ac header_spec=CEA_WP
+
+Makefile header_spec=CEA_WP
+Makefile.in header_spec=CEA_WP
+Makefile.resources header_spec=CEA_WP
+MakeDoc header_spec=CEA_WP
+
+/intro_wp.txt header_spec=CEA_WP
+
+#######################
+# HEADER_SPEC: others #
+#######################
+
+/doc/coqdoc/coq2tex/*.mll header_spec=XL_COMPCERT
+
+/share/coqwp/BuiltIn.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/HighOrd.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/bool/Bool.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/Abs.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/ComputerDivision.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/EuclideanDivision.v header_spec=MODIFIED_WHY3
+/share/coqwp/int/Exponentiation.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/Int.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/MinMax.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/Power.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/int/ComputerOfEuclideanDivision.v header_spec=MODIFIED_WHY3
+/share/coqwp/map/Map.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/map/Const.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/Abs.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/FromInt.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/ExpLog.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/MinMax.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/PowerReal.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/Real.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/RealInfix.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/Square.v header_spec=UNMODIFIED_WHY3
+/share/coqwp/real/Trigonometry.v header_spec=UNMODIFIED_WHY3
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+/doc/coqdoc/coq2tex/coq2html.js header_spec=.ignore
+/doc/coqdoc/coq2tex/*.css header_spec=.ignore
+/doc/coqdoc/coq2tex/*.html header_spec=.ignore
+/doc/coqdoc/*.tex header_spec=.ignore
+
+/doc/manual/nullable.c header_spec=.ignore
+/doc/manual/*.tex header_spec=.ignore
+
+
+/tests/**/* header_spec=.ignore
diff --git a/src/plugins/wp/doc/MakeDoc b/src/plugins/wp/doc/MakeDoc
index b646e4383b9812cac2fde373dbbb3679487199d8..53d34f0f625a9e62b19c64eee2b304dbf050e323 100644
--- a/src/plugins/wp/doc/MakeDoc
+++ b/src/plugins/wp/doc/MakeDoc
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# This file is part of WP plug-in of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat a l'energie atomique et aux energies #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- Resources ---
# --------------------------------------------------------------------------
diff --git a/src/plugins/wp/doc/coqdoc/Makefile b/src/plugins/wp/doc/coqdoc/Makefile
index a0a35db3e79cc52fe79a66e45c47a29ea641128b..92c3db78d1c683bd1e9b9ed36dcacd45c99eff44 100644
--- a/src/plugins/wp/doc/coqdoc/Makefile
+++ b/src/plugins/wp/doc/coqdoc/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# This file is part of WP plug-in of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat a l'energie atomique et aux energies #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- WP User & Reference Manual ---
# --------------------------------------------------------------------------
@@ -31,4 +53,4 @@ wpcoq.pdf: $(FRAMAC_DOC) $(TEX) .lib coq2latex.sty
rubber -d wpcoq
clean::
- rm -f .lib $(addsuffix .tex,$(COQL))
\ No newline at end of file
+ rm -f .lib $(addsuffix .tex,$(COQL))
diff --git a/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll b/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll
index 21d22600021af223732b9a6a500bc145f0f9790d..230de710f3bed354453441f7ffb9a8a44acbe7fb 100644
--- a/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll
+++ b/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll
@@ -1,17 +1,15 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
+(**************************************************************************)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(**************************************************************************)
{
open Printf
diff --git a/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll b/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll
index 78cb86b014a44c583ba4aeeca87114d9900aa5b0..0d16708fe724eae0c57464d3cd51c392900d0779 100644
--- a/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll
+++ b/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll
@@ -1,17 +1,15 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
+(**************************************************************************)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(**************************************************************************)
{
open Printf
diff --git a/src/plugins/wp/doc/manual/Makefile b/src/plugins/wp/doc/manual/Makefile
index 1f64775fdcf26a85f3802aeafe0434ddc1ff5220..f1e5b1b10dfcc4f310da006442df013170f40cb5 100644
--- a/src/plugins/wp/doc/manual/Makefile
+++ b/src/plugins/wp/doc/manual/Makefile
@@ -1,3 +1,25 @@
+##########################################################################
+# #
+# This file is part of WP plug-in of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat a l'energie atomique et aux energies #
+# 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). #
+# #
+##########################################################################
+
# --------------------------------------------------------------------------
# --- WP User & Reference Manual ---
# --------------------------------------------------------------------------
diff --git a/src/plugins/wp/doc/ocamldoc.css b/src/plugins/wp/doc/ocamldoc.css
index 61e22cc801685a15b9c78b7d38d3c54b0ec99e87..2dd72db72c834a5ab192511cd0a32eb84567f01c 100644
--- a/src/plugins/wp/doc/ocamldoc.css
+++ b/src/plugins/wp/doc/ocamldoc.css
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* This file is part of WP plug-in of Frama-C. */
+/* */
+/* Copyright (C) 2007-2022 */
+/* CEA (Commissariat a l'energie atomique et aux energies */
+/* 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). */
+/* */
+/**************************************************************************/
+
* { margin: 0; padding: 0 }
body {