diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh index eec32ca3d2727b4af96d0008f390c2a38fdecf28..73a586aed81b611d5625e3d8f9c6bd92b212b51f 100755 --- a/bin/build-src-distrib.sh +++ b/bin/build-src-distrib.sh @@ -1,4 +1,25 @@ #! /usr/bin/env bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## set -u diff --git a/bin/check-reference-configuration.sh b/bin/check-reference-configuration.sh index e91365642881b711352f863c119deecc00de901e..6095ffc385bf0c6f31ae5a25dd1ec3f32844e3fc 100755 --- a/bin/check-reference-configuration.sh +++ b/bin/check-reference-configuration.sh @@ -1,4 +1,25 @@ #!/bin/bash -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # Displays the current working configuration of OCaml dependencies of Frama-C, # comparing them with the one in `reference-configuration.md`. diff --git a/bin/check_newlines.ml b/bin/check_newlines.ml index 4524bdc80d9d1e14edd919acb4de2e4db746a7eb..29e3c5a2dadb2f66097b57bb68010435ce1bf968 100644 --- a/bin/check_newlines.ml +++ b/bin/check_newlines.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2022 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + module StringSet = Set.Make(String) (* returns true for empty files *) diff --git a/bin/git.sh b/bin/git.sh index 18e931bd054a7e66969122c00a9def62d2048bf9..f5b81e49bcf8b17404963987b204acb9cddf47e1 100755 --- a/bin/git.sh +++ b/bin/git.sh @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + ACTION="$*" if [ "$ACTION" == "" ] diff --git a/bin/indent.sh b/bin/indent.sh index 9c402daacff0384024c5a86f412f0a8169488007..68ad76654dd84b51ad583c3d28f218d0c47513e6 100755 --- a/bin/indent.sh +++ b/bin/indent.sh @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # Help case "$1" in diff --git a/bin/isutf8.ml b/bin/isutf8.ml index 5950a0c6b826126676304be8212ae28b53c0cfdb..0e775f13502710afea395fa9aadb2686ca72b40d 100644 --- a/bin/isutf8.ml +++ b/bin/isutf8.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2022 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + module StringSet = Set.Make(String) exception False diff --git a/bin/lint.sh b/bin/lint.sh index 797b61e433cb7aa56eac155c2bb4f704e16eb866..e1cb6e6a76f901ee553413d435145dde4ca2722d 100755 --- a/bin/lint.sh +++ b/bin/lint.sh @@ -1,4 +1,26 @@ #!/bin/sh +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + set -e # -------------------------------------------------------------------------- diff --git a/bin/merge-master.sh b/bin/merge-master.sh index 5664dbaeb74bd486648594e7817332a9d3e27f15..28ae15023e585ccbe7228f98f8f563eb106403ea 100755 --- a/bin/merge-master.sh +++ b/bin/merge-master.sh @@ -1,4 +1,25 @@ #!/bin/sh +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## if test -z "$1"; then echo "Syntax: $0 <release name>"; diff --git a/bin/migration_scripts/git-replace.sh b/bin/migration_scripts/git-replace.sh index d32b5d6bb15c50f59e013b9479ba0d06837bebe8..cf96d73698372ae449f7e54b85954ab29aa3dabd 100755 --- a/bin/migration_scripts/git-replace.sh +++ b/bin/migration_scripts/git-replace.sh @@ -1,4 +1,26 @@ #!/bin/sh -u +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + git replace fbe13264f29d59b5388096281f98f05116b17f76 8e6afe71d01b1bc4f4d778a5326d0a2e1f2998b3 git replace cef5bf08946dccaf6b51e515eea76443976e6550 8bd30e2d47ffab72507d5ea291bdbd9f0fea0384 git replace 32d8c505805a060e5112c104ea0ffe06c6df308d 3fb543f7adaac4c2942c45f0244f270c86c23605 diff --git a/bin/rebuild.sh b/bin/rebuild.sh index f8d3346fab80481cfd8a6eaa73f3f1d92765a6eb..f50cecdb02c21de5dcabda7ec3df1ad1655cabe2 100755 --- a/bin/rebuild.sh +++ b/bin/rebuild.sh @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + make -k clean find src \( -name "*.cm*" -or -name "*.o" \) -delete -print rm -fr config.status autom4te.cache/ diff --git a/bin/shift_oracles.sh b/bin/shift_oracles.sh index 1a8cba4f5da6526ab0a05fd6050b8ac3afb0efc9..0b9ea6cd135d8506fcfe381021c58bd616db2051 100755 --- a/bin/shift_oracles.sh +++ b/bin/shift_oracles.sh @@ -1,4 +1,25 @@ #!/bin/bash -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # [shift_oracles.sh [commit] source.c -- test1.oracle test2.oracle ...] # modifies the set of oracles w.r.t. [source.c], using `git diff` to diff --git a/bin/update_api_doc.sh b/bin/update_api_doc.sh index 80313ff753fa109745439f24d9dd21e856834089..9601c2544f152459bbfb8af60514b3a2bb8c489a 100755 --- a/bin/update_api_doc.sh +++ b/bin/update_api_doc.sh @@ -1,4 +1,25 @@ #!/bin/sh +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## next=$1 diff --git a/bin/wp-qualif.sh b/bin/wp-qualif.sh index ae239fbadbe2bcd440bac1a4cd149dcc391e1d13..418cabf7b371c8ac91a44196bdcf23d68fab7af3 100644 --- a/bin/wp-qualif.sh +++ b/bin/wp-qualif.sh @@ -1,2 +1,24 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + export FRAMAC_WP_CACHE=update export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile index 04d1c97261bf1c50ddebd680e3f9f7458ddffaca..c6cae592a0f241287c37ea2fba3a5c897463c8ff 100644 --- a/devel_tools/docker/Makefile +++ b/devel_tools/docker/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + .PHONY: *-stripped *-gui push-* help: diff --git a/devel_tools/duplicates.pl b/devel_tools/duplicates.pl index ba91fcccfdd869819e6ed19491723f03f9af9cfa..019ac1e21d113b188e988f92d3aedecaa287521b 100755 --- a/devel_tools/duplicates.pl +++ b/devel_tools/duplicates.pl @@ -1,4 +1,25 @@ #!/usr/bin/env perl +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # Finds duplicate adjacent words. diff --git a/devel_tools/ocamldep_transitive_closure.ml b/devel_tools/ocamldep_transitive_closure.ml index 9f7e383573055866bf377d20dd4fd2aaccb0fb92..363d14205bb5a6ff0829e739abfe61e7015a2429 100644 --- a/devel_tools/ocamldep_transitive_closure.ml +++ b/devel_tools/ocamldep_transitive_closure.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2022 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + let depend_files = ref [] let add_deps s = depend_files:= s :: !depend_files diff --git a/devel_tools/size.mli b/devel_tools/size.mli index 1146e6da562d9c897324a476d9d9b1f19d08b820..037d5b4a707c50988c444da0c7179ff193cc5a3a 100644 --- a/devel_tools/size.mli +++ b/devel_tools/size.mli @@ -4,13 +4,16 @@ (* *) (* This software is free software; you can redistribute it and/or *) (* modify it under the terms of the GNU Library General Public *) -(* License version 2, with the special exception on linking *) +(* License version 2.1, with the special exception on linking *) (* described in file LICENSE. *) (* *) (* This software is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) +(* File modified by CEA (Commissariat à l'énergie atomique et aux *) +(* énergies alternatives). *) +(* *) (**************************************************************************) (*i $Id: size.mli,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*) diff --git a/doc/aorai/Makefile b/doc/aorai/Makefile index 515b0938ec06b9de1bd34f5ad8c4e9f97b161cca..750c6c23f14ea14be2145c360c8613e03c85f89c 100644 --- a/doc/aorai/Makefile +++ b/doc/aorai/Makefile @@ -1,3 +1,28 @@ +########################################################################## +# # +# This file is part of Aorai plug-in of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# INRIA (Institut National de Recherche en Informatique et en # +# Automatique) # +# INSA (Institut National des Sciences Appliquees) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + .PHONY: all clean DWNLDDIR=../manuals diff --git a/doc/developer/Makefile b/doc/developer/Makefile index eb5f0c6b5a53b6139548bf6d9ca0565bf0d57c2d..80c5b48ec69a2e9504a09bdda30be81a32f50d47 100644 --- a/doc/developer/Makefile +++ b/doc/developer/Makefile @@ -2,12 +2,21 @@ # # # This file is part of Frama-C. # # # -# Copyright (C) 2007-2021 # +# Copyright (C) 2007-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # -# All rights reserved. # -# Contact CEA LIST for licensing. # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # # # ########################################################################## diff --git a/doc/developer/check_api/Makefile b/doc/developer/check_api/Makefile index e2219705a5916e3457881ef319d1a7be13d26059..ac8885a77293456c23af39bb71fcfd03a516cbf9 100644 --- a/doc/developer/check_api/Makefile +++ b/doc/developer/check_api/Makefile @@ -2,12 +2,21 @@ # # # This file is part of Frama-C. # # # -# Copyright (C) 2007-2021 # +# Copyright (C) 2007-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # -# All rights reserved. # -# Contact CEA LIST for licensing. # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # # # ########################################################################## diff --git a/doc/developer/check_api/check_index_grammar.mly b/doc/developer/check_api/check_index_grammar.mly index 3db1a867b460006aeba5f6b15d8e91ae5b59c960..26b5b76ac8f08841cbc98cd63664b34fd675213b 100644 --- a/doc/developer/check_api/check_index_grammar.mly +++ b/doc/developer/check_api/check_index_grammar.mly @@ -2,12 +2,21 @@ /* */ /* This file is part of Frama-C. */ /* */ -/* Copyright (C) 2007-2021 */ +/* Copyright (C) 2007-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ -/* All rights reserved. */ -/* Contact CEA LIST for licensing. */ +/* you can redistribute it and/or modify it under the terms of the GNU */ +/* Lesser General Public License as published by the Free Software */ +/* Foundation, version 2.1. */ +/* */ +/* It is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU Lesser General Public License for more details. */ +/* */ +/* See the GNU Lesser General Public License version 2.1 */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ /* */ /**************************************************************************/ diff --git a/doc/developer/tutorial/viewcfg/Makefile b/doc/developer/tutorial/viewcfg/Makefile index a143ee77a73cdb3b65f71e5c0323664f7444f931..67918576782a6915848671cabc6c6808eebba8d5 100644 --- a/doc/developer/tutorial/viewcfg/Makefile +++ b/doc/developer/tutorial/viewcfg/Makefile @@ -2,12 +2,21 @@ # # # This file is part of Frama-C. # # # -# Copyright (C) 2007-2021 # +# Copyright (C) 2007-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # -# All rights reserved. # -# Contact CEA LIST for licensing. # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # # # ########################################################################## diff --git a/doc/hevea.css b/doc/hevea.css index c549e52ced4e470e2dc4385c745aa71969e2f95b..fe81db6e64960b94032e68a422f3f16176b4a649 100644 --- a/doc/hevea.css +++ b/doc/hevea.css @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* This file is part of Frama-C. */ +/* */ +/* Copyright (C) 2007-2022 */ +/* CEA (Commissariat à l'énergie atomique et aux énergies */ +/* alternatives) */ +/* */ +/* you can redistribute it and/or modify it under the terms of the GNU */ +/* Lesser General Public License as published by the Free Software */ +/* Foundation, version 2.1. */ +/* */ +/* It is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU Lesser General Public License for more details. */ +/* */ +/* See the GNU Lesser General Public License version 2.1 */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ +/**************************************************************************/ + html{ background: darkgrey; padding: 24px; diff --git a/doc/metrics/Makefile b/doc/metrics/Makefile index cf7cd6b60d7c1453e281bc04785fe05a439d2de6..e998a3da92f4dcf793ed28aba1ad6f50b38d49fb 100644 --- a/doc/metrics/Makefile +++ b/doc/metrics/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + .PHONY: default all clean TARGET = metrics.pdf diff --git a/doc/pandoc/style.css b/doc/pandoc/style.css index f32fd1e16621cfeb8f7367a3d83a1bf29570181b..18398ee443a0dce7d08bfcafeca107288b2b1423 100644 --- a/doc/pandoc/style.css +++ b/doc/pandoc/style.css @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-C. */ /* */ -/* Copyright (C) 2007-2021 */ +/* Copyright (C) 2007-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/doc/pdg/Makefile b/doc/pdg/Makefile index de8bc6307421bec04bd8fab929978e1191a8f78e..74b8af4e70b48417b982ac3781490c8ccad5418e 100644 --- a/doc/pdg/Makefile +++ b/doc/pdg/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + .PHONY: all clean all: main.pdf diff --git a/doc/release/Makefile b/doc/release/Makefile index 0c698b87a884f92a6cbfceb457a287f2f690fd7e..7797c93e029f967707f40d3cf89fe92f858326de 100644 --- a/doc/release/Makefile +++ b/doc/release/Makefile @@ -2,12 +2,21 @@ # # # This file is part of Frama-C. # # # -# Copyright (C) 2007-2021 # +# Copyright (C) 2007-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # -# All rights reserved. # -# Contact CEA LIST for licensing. # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # # # ########################################################################## diff --git a/doc/rte/Makefile b/doc/rte/Makefile index c3d71f538c537d4c9ccc072d7786205621c94034..2c6a25c25ee9686ed17cc8c56dee151223019b2b 100644 --- a/doc/rte/Makefile +++ b/doc/rte/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + .PHONY: all clean all: main.pdf diff --git a/doc/scope/Makefile b/doc/scope/Makefile index 3e14c50237d6411697cad872bdff9a1878a9c1a5..ac55e30f1991ffdb38612fdfcb1ee248d6e01ce8 100644 --- a/doc/scope/Makefile +++ b/doc/scope/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + #vide : pour ne pas utiliser de règles implicites .SUFFIXE: .PHONY: clean all debug diff --git a/doc/slicing/Makefile b/doc/slicing/Makefile index b09932ac72db4cf6512927e70d60debfe827927c..673e0ac1c9ae83a3294e668d0c6c00c92a20a7f6 100644 --- a/doc/slicing/Makefile +++ b/doc/slicing/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + .PHONY: all clean all: main.pdf diff --git a/doc/userman/Makefile b/doc/userman/Makefile index 433971360454eaafc0c43dccfe11c4a15f044b5e..0b98372bc4d1250d4113ea4827edf80d636b4edf 100644 --- a/doc/userman/Makefile +++ b/doc/userman/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # Require texi2pdf .DEFAULT_GOAL := all diff --git a/headers/check-headers.sh b/headers/check-headers.sh index 6846de19e9ba7363bba0b0b10a0f671bd7faabcb..c0b5be588ad2fc96e2ff6944504f3902963954f3 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 0000000000000000000000000000000000000000..03295570cfc43bc942288ad03439c060114d655d --- /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 0000000000000000000000000000000000000000..e8e6bf9af8871ef73e2d4bafb6aaa5a9af9f2c1f --- /dev/null +++ b/headers/close-source/XL_COMPCERT @@ -0,0 +1,10 @@ + The Compcert verified compiler + + Xavier Leroy, INRIA Paris-Rocquencourt + + Copyright Institut National de Recherche en Informatique et en + Automatique. All rights reserved. This file is distributed + under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 2 of the License, or + (at your option) any later version. This file is also distributed + under the terms of the INRIA Non-Commercial License Agreement. diff --git a/headers/headache.sh b/headers/headache.sh index 2eb900248cf06073b1f17e19616f80ca800e393e..534bae2a5d220fc9080bd8889a8b54f9cb957d49 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 8ca8829fd006a1e0d5bb98d7625dd86a90bb807f..3f188ea4f7ae176613c7216892f3887041786f2e 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 0000000000000000000000000000000000000000..03295570cfc43bc942288ad03439c060114d655d --- /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 0000000000000000000000000000000000000000..e8e6bf9af8871ef73e2d4bafb6aaa5a9af9f2c1f --- /dev/null +++ b/headers/open-source/XL_COMPCERT @@ -0,0 +1,10 @@ + The Compcert verified compiler + + Xavier Leroy, INRIA Paris-Rocquencourt + + Copyright Institut National de Recherche en Informatique et en + Automatique. All rights reserved. This file is distributed + under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 2 of the License, or + (at your option) any later version. This file is also distributed + under the terms of the INRIA Non-Commercial License Agreement. diff --git a/headers/updates-headers.sh b/headers/updates-headers.sh index 9041bac49bea0bda16ac9177961ea4f53bf8e3df..ad3398d4ca76eccf2de3aae0628ff8a0abbb933a 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 0f933db596ee0febd3157aa739797a507e871fee..aba92d615b478994627ab07a2b5afdf7dae9e98a 100644 --- a/ivette/Makefile.distrib +++ b/ivette/Makefile.distrib @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + HEADER_SPEC += ivette/./headers/header_spec.txt DISTRIB_FILES += ivette/.babelrc DISTRIB_FILES += ivette/.dome-pkg-app.lock diff --git a/ivette/distrib.sh b/ivette/distrib.sh index 38012edac621ff293d5ea0b1f3964f68d9adc5a4..bf3f52392ee8af21f0f2d32e441a1dec2d072b6f 100755 --- a/ivette/distrib.sh +++ b/ivette/distrib.sh @@ -1,4 +1,26 @@ #!/bin/sh -e +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Generate Files for Ivette Distribution # -------------------------------------------------------------------------- diff --git a/ivette/ivette-macos.sh b/ivette/ivette-macos.sh index 8e11dedfccca2c9f3e64980f0ceb19444f8d3ffd..a07d3b365c67ec522b7c1d64aed3b56d745a204c 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 b579cf35a1a2492f9cbe452e63abbc1a6dcf7244..7bec6736c8a5581a09075f1554fa0161efcb0efa 100755 --- a/ivette/src/dome/template/dome-pull.sh +++ b/ivette/src/dome/template/dome-pull.sh @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Pulling Dome Updates # -------------------------------------------------------------------------- diff --git a/ivette/src/dome/template/dome-push.sh b/ivette/src/dome/template/dome-push.sh index 60816ed9ecb0103ee1206d5c28db7ecada3737e5..94fd495fbb990453016fdc2ad2737e331c6e1bbe 100755 --- a/ivette/src/dome/template/dome-push.sh +++ b/ivette/src/dome/template/dome-push.sh @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Pulling Dome Updates # -------------------------------------------------------------------------- diff --git a/ivette/src/dome/template/export.sh b/ivette/src/dome/template/export.sh index ea5dc39d5fee0fabce5501431253fce3e19bf788..6cdae2a4802e0931935cf2ef7d504c4844b733ae 100755 --- a/ivette/src/dome/template/export.sh +++ b/ivette/src/dome/template/export.sh @@ -1,4 +1,25 @@ #!/bin/bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # -------------------------------------------------------------------------- # --- Export Dome API diff --git a/ivette/src/dome/template/makefile b/ivette/src/dome/template/makefile index 376d32c4fadf74c1c5bd08d3f8761a1821cb570d..29df4121517ee94ea96a1a9e90a0ea3e559bd768 100644 --- a/ivette/src/dome/template/makefile +++ b/ivette/src/dome/template/makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Main Makefile for building Dome applications # -------------------------------------------------------------------------- diff --git a/ivette/src/dome/template/makefile.app.packages b/ivette/src/dome/template/makefile.app.packages index 58aa6a3ad516168d48315864bfcf57376187f2b0..04b26ffe0ed0ff0757a23a0fc4b805fa32249742 100644 --- a/ivette/src/dome/template/makefile.app.packages +++ b/ivette/src/dome/template/makefile.app.packages @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Package Template Definitions # -------------------------------------------------------------------------- diff --git a/ivette/src/dome/template/makefile.packages b/ivette/src/dome/template/makefile.packages index 72e46b988425f140e03588c687b63acca23b4b39..4b5bbafac90e47fcfbee33487b0339ff7de43452 100644 --- a/ivette/src/dome/template/makefile.packages +++ b/ivette/src/dome/template/makefile.packages @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Packages Definitions for Dome environment --- # -------------------------------------------------------------------------- diff --git a/ivette/src/dome/template/package.sh b/ivette/src/dome/template/package.sh index 58e4428ffb8b421a8c3c99266057dbb0962bc1fe..5cadbb7444030b1dfb0cec0a82f6591554fe1bdd 100755 --- a/ivette/src/dome/template/package.sh +++ b/ivette/src/dome/template/package.sh @@ -1,4 +1,25 @@ #!/bin/sh +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # -------------------------------------------------------------------------- # --- Compute mode diff --git a/ivette/src/dome/template/update.sh b/ivette/src/dome/template/update.sh index 56d22295ef24fa4f37c19a100797c6005561921d..d48e589170acc09d3e9bbb52e76d377912e51574 100755 --- a/ivette/src/dome/template/update.sh +++ b/ivette/src/dome/template/update.sh @@ -1,4 +1,25 @@ #!/bin/sh +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # -------------------------------------------------------------------------- # --- Update Templated File (merge with user modifications) diff --git a/nix/frama-c-public/ssh.sh b/nix/frama-c-public/ssh.sh index faeb299c681d47c6abdc79ffafbde0a2b1ec9ad9..55e5887a4070163f5243a49a71377267f8d14f7a 100755 --- a/nix/frama-c-public/ssh.sh +++ b/nix/frama-c-public/ssh.sh @@ -1,4 +1,25 @@ #!/bin/sh -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## PWD=$(dirname $0) diff --git a/nix/frama-ci.sh b/nix/frama-ci.sh index b4deee0abc1543e01c82d3c6c92d9b0045b26d77..5db2f7357c230c6040e64d3d37d1e315c50e9f8a 100755 --- a/nix/frama-ci.sh +++ b/nix/frama-ci.sh @@ -1,4 +1,25 @@ #!/bin/sh -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## DIR=$(dirname $0) diff --git a/ptests/check_oracles.sh b/ptests/check_oracles.sh index a7bb568c1f52e01a6a31cc2a0478c30abdb3a003..91e7177f6b99224f6c04c156c8f435e729fd22bc 100755 --- a/ptests/check_oracles.sh +++ b/ptests/check_oracles.sh @@ -1,4 +1,25 @@ #!/bin/bash -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # Checks for extraneous, leftover oracle files that are no longer necessary. # Only reports files in plugins with a ptests_config file, and in directories diff --git a/share/_frama-c.zsh b/share/_frama-c.zsh index 8dda747e2e0f3e1d551c5cc0654e0aec1446eec3..8a4a6b2a743d35e495a3d06bd7f64118662e8b11 100644 --- a/share/_frama-c.zsh +++ b/share/_frama-c.zsh @@ -1,4 +1,25 @@ #compdef frama-c +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # ----------------------------------------------------------------------------- # zsh completion for Frama-C diff --git a/share/analysis-scripts/bench-sqlite.sh b/share/analysis-scripts/bench-sqlite.sh index 954cb0e9f84226309f3a60a98b542cffd5373fff..17eaa35c3d2ba5027982782c6ac3463da3806ecb 100755 --- a/share/analysis-scripts/bench-sqlite.sh +++ b/share/analysis-scripts/bench-sqlite.sh @@ -1,4 +1,25 @@ #!/bin/bash -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## database="benchmark-results.db" stats="$1" diff --git a/share/analysis-scripts/clone.sh b/share/analysis-scripts/clone.sh index 0ed6b8553c2144fb94fb9cd8f3260f39b65212d9..c8ee9c96ed909f15822a2eb038d676fa067d90c2 100755 --- a/share/analysis-scripts/clone.sh +++ b/share/analysis-scripts/clone.sh @@ -1,4 +1,25 @@ #!/bin/bash -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## git_hash="master" clone_dir="frama-c-clones" diff --git a/share/analysis-scripts/cmd-dep.sh b/share/analysis-scripts/cmd-dep.sh index d045b1cf56304862be02148358550bd8c6cb7dfc..f7ed9168d22dbb0c62fcd658b6b36f341075c304 100755 --- a/share/analysis-scripts/cmd-dep.sh +++ b/share/analysis-scripts/cmd-dep.sh @@ -1,4 +1,26 @@ #!/bin/bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + set -eu if [ $# -lt 1 ] diff --git a/share/analysis-scripts/concat-csv.sh b/share/analysis-scripts/concat-csv.sh index 8079d3004553a63ca9b20b93e8330016993bc2dc..96d87aeed87b2f45bf927251e11feffa01bf2e9e 100755 --- a/share/analysis-scripts/concat-csv.sh +++ b/share/analysis-scripts/concat-csv.sh @@ -1,4 +1,25 @@ #!/bin/bash -eu +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## set -o pipefail diff --git a/share/analysis-scripts/fc_stubs.c b/share/analysis-scripts/fc_stubs.c index fad866f2160ba5533c8658794a520c2bf0880962..2c9698c18e444f0ebe44055faa0450821faea0bb 100644 --- a/share/analysis-scripts/fc_stubs.c +++ b/share/analysis-scripts/fc_stubs.c @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* This file is part of Frama-C. */ +/* */ +/* Copyright (C) 2007-2022 */ +/* CEA (Commissariat à l'énergie atomique et aux énergies */ +/* alternatives) */ +/* */ +/* you can redistribute it and/or modify it under the terms of the GNU */ +/* Lesser General Public License as published by the Free Software */ +/* Foundation, version 2.1. */ +/* */ +/* It is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU Lesser General Public License for more details. */ +/* */ +/* See the GNU Lesser General Public License version 2.1 */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ +/**************************************************************************/ + // Stub for a main function which reads arguments from the command line, to be // used by the Eva plug-in. // This stub emulates non-deterministic input of up to 5 arguments, each up diff --git a/share/analysis-scripts/function_finder.py b/share/analysis-scripts/function_finder.py index 22af511f79059b026127417874d7509f98a309bb..381dd64b29da58e3660d7fa99ff2d3cfb7fb9bf8 100644 --- a/share/analysis-scripts/function_finder.py +++ b/share/analysis-scripts/function_finder.py @@ -1,9 +1,10 @@ +#!/usr/bin/env python3 # -*- coding: utf-8 -*- ########################################################################## # # # This file is part of Frama-C. # # # -# Copyright (C) 2007-2021 # +# Copyright (C) 2007-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/share/analysis-scripts/parse-coverage.sh b/share/analysis-scripts/parse-coverage.sh index 13ef4141765c34b099f2d8ae7409f562c788feed..ade4f113bcac226b8747bc589c539c5e612989db 100755 --- a/share/analysis-scripts/parse-coverage.sh +++ b/share/analysis-scripts/parse-coverage.sh @@ -1,4 +1,25 @@ #!/bin/bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## log_file=$1 stats_file=$2 diff --git a/share/analysis-scripts/plot.sh b/share/analysis-scripts/plot.sh index 0db4d1ba284bbdfa2e0ef26e8f6180e231cd2b1c..bc68f1fef0ede3dd8d4e95cda8d98fd810169bde 100755 --- a/share/analysis-scripts/plot.sh +++ b/share/analysis-scripts/plot.sh @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + target=$1 { diff --git a/share/analysis-scripts/script_for_creduce_fatal.sh b/share/analysis-scripts/script_for_creduce_fatal.sh index a0fc2ba7b9574f959ac738261ec7486cc5850c52..4a2e8b9ef3d1273f85e5640e7516a31c9c8fcea0 100644 --- a/share/analysis-scripts/script_for_creduce_fatal.sh +++ b/share/analysis-scripts/script_for_creduce_fatal.sh @@ -1,4 +1,25 @@ #!/bin/bash -e +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # Script to reduce a Frama-C crashing test case. diff --git a/share/analysis-scripts/script_for_creduce_non_fatal.sh b/share/analysis-scripts/script_for_creduce_non_fatal.sh index d886aeaba29099358e77597529d56ed6ff25dbad..7ad71d593dbb729b76aea893363088a147df8609 100644 --- a/share/analysis-scripts/script_for_creduce_non_fatal.sh +++ b/share/analysis-scripts/script_for_creduce_non_fatal.sh @@ -1,4 +1,25 @@ #!/bin/bash -e +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # Script to reduce a Frama-C non-crashing test case. diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk index 689b9eab61ccedee46cb8637eaaa9a51e3ad3f09..54cdd1332ac9cc37c6ceaae223ad16f217af1d79 100644 --- a/share/analysis-scripts/template.mk +++ b/share/analysis-scripts/template.mk @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # Makefile template for Frama-C/Eva case studies. # For details and usage information, see the Frama-C User Manual. diff --git a/src/plugins/value/gen-api.sh b/src/plugins/value/gen-api.sh index d00c16fdd4a1175ff780c5479fbb266043c7ba49..e626fff905e7d6920d563b961cacea3ad7a5166f 100755 --- a/src/plugins/value/gen-api.sh +++ b/src/plugins/value/gen-api.sh @@ -1,4 +1,26 @@ #!/usr/bin/env bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + set -eu printf '(** Eva public API. diff --git a/src/plugins/value/gen_test_config.sh b/src/plugins/value/gen_test_config.sh index b1085f0868634319e144ef3549f4518e100638ca..7d2f84316e0bf62436771e4f0af36314a427f049 100755 --- a/src/plugins/value/gen_test_config.sh +++ b/src/plugins/value/gen_test_config.sh @@ -1,4 +1,25 @@ #!/bin/bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## # This scripts creates the ptests config files for the alternative testing # configurations of Eva. You must create the tests/test_config and diff --git a/src/plugins/value/test.assert.sh b/src/plugins/value/test.assert.sh index 38049b28c4c8d1e44620765127875b5d1773f8db..382cdce643d939134c587a687c763e82f261746c 100755 --- a/src/plugins/value/test.assert.sh +++ b/src/plugins/value/test.assert.sh @@ -1,4 +1,26 @@ #!/bin/bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + export GCC3264=-m32 export FRAMAC3264=x86_32 #export GCC3264= diff --git a/src/plugins/value/test.sh b/src/plugins/value/test.sh index 1c19540871f090abbdb78f4ee1c4eda1b8f15625..54e88f0a2fb5d1e336be131bdcfc4cd977e576f3 100755 --- a/src/plugins/value/test.sh +++ b/src/plugins/value/test.sh @@ -1,4 +1,26 @@ #!/bin/bash +########################################################################## +# # +# This file is part of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat à l'énergie atomique et aux énergies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + export GCC3264=-m32 export FRAMAC3264=x86_32 #export GCC3264= diff --git a/src/plugins/value/vtests.sh b/src/plugins/value/vtests.sh index 14cd7c69237386cfa4f64debc1346bb98744b315..0137eaf4c6a18eac0248af5f9d82b438bbf130ce 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 b646e4383b9812cac2fde373dbbb3679487199d8..53d34f0f625a9e62b19c64eee2b304dbf050e323 100644 --- a/src/plugins/wp/doc/MakeDoc +++ b/src/plugins/wp/doc/MakeDoc @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of WP plug-in of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat a l'energie atomique et aux energies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- Resources --- # -------------------------------------------------------------------------- diff --git a/src/plugins/wp/doc/coqdoc/Makefile b/src/plugins/wp/doc/coqdoc/Makefile index a0a35db3e79cc52fe79a66e45c47a29ea641128b..92c3db78d1c683bd1e9b9ed36dcacd45c99eff44 100644 --- a/src/plugins/wp/doc/coqdoc/Makefile +++ b/src/plugins/wp/doc/coqdoc/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of WP plug-in of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat a l'energie atomique et aux energies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- WP User & Reference Manual --- # -------------------------------------------------------------------------- @@ -31,4 +53,4 @@ wpcoq.pdf: $(FRAMAC_DOC) $(TEX) .lib coq2latex.sty rubber -d wpcoq clean:: - rm -f .lib $(addsuffix .tex,$(COQL)) \ No newline at end of file + rm -f .lib $(addsuffix .tex,$(COQL)) diff --git a/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll b/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll index 21d22600021af223732b9a6a500bc145f0f9790d..230de710f3bed354453441f7ffb9a8a44acbe7fb 100644 --- a/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll +++ b/src/plugins/wp/doc/coqdoc/coq2tex/coq2html.mll @@ -1,17 +1,15 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) +(**************************************************************************) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(**************************************************************************) { open Printf diff --git a/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll b/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll index 78cb86b014a44c583ba4aeeca87114d9900aa5b0..0d16708fe724eae0c57464d3cd51c392900d0779 100644 --- a/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll +++ b/src/plugins/wp/doc/coqdoc/coq2tex/coq2latex.mll @@ -1,17 +1,15 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) +(**************************************************************************) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(**************************************************************************) { open Printf diff --git a/src/plugins/wp/doc/manual/Makefile b/src/plugins/wp/doc/manual/Makefile index 1f64775fdcf26a85f3802aeafe0434ddc1ff5220..f1e5b1b10dfcc4f310da006442df013170f40cb5 100644 --- a/src/plugins/wp/doc/manual/Makefile +++ b/src/plugins/wp/doc/manual/Makefile @@ -1,3 +1,25 @@ +########################################################################## +# # +# This file is part of WP plug-in of Frama-C. # +# # +# Copyright (C) 2007-2022 # +# CEA (Commissariat a l'energie atomique et aux energies # +# alternatives) # +# # +# you can redistribute it and/or modify it under the terms of the GNU # +# Lesser General Public License as published by the Free Software # +# Foundation, version 2.1. # +# # +# It is distributed in the hope that it will be useful, # +# but WITHOUT ANY WARRANTY; without even the implied warranty of # +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # +# GNU Lesser General Public License for more details. # +# # +# See the GNU Lesser General Public License version 2.1 # +# for more details (enclosed in the file licenses/LGPLv2.1). # +# # +########################################################################## + # -------------------------------------------------------------------------- # --- WP User & Reference Manual --- # -------------------------------------------------------------------------- diff --git a/src/plugins/wp/doc/ocamldoc.css b/src/plugins/wp/doc/ocamldoc.css index 61e22cc801685a15b9c78b7d38d3c54b0ec99e87..2dd72db72c834a5ab192511cd0a32eb84567f01c 100644 --- a/src/plugins/wp/doc/ocamldoc.css +++ b/src/plugins/wp/doc/ocamldoc.css @@ -1,3 +1,25 @@ +/**************************************************************************/ +/* */ +/* This file is part of WP plug-in of Frama-C. */ +/* */ +/* Copyright (C) 2007-2022 */ +/* CEA (Commissariat a l'energie atomique et aux energies */ +/* alternatives) */ +/* */ +/* you can redistribute it and/or modify it under the terms of the GNU */ +/* Lesser General Public License as published by the Free Software */ +/* Foundation, version 2.1. */ +/* */ +/* It is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU Lesser General Public License for more details. */ +/* */ +/* See the GNU Lesser General Public License version 2.1 */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ +/**************************************************************************/ + * { margin: 0; padding: 0 } body {