From e5a5daa7124e2c19958ee98ecd67ae5cbc12b0cd Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Wed, 1 Jun 2022 17:07:58 +0200 Subject: [PATCH] [headers] fixes some headers --- bin/build-src-distrib.sh | 21 ++++++++++ bin/check-reference-configuration.sh | 21 ++++++++++ bin/check_newlines.ml | 22 ++++++++++ bin/git.sh | 22 ++++++++++ bin/indent.sh | 22 ++++++++++ bin/isutf8.ml | 22 ++++++++++ bin/lint.sh | 22 ++++++++++ bin/merge-master.sh | 21 ++++++++++ bin/migration_scripts/git-replace.sh | 22 ++++++++++ bin/rebuild.sh | 22 ++++++++++ bin/shift_oracles.sh | 21 ++++++++++ bin/update_api_doc.sh | 21 ++++++++++ bin/wp-qualif.sh | 22 ++++++++++ devel_tools/docker/Makefile | 22 ++++++++++ devel_tools/duplicates.pl | 21 ++++++++++ devel_tools/ocamldep_transitive_closure.ml | 22 ++++++++++ devel_tools/size.mli | 5 ++- doc/aorai/Makefile | 25 +++++++++++ doc/developer/Makefile | 15 +++++-- doc/developer/check_api/Makefile | 15 +++++-- .../check_api/check_index_grammar.mly | 15 +++++-- doc/developer/tutorial/viewcfg/Makefile | 15 +++++-- doc/hevea.css | 22 ++++++++++ doc/metrics/Makefile | 22 ++++++++++ doc/pandoc/style.css | 2 +- doc/pdg/Makefile | 22 ++++++++++ doc/release/Makefile | 15 +++++-- doc/rte/Makefile | 22 ++++++++++ doc/scope/Makefile | 22 ++++++++++ doc/slicing/Makefile | 22 ++++++++++ doc/userman/Makefile | 22 ++++++++++ headers/check-headers.sh | 13 +++++- headers/close-source/CEA_PR_LGPL | 21 ++++++++++ headers/close-source/XL_COMPCERT | 10 +++++ headers/headache.sh | 13 +++++- headers/headache_config.txt | 42 ++++++++++++++++++- headers/open-source/CEA_PR_LGPL | 21 ++++++++++ headers/open-source/XL_COMPCERT | 10 +++++ headers/updates-headers.sh | 13 +++++- ivette/Makefile.distrib | 22 ++++++++++ ivette/distrib.sh | 22 ++++++++++ ivette/ivette-macos.sh | 21 ++++++++++ ivette/src/dome/template/dome-pull.sh | 22 ++++++++++ ivette/src/dome/template/dome-push.sh | 22 ++++++++++ ivette/src/dome/template/export.sh | 21 ++++++++++ ivette/src/dome/template/makefile | 22 ++++++++++ .../src/dome/template/makefile.app.packages | 22 ++++++++++ ivette/src/dome/template/makefile.packages | 22 ++++++++++ ivette/src/dome/template/package.sh | 21 ++++++++++ ivette/src/dome/template/update.sh | 21 ++++++++++ nix/frama-c-public/ssh.sh | 21 ++++++++++ nix/frama-ci.sh | 21 ++++++++++ ptests/check_oracles.sh | 21 ++++++++++ share/_frama-c.zsh | 21 ++++++++++ share/analysis-scripts/bench-sqlite.sh | 21 ++++++++++ share/analysis-scripts/clone.sh | 21 ++++++++++ share/analysis-scripts/cmd-dep.sh | 22 ++++++++++ share/analysis-scripts/concat-csv.sh | 21 ++++++++++ share/analysis-scripts/fc_stubs.c | 22 ++++++++++ share/analysis-scripts/function_finder.py | 3 +- share/analysis-scripts/parse-coverage.sh | 21 ++++++++++ share/analysis-scripts/plot.sh | 22 ++++++++++ .../script_for_creduce_fatal.sh | 21 ++++++++++ .../script_for_creduce_non_fatal.sh | 21 ++++++++++ share/analysis-scripts/template.mk | 22 ++++++++++ src/plugins/value/gen-api.sh | 22 ++++++++++ src/plugins/value/gen_test_config.sh | 21 ++++++++++ src/plugins/value/test.assert.sh | 22 ++++++++++ src/plugins/value/test.sh | 22 ++++++++++ src/plugins/value/vtests.sh | 21 ++++++++++ src/plugins/wp/doc/MakeDoc | 22 ++++++++++ src/plugins/wp/doc/coqdoc/Makefile | 24 ++++++++++- .../wp/doc/coqdoc/coq2tex/coq2html.mll | 26 ++++++------ .../wp/doc/coqdoc/coq2tex/coq2latex.mll | 26 ++++++------ src/plugins/wp/doc/manual/Makefile | 22 ++++++++++ src/plugins/wp/doc/ocamldoc.css | 22 ++++++++++ 76 files changed, 1485 insertions(+), 54 deletions(-) create mode 100644 headers/close-source/CEA_PR_LGPL create mode 100644 headers/close-source/XL_COMPCERT create mode 100644 headers/open-source/CEA_PR_LGPL create mode 100644 headers/open-source/XL_COMPCERT diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh index eec32ca3d27..73a586aed81 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 e9136564288..6095ffc385b 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 4524bdc80d9..29e3c5a2dad 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 18e931bd054..f5b81e49bcf 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 9c402daacff..68ad76654dd 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 5950a0c6b82..0e775f13502 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 797b61e433c..e1cb6e6a76f 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 5664dbaeb74..28ae15023e5 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 d32b5d6bb15..cf96d736983 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 f8d3346fab8..f50cecdb02c 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 1a8cba4f5da..0b9ea6cd135 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 80313ff753f..9601c2544f1 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 ae239fbadbe..418cabf7b37 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 04d1c97261b..c6cae592a0f 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 ba91fcccfdd..019ac1e21d1 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/ocamldep_transitive_closure.ml b/devel_tools/ocamldep_transitive_closure.ml index 9f7e3835730..363d14205bb 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 1146e6da562..037d5b4a707 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 515b0938ec0..750c6c23f14 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 eb5f0c6b5a5..80c5b48ec69 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/check_api/Makefile b/doc/developer/check_api/Makefile index e2219705a59..ac8885a7729 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 3db1a867b46..26b5b76ac8f 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/tutorial/viewcfg/Makefile b/doc/developer/tutorial/viewcfg/Makefile index a143ee77a73..67918576782 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/hevea.css b/doc/hevea.css index c549e52ced4..fe81db6e649 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 cf7cd6b60d7..e998a3da92f 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 f32fd1e1662..18398ee443a 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 de8bc630742..74b8af4e70b 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 0c698b87a88..7797c93e029 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 c3d71f538c5..2c6a25c25ee 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 3e14c50237d..ac55e30f199 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 b09932ac72d..673e0ac1c9a 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 43397136045..0b98372bc4d 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/headers/check-headers.sh b/headers/check-headers.sh index 6846de19e9b..c0b5be588ad 100755 --- a/headers/check-headers.sh +++ b/headers/check-headers.sh @@ -7,8 +7,17 @@ # 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/headers/close-source/CEA_PR_LGPL b/headers/close-source/CEA_PR_LGPL new file mode 100644 index 00000000000..03295570cfc --- /dev/null +++ b/headers/close-source/CEA_PR_LGPL @@ -0,0 +1,21 @@ + +This file is part of Frama-C. + +Copyright (C) 2008-2011 + Pierre Roux + +Copyright (C) 2009-2022 + CEA LIST + +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/headers/close-source/XL_COMPCERT b/headers/close-source/XL_COMPCERT new file mode 100644 index 00000000000..e8e6bf9af88 --- /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/headache.sh b/headers/headache.sh index 2eb900248cf..534bae2a5d2 100755 --- a/headers/headache.sh +++ b/headers/headache.sh @@ -7,8 +7,17 @@ # 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/headers/headache_config.txt b/headers/headache_config.txt index 8ca8829fd00..3f188ea4f7a 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,23 @@ | "frama-c.debug" -> frame open:"#" line:"#" close:"#" | ".*frama-c.debug" -> skip 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/open-source/CEA_PR_LGPL b/headers/open-source/CEA_PR_LGPL new file mode 100644 index 00000000000..03295570cfc --- /dev/null +++ b/headers/open-source/CEA_PR_LGPL @@ -0,0 +1,21 @@ + +This file is part of Frama-C. + +Copyright (C) 2008-2011 + Pierre Roux + +Copyright (C) 2009-2022 + CEA LIST + +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/headers/open-source/XL_COMPCERT b/headers/open-source/XL_COMPCERT new file mode 100644 index 00000000000..e8e6bf9af88 --- /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 index 9041bac49be..ad3398d4ca7 100755 --- a/headers/updates-headers.sh +++ b/headers/updates-headers.sh @@ -7,8 +7,17 @@ # 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/ivette/Makefile.distrib b/ivette/Makefile.distrib index 0f933db596e..aba92d615b4 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 38012edac62..bf3f52392ee 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/ivette-macos.sh b/ivette/ivette-macos.sh index 8e11dedfccc..a07d3b365c6 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 Ivette.app --args --cwd $PWD $* diff --git a/ivette/src/dome/template/dome-pull.sh b/ivette/src/dome/template/dome-pull.sh index b579cf35a1a..7bec6736c8a 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 60816ed9ecb..94fd495fbb9 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 ea5dc39d5fe..6cdae2a4802 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 376d32c4fad..29df4121517 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 58aa6a3ad51..04b26ffe0ed 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 72e46b98842..4b5bbafac90 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 58e4428ffb8..5cadbb74440 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 56d22295ef2..d48e589170a 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/frama-c-public/ssh.sh b/nix/frama-c-public/ssh.sh index faeb299c681..55e5887a407 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 b4deee0abc1..5db2f7357c2 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 a7bb568c1f5..91e7177f6b9 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 8dda747e2e0..8a4a6b2a743 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 954cb0e9f84..17eaa35c3d2 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 0ed6b8553c2..c8ee9c96ed9 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 d045b1cf563..f7ed9168d22 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 8079d300455..96d87aeed87 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 fad866f2160..2c9698c18e4 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 22af511f790..381dd64b29d 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 13ef4141765..ade4f113bca 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 0db4d1ba284..bc68f1fef0e 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 a0fc2ba7b95..4a2e8b9ef3d 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 d886aeaba29..7ad71d593db 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 689b9eab61c..54cdd1332ac 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/value/gen-api.sh b/src/plugins/value/gen-api.sh index d00c16fdd4a..e626fff905e 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 b1085f08686..7d2f84316e0 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 38049b28c4c..382cdce643d 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 1c19540871f..54e88f0a2fb 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/vtests.sh b/src/plugins/value/vtests.sh index 14cd7c69237..0137eaf4c6a 100755 --- a/src/plugins/value/vtests.sh +++ b/src/plugins/value/vtests.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). # +# # +########################################################################## if [ -z ${TARGETS+x} ]; then TARGETS="float value idct builtins" diff --git a/src/plugins/wp/doc/MakeDoc b/src/plugins/wp/doc/MakeDoc index b646e4383b9..53d34f0f625 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 a0a35db3e79..92c3db78d1c 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 21d22600021..230de710f3b 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 78cb86b014a..0d16708fe72 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 1f64775fdcf..f1e5b1b10df 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 61e22cc8016..2dd72db72c8 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 { -- GitLab