From 638439797b49138dc55aa9fc42e0c60e2bc98bf0 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 1 Feb 2021 19:19:56 +0100
Subject: [PATCH] fix headers

---
 Makefile.in                                   | 31 +++++++++++++++----
 MetAcsl.mli                                   | 15 +++++++--
 configure.ac                                  |  3 +-
 .../close-source/CEA_LGPL_OR_PROPRIETARY.META |  2 +-
 headers/close-source/SETLOG_LGPL              |  6 ++++
 headers/header_config.txt                     |  6 ++++
 headers/header_spec.txt                       | 13 +++++++-
 .../open-source/CEA_LGPL_OR_PROPRIETARY.META  |  3 +-
 headers/open-source/SETLOG_LGPL               |  6 ++++
 meta_annotate.ml                              |  3 +-
 meta_bindings.ml                              |  3 +-
 meta_bindings.mli                             |  3 +-
 meta_deduce.ml                                | 22 +++++++++++++
 meta_dispatch.ml                              |  3 +-
 meta_dispatch.mli                             |  3 +-
 meta_options.ml                               |  3 +-
 meta_parse.ml                                 |  3 +-
 meta_parse.mli                                |  3 +-
 meta_run.ml                                   |  3 +-
 meta_simplify.ml                              |  3 +-
 meta_simplify.mli                             |  3 +-
 meta_utils.ml                                 |  3 +-
 share/model.slog                              | 22 +++++++++++++
 share/run.pl                                  | 22 +++++++++++++
 share/setlog.pl                               |  8 +++++
 share/setlog_rules.pl                         | 10 +++++-
 share/setloglib.slog                          | 12 +++++--
 27 files changed, 189 insertions(+), 28 deletions(-)
 create mode 100644 headers/close-source/SETLOG_LGPL
 create mode 100644 headers/open-source/SETLOG_LGPL

diff --git a/Makefile.in b/Makefile.in
index ca8f1b5..82d2e16 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -2,12 +2,21 @@
 #                                                                        #
 #  This file is part of the Frama-C's MetACSL plug-in.                   #
 #                                                                        #
-#  Copyright (C) 2012-2020                                               #
+#  Copyright (C) 2018-2021                                               #
 #    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 LICENSE)                       #
 #                                                                        #
 ##########################################################################
 
@@ -22,7 +31,10 @@ HAS_WP=@HAS_WP@
 
 PLUGIN_NAME = MetAcsl
 
-MetAcsl_DISTRIB_EXTERNAL:=Makefile.in configure configure.ac README.md tests share opam
+MetAcsl_DISTRIB_EXTERNAL:=Makefile.in configure configure.ac README.md \
+	tests opam \
+	$(addprefix share/, \
+	   model.slog run.pl setloglib.slog setlog.pl setlog_rules.pl)
 
 PLUGIN_DIR ?= .
 PLUGIN_CMO = meta_utils      \
@@ -79,6 +91,7 @@ ifneq ("$(FRAMAC_INTERNAL)","yes")
 
 VERSION=0.0
 EXTRAVERSION?=
+OPEN_SOURCE?=yes
 
 configure: configure.ac
 	autoconf -f
@@ -87,14 +100,20 @@ Makefile: configure Makefile.in
 	./config.status --recheck
 	./config.status
 
+ifeq ("$(OPEN_SOURCE)","yes")
+HEADER_DIR=open-source
+else
+HEADER_DIR=close-source
+endif
+
 .PHONY: headers
 headers:
 	while IFS=: read FILE LICENCE; do \
           LICENCE=$$(echo $$LICENCE | sed -e 's/^ *//'); \
           if test "$$LICENCE" != ".ignore"; then \
              headache \
-               -c headers/header_config.txt \
-               -h headers/open-source/$${LICENCE} \
+               -c $(MetAcsl_DIR)/headers/header_config.txt \
+               -h $(MetAcsl_DIR)/headers/$(HEADER_DIR)/$${LICENCE} \
                $${FILE}; \
           fi; \
         done \
diff --git a/MetAcsl.mli b/MetAcsl.mli
index b812cf9..14274bb 100644
--- a/MetAcsl.mli
+++ b/MetAcsl.mli
@@ -2,12 +2,21 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2019                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    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 LICENSE)                       *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/configure.ac b/configure.ac
index fd3978e..b5099a0 100644
--- a/configure.ac
+++ b/configure.ac
@@ -2,7 +2,7 @@
 #                                                                        #
 #  This file is part of the Frama-C's MetACSL plug-in.                   #
 #                                                                        #
-#  Copyright (C) 2018-2020                                               #
+#  Copyright (C) 2018-2021                                               #
 #    CEA (Commissariat à l'énergie atomique et aux énergies              #
 #         alternatives)                                                  #
 #                                                                        #
@@ -17,6 +17,7 @@
 #                                                                        #
 #  See the GNU Lesser General Public License version 2.1                 #
 #  for more details (enclosed in the file LICENSE)                       #
+#                                                                        #
 ##########################################################################
 
 m4_define([plugin_file],Makefile.in)
diff --git a/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META b/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META
index 51cae7a..13946ca 100644
--- a/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META
+++ b/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META
@@ -1,7 +1,7 @@
 
 This file is part of the Frama-C's MetACSL plug-in.
 
-Copyright (C) 2018-2020
+Copyright (C) 2018-2021
   CEA (Commissariat à l'énergie atomique et aux énergies
        alternatives)
 
diff --git a/headers/close-source/SETLOG_LGPL b/headers/close-source/SETLOG_LGPL
new file mode 100644
index 0000000..6bfdcac
--- /dev/null
+++ b/headers/close-source/SETLOG_LGPL
@@ -0,0 +1,6 @@
+                        Setlog library
+
+           by Maximiliano Cristia' and  Gianfranco Rossi
+                          April 2014
+
+                     Revised March 2017
diff --git a/headers/header_config.txt b/headers/header_config.txt
index f917283..d2e0b96 100644
--- a/headers/header_config.txt
+++ b/headers/header_config.txt
@@ -1 +1,7 @@
 | ".*configure\..*" -> frame open:"#"  line:"#" close:"#"
+
+##########
+# PROLOG #
+##########
+| ".*\.pl" -> frame open: "%" line: "%" close: "%"
+| ".*\.slog" -> frame open: "%" line: "%" close: "%"
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index c054331..050fca9 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1,10 +1,13 @@
-Makefile: CEA_LGPL_OR_PROPRIETARY.META
+Makefile: .ignore
+Makefile.in: CEA_LGPL_OR_PROPRIETARY.META
 TODO.md: .ignore
 configure: .ignore
 configure.ac: CEA_LGPL_OR_PROPRIETARY.META
+MetAcsl.mli: CEA_LGPL_OR_PROPRIETARY.META
 meta_annotate.ml: CEA_LGPL_OR_PROPRIETARY.META
 meta_bindings.ml: CEA_LGPL_OR_PROPRIETARY.META
 meta_bindings.mli: CEA_LGPL_OR_PROPRIETARY.META
+meta_deduce.ml: CEA_LGPL_OR_PROPRIETARY.META
 meta_dispatch.ml: CEA_LGPL_OR_PROPRIETARY.META
 meta_dispatch.mli: CEA_LGPL_OR_PROPRIETARY.META
 meta_options.ml: CEA_LGPL_OR_PROPRIETARY.META
@@ -13,4 +16,12 @@ meta_parse.mli: CEA_LGPL_OR_PROPRIETARY.META
 meta_run.ml: CEA_LGPL_OR_PROPRIETARY.META
 meta_simplify.ml: CEA_LGPL_OR_PROPRIETARY.META
 meta_simplify.mli: CEA_LGPL_OR_PROPRIETARY.META
+meta_utils.ml: CEA_LGPL_OR_PROPRIETARY.META
 README.md: .ignore
+tests: .ignore
+opam: .ignore
+share/setloglib.slog: SETLOG_LGPL
+share/setlog.pl: SETLOG_LGPL
+share/setlog_rules.pl: SETLOG_LGPL
+share/run.pl: CEA_LGPL_OR_PROPRIETARY.META
+share/model.slog: CEA_LGPL_OR_PROPRIETARY.META
diff --git a/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META b/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META
index 6dce548..2ea608f 100644
--- a/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META
+++ b/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META
@@ -1,7 +1,7 @@
 
 This file is part of the Frama-C's MetACSL plug-in.
 
-Copyright (C) 2018-2020
+Copyright (C) 2018-2021
   CEA (Commissariat à l'énergie atomique et aux énergies
        alternatives)
 
@@ -16,3 +16,4 @@ 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 LICENSE)
+
diff --git a/headers/open-source/SETLOG_LGPL b/headers/open-source/SETLOG_LGPL
new file mode 100644
index 0000000..6bfdcac
--- /dev/null
+++ b/headers/open-source/SETLOG_LGPL
@@ -0,0 +1,6 @@
+                        Setlog library
+
+           by Maximiliano Cristia' and  Gianfranco Rossi
+                          April 2014
+
+                     Revised March 2017
diff --git a/meta_annotate.ml b/meta_annotate.ml
index 59065ee..f45ea10 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Meta_utils
diff --git a/meta_bindings.ml b/meta_bindings.ml
index 14d88c5..e37d8a8 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Meta_options
diff --git a/meta_bindings.mli b/meta_bindings.mli
index d079ec2..9a13f46 100644
--- a/meta_bindings.mli
+++ b/meta_bindings.mli
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Cil_types
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 58dca2d..0d2e831 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -1,3 +1,25 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
+(*                                                                        *)
+(*  Copyright (C) 2018-2021                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
 open Cil_types
 open Meta_utils
 open Meta_options
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 923996f..27de33b 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Cil_types
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index dd72b00..0c9ec21 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Cil_types
diff --git a/meta_options.ml b/meta_options.ml
index 059c53a..d0e8c76 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 let help_msg = "This plugin translates the metaproperties in the code to native ACSL annotations" ^
diff --git a/meta_parse.ml b/meta_parse.ml
index b5e7607..882428f 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Logic_ptree
diff --git a/meta_parse.mli b/meta_parse.mli
index 61b01fc..4540c41 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Cil_types
diff --git a/meta_run.ml b/meta_run.ml
index 4cfcfb7..ab057a2 100644
--- a/meta_run.ml
+++ b/meta_run.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Meta_options
diff --git a/meta_simplify.ml b/meta_simplify.ml
index 46b985a..76f52db 100644
--- a/meta_simplify.ml
+++ b/meta_simplify.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Cil_types
diff --git a/meta_simplify.mli b/meta_simplify.mli
index 5e4dbaf..bd33ed1 100644
--- a/meta_simplify.mli
+++ b/meta_simplify.mli
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 open Cil_types
diff --git a/meta_utils.ml b/meta_utils.ml
index 5859dc3..64cdcf0 100644
--- a/meta_utils.ml
+++ b/meta_utils.ml
@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of the Frama-C's MetACSL plug-in.                   *)
 (*                                                                        *)
-(*  Copyright (C) 2018-2020                                               *)
+(*  Copyright (C) 2018-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -17,6 +17,7 @@
 (*                                                                        *)
 (*  See the GNU Lesser General Public License version 2.1                 *)
 (*  for more details (enclosed in the file LICENSE)                       *)
+(*                                                                        *)
 (**************************************************************************)
 
 module StrSet = Datatype.String.Set
diff --git a/share/model.slog b/share/model.slog
index 098c75a..279ad1c 100644
--- a/share/model.slog
+++ b/share/model.slog
@@ -1,3 +1,25 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                                        %
+%  This file is part of the Frama-C's MetACSL plug-in.                   %
+%                                                                        %
+%  Copyright (C) 2018-2021                                               %
+%    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 LICENSE)                       %
+%                                                                        %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 % ----------------
 % Call graph
 % ----------------
diff --git a/share/run.pl b/share/run.pl
index c2aaec2..1085239 100755
--- a/share/run.pl
+++ b/share/run.pl
@@ -1,3 +1,25 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                                        %
+%  This file is part of the Frama-C's MetACSL plug-in.                   %
+%                                                                        %
+%  Copyright (C) 2018-2021                                               %
+%    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 LICENSE)                       %
+%                                                                        %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 #!/usr/bin/env swipl
 
 :- initialization main.
diff --git a/share/setlog.pl b/share/setlog.pl
index 09091eb..4c543ab 100644
--- a/share/setlog.pl
+++ b/share/setlog.pl
@@ -1,3 +1,11 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                          Setlog library                                %
+%                                                                        %
+%             by Maximiliano Cristia' and  Gianfranco Rossi              %
+%                            April 2014                                  %
+%                                                                        %
+%                       Revised March 2017                               %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  VERSION 4.9.1-20
 
diff --git a/share/setlog_rules.pl b/share/setlog_rules.pl
index 114ea53..1fc68f1 100644
--- a/share/setlog_rules.pl
+++ b/share/setlog_rules.pl
@@ -1,3 +1,11 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                          Setlog library                                %
+%                                                                        %
+%             by Maximiliano Cristia' and  Gianfranco Rossi              %
+%                            April 2014                                  %
+%                                                                        %
+%                       Revised March 2017                               %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %
@@ -257,4 +265,4 @@ fail_rule('NatRangeNotEmpty4',I=int(N,Y),
  
 :- (exists_file('TTF_rules.pl'),!,consult('TTF_rules.pl') 
     ; 
-    true).
\ No newline at end of file
+    true).
diff --git a/share/setloglib.slog b/share/setloglib.slog
index 103b847..31371a1 100644
--- a/share/setloglib.slog
+++ b/share/setloglib.slog
@@ -1,4 +1,12 @@
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                          Setlog library                                %
+%                                                                        %
+%             by Maximiliano Cristia' and  Gianfranco Rossi              %
+%                            April 2014                                  %
+%                                                                        %
+%                       Revised March 2017                               %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 %%% version 4.6.13-1 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -386,4 +394,4 @@ filter([X|List],Set,NewList) :-
  setlog_prolog :-
     prolog_call(assert((user:unbounded_int(I) :- nonvar(I), I=int(A,B), (var(A),! ; var(B)) ))).
 
-:- setlog_prolog.
\ No newline at end of file
+:- setlog_prolog.
-- 
GitLab