From ab8e196dadea5ccc1b5f22bc5447a728471d1097 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Fri, 19 Jun 2020 09:33:54 +0200 Subject: [PATCH] [Dive] Uses frama-c headers. --- headers/header_spec.txt | 17 +++++++++++++++++ src/plugins/dive/Dive.mli | 2 +- src/plugins/dive/Makefile.in | 12 +----------- src/plugins/dive/build.ml | 2 +- src/plugins/dive/build.mli | 2 +- src/plugins/dive/callstack.ml | 2 +- src/plugins/dive/callstack.mli | 2 +- src/plugins/dive/configure.ac | 2 +- src/plugins/dive/graph_types.mli | 2 +- .../dive/headers/close-source/LGPL.Dive | 19 ------------------- src/plugins/dive/headers/header_spec.txt | 17 ----------------- .../dive/headers/open-source/LGPL.Dive | 19 ------------------- src/plugins/dive/imprecision_graph.ml | 2 +- src/plugins/dive/imprecision_graph.mli | 2 +- src/plugins/dive/main.ml | 2 +- src/plugins/dive/node_kind.ml | 2 +- src/plugins/dive/node_kind.mli | 2 +- src/plugins/dive/self.ml | 2 +- src/plugins/dive/self.mli | 2 +- src/plugins/dive/server_interface.ml | 2 +- src/plugins/dive/server_interface.mli | 2 +- src/plugins/dive/simple_deps.ml | 2 +- 22 files changed, 35 insertions(+), 83 deletions(-) delete mode 100644 src/plugins/dive/headers/close-source/LGPL.Dive delete mode 100644 src/plugins/dive/headers/header_spec.txt delete mode 100644 src/plugins/dive/headers/open-source/LGPL.Dive diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 32832478186..7fdecae8316 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -763,6 +763,23 @@ src/plugins/constant_propagation/propagationParameters.ml: CEA_LGPL_OR_PROPRIETA src/plugins/constant_propagation/propagationParameters.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/constant_propagation/api.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/constant_propagation/api.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/build.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/graph_types.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/imprecision_graph.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/imprecision_graph.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/dive/server_interface.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/from/From.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/from/callwise.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/from/callwise.mli: CEA_LGPL_OR_PROPRIETARY diff --git a/src/plugins/dive/Dive.mli b/src/plugins/dive/Dive.mli index c6933a73bc1..182bc40a8e1 100644 --- a/src/plugins/dive/Dive.mli +++ b/src/plugins/dive/Dive.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in index d2a945eff91..c4b5b76d4eb 100644 --- a/src/plugins/dive/Makefile.in +++ b/src/plugins/dive/Makefile.in @@ -1,6 +1,6 @@ ########################################################################## # # -# This file is part of the Frama-C plug-in `Dive'. # +# This file is part of Frama-C. # # # # Copyright (C) 2007-2020 # # CEA (Commissariat à l'énergie atomique et aux énergies # @@ -53,16 +53,6 @@ PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure include $(FRAMAC_SHARE)/Makefile.dynamic -########## -# Header # -########## - -headers:: - @echo "Applying Headers..." - headache -c licence/headache_config.txt -h licence/LGPL_HEADER \ - *.ml *.mli \ - Makefile.in configure.ac - ##################################### # Regenerating the Makefile on need # ##################################### diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index b22b27cca53..236582ae1ad 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli index 2de92ccbd83..990e3e6f89c 100644 --- a/src/plugins/dive/build.mli +++ b/src/plugins/dive/build.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml index d61097fd535..8b25837a113 100644 --- a/src/plugins/dive/callstack.ml +++ b/src/plugins/dive/callstack.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli index f8073bfcf77..48d3a417b96 100644 --- a/src/plugins/dive/callstack.mli +++ b/src/plugins/dive/callstack.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/configure.ac b/src/plugins/dive/configure.ac index fe369c0ccd8..dddb5ed24e2 100644 --- a/src/plugins/dive/configure.ac +++ b/src/plugins/dive/configure.ac @@ -1,6 +1,6 @@ ########################################################################## # # -# This file is part of the Frama-C plug-in `Dive'. # +# This file is part of Frama-C. # # # # Copyright (C) 2007-2020 # # CEA (Commissariat à l'énergie atomique et aux énergies # diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli index cfd8a04aa9a..f1920b35026 100644 --- a/src/plugins/dive/graph_types.mli +++ b/src/plugins/dive/graph_types.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/headers/close-source/LGPL.Dive b/src/plugins/dive/headers/close-source/LGPL.Dive deleted file mode 100644 index 367db7ff3b1..00000000000 --- a/src/plugins/dive/headers/close-source/LGPL.Dive +++ /dev/null @@ -1,19 +0,0 @@ - -This file is part of the Frama-C plug-in `Dive'. - -Copyright (C) 2007-2020 - 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). - diff --git a/src/plugins/dive/headers/header_spec.txt b/src/plugins/dive/headers/header_spec.txt deleted file mode 100644 index b6d32434c6e..00000000000 --- a/src/plugins/dive/headers/header_spec.txt +++ /dev/null @@ -1,17 +0,0 @@ -build.ml: LGPL.Dive -build.mli: LGPL.Dive -callstack.ml: LGPL.Dive -callstack.mli: LGPL.Dive -configure.ac: LGPL.Dive -Dive.mli: LGPL.Dive -graph_types.mli: LGPL.Dive -imprecision_graph.ml: LGPL.Dive -imprecision_graph.mli: LGPL.Dive -main.ml: LGPL.Dive -Makefile.in: LGPL.Dive -node_kind.ml: LGPL.Dive -node_kind.mli: LGPL.Dive -self.ml: LGPL.Dive -self.mli: LGPL.Dive -server_interface.ml: LGPL.Dive -server_interface.mli: LGPL.Dive diff --git a/src/plugins/dive/headers/open-source/LGPL.Dive b/src/plugins/dive/headers/open-source/LGPL.Dive deleted file mode 100644 index 367db7ff3b1..00000000000 --- a/src/plugins/dive/headers/open-source/LGPL.Dive +++ /dev/null @@ -1,19 +0,0 @@ - -This file is part of the Frama-C plug-in `Dive'. - -Copyright (C) 2007-2020 - 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). - diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml index a2afcae0b51..2ebd12cf182 100644 --- a/src/plugins/dive/imprecision_graph.ml +++ b/src/plugins/dive/imprecision_graph.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli index e3194bab010..dae5176aff1 100644 --- a/src/plugins/dive/imprecision_graph.mli +++ b/src/plugins/dive/imprecision_graph.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml index 373bab6c9a5..7638783ac20 100644 --- a/src/plugins/dive/main.ml +++ b/src/plugins/dive/main.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml index e0335300fb1..5c6b5979cf3 100644 --- a/src/plugins/dive/node_kind.ml +++ b/src/plugins/dive/node_kind.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/node_kind.mli b/src/plugins/dive/node_kind.mli index 606d161a8fb..a65055305c6 100644 --- a/src/plugins/dive/node_kind.mli +++ b/src/plugins/dive/node_kind.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml index ec9312e31cb..aed894bef8f 100644 --- a/src/plugins/dive/self.ml +++ b/src/plugins/dive/self.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli index ff3819ddf14..f15ce3c96bd 100644 --- a/src/plugins/dive/self.mli +++ b/src/plugins/dive/self.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml index cf378625c7d..c80a64405a8 100644 --- a/src/plugins/dive/server_interface.ml +++ b/src/plugins/dive/server_interface.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/server_interface.mli b/src/plugins/dive/server_interface.mli index acb8b1fda94..6b8cd770d93 100644 --- a/src/plugins/dive/server_interface.mli +++ b/src/plugins/dive/server_interface.mli @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2020 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) diff --git a/src/plugins/dive/simple_deps.ml b/src/plugins/dive/simple_deps.ml index f67f9e05d81..3bb0950359e 100644 --- a/src/plugins/dive/simple_deps.ml +++ b/src/plugins/dive/simple_deps.ml @@ -1,6 +1,6 @@ (**************************************************************************) (* *) -(* This file is part of the Frama-C plug-in `Dive'. *) +(* This file is part of Frama-C. *) (* *) (* Copyright (C) 2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) -- GitLab