diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli index f804c3899dcfec14893ab0da738fa0ccd6e58a3c..29aea1b1ba1f4f8b0c199414ce2db39e86f7e7cc 100644 --- a/src/plugins/e-acsl/E_ACSL.mli +++ b/src/plugins/e-acsl/E_ACSL.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 935abd3c882ac4490d04a4d43abcae1718ce545c..6c10b16e3ae7d0469babc267d970397edf96e6a0 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -1,8 +1,8 @@ ########################################################################## # # -# This file is part of Frama-C. # +# This file is part of the Frama-C's E-ACSL plug-in. # # # -# Copyright (C) 2007-2018 # +# Copyright (C) 2012-2018 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # @@ -349,12 +349,19 @@ e-acsl-distrib-check: # Header # ########## -EACSL_CEA_LGPL_BARE= *.ml *.mli Makefile.in configure.ac share/e-acsl/*.[ch] \ - share/e-acsl/*/*.[ch] scripts/*.sh tests/print.ml man/e-acsl-gcc.sh.1 -EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) +ifneq ("$(FRAMAC_INTERNAL)","yes") EACSL_SPARETIMELABS=$(EACSL_PLUGIN_DIR)/share/e-acsl/e_acsl_printf.h +EACSL_SHARE_BARE= share/e-acsl/*.[ch] share/e-acsl/*/*.[ch] +EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE)) +EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE))) + +EACSL_CEA_LGPL_BARE= *.ml *.mli Makefile.in configure.ac \ + scripts/*.sh tests/print.ml man/e-acsl-gcc.sh.1 +EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \ + $(EACSL_CEA_SHARE) + # Files without header. contrib files keep their own header. EACSL_NOHEADER_BARE=INSTALL README VERSION license/* \ doc/Changelog doc/doxygen/doxygen.cfg.in .depend tests/test_config.in \ @@ -362,23 +369,24 @@ EACSL_NOHEADER_BARE=INSTALL README VERSION license/* \ EACSL_NOHEADER=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_NOHEADER_BARE)) -ifeq ("$(FRAMAC_INTERNAL)","yes") -CEA_LGPL_HEADER=$(FRAMAC_ROOT_SRCDIR)/headers/open-source/CEA_LGPL -# EACSL does not use hdrck mechanism -HEADER_EXCEPTIONS+=\ - $(wildcard $(EACSL_CEA_LGPL) $(EACSL_SPARETIMELABS) $(EACSL_NOHEADER)) -else -CEA_LGPL_HEADER=$(EACSL_PLUGIN_DIR)/license/CEA_LGPL -endif - +# valid values: open-source, close-source +EACSL_HEADERS?=open-source headers:: - @echo "Applying Headers..." + @echo "Applying $(EACSL_HEADERS) Headers..." headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \ - -h $(CEA_LGPL_HEADER) $(EACSL_CEA_LGPL) + -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/CEA_LGPL_OR_PROPRIETARY.E_ACSL \ + $(EACSL_CEA_LGPL) headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \ - -h $(EACSL_PLUGIN_DIR)/license/SPARETIMELABS \ + -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_SPARETIMELABS \ $(EACSL_SPARETIMELABS) + headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \ + -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_DLMALLOC \ + $(EACSL_PLUGIN_DIR)/contrib/libdlmalloc/dlmalloc.c + headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \ + -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_LIB_GMP \ + $(EACSL_PLUGIN_DIR)/contrib/libgmp/mini-gmp.[ch] +endif ################ # Generic part # diff --git a/src/plugins/e-acsl/builtins.ml b/src/plugins/e-acsl/builtins.ml index a88dd558e446801eeca9e580bebef22fbb40896d..45467db85bc2a5a59e5355efcff42e380860567a 100644 --- a/src/plugins/e-acsl/builtins.ml +++ b/src/plugins/e-acsl/builtins.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/builtins.mli b/src/plugins/e-acsl/builtins.mli index 367dd4143c8fa1bd431bf1e2140b2d57411a5b5e..7e1eb3f7b809988be06a54b4318cfd81dcc54f62 100644 --- a/src/plugins/e-acsl/builtins.mli +++ b/src/plugins/e-acsl/builtins.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac index 576b85a5f4611caa6cc1ee13a1ae6a15799efef4..d1376c9639ddaf40bf4fa31568d2fba89efa9822 100644 --- a/src/plugins/e-acsl/configure.ac +++ b/src/plugins/e-acsl/configure.ac @@ -1,8 +1,8 @@ ########################################################################## # # -# This file is part of Frama-C. # +# This file is part of the Frama-C's E-ACSL plug-in. # # # -# Copyright (C) 2007-2018 # +# Copyright (C) 2012-2018 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c b/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c index 98744d443fadc8c52dab25fc317429e08d95c466..0f9de38fb1e9e22b7351044f7915504cd5c049cd 100644 --- a/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c +++ b/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c @@ -1,21 +1,27 @@ -/* - This is a version (aka dlmalloc) of malloc/free/realloc written by - Doug Lea and released to the public domain, as explained at - http://creativecommons.org/publicdomain/zero/1.0/ Send questions, - comments, complaints, performance data, etc to dl@cs.oswego.edu - -* Version 2.8.6 Wed Aug 29 06:57:58 2012 Doug Lea - Note: There may be an updated version of this malloc obtainable at - ftp://gee.cs.oswego.edu/pub/misc/malloc.c - Check before installing! - -* This file has been modified by CEA for use together with Runtime Library +/**************************************************************************/ +/* */ +/* This is a version (aka dlmalloc) of malloc/free/realloc written by */ +/* Doug Lea and released to the public domain, as explained at */ +/* http://creativecommons.org/publicdomain/zero/1.0/ Send questions, */ +/* comments, complaints, performance data, etc to dl@cs.oswego.edu */ +/* */ +/* Version 2.8.6 Wed Aug 29 06:57:58 2012 Doug Lea */ +/* Note: There may be an updated version of this malloc obtainable at */ +/* ftp://gee.cs.oswego.edu/pub/misc/malloc.c */ +/* Check before installing! */ +/* */ +/* File modified by CEA (Commissariat à l'énergie atomique et aux */ +/* énergies alternatives). */ +/* */ +/**************************************************************************/ + +/* This file has been modified by CEA for use together with Runtime Library of the E-ACSL plugin of Frama-C. The changes introduced by CEA are limited to the following modifications: * Added declaration/definition of mspace_least_addr function - * Added functionality to modify prefix of `mspace_...` functions + * Added functionality to modify prefix of `mspace_...` functions. */ -* Quickstart +/* Quickstart This library is all in one file to simplify the most common usage: ftp it, compile it (-O3), and link it into another program. All of diff --git a/src/plugins/e-acsl/contrib/libgmp/mini-gmp.c b/src/plugins/e-acsl/contrib/libgmp/mini-gmp.c index 797c94aad776b68e0d83d5f6e826f4e33855c6b0..5764a9fcb9d6c1576a3b0a1ce7e3f778ceeaaee5 100644 --- a/src/plugins/e-acsl/contrib/libgmp/mini-gmp.c +++ b/src/plugins/e-acsl/contrib/libgmp/mini-gmp.c @@ -1,34 +1,41 @@ -/* mini-gmp, a minimalistic implementation of a GNU GMP subset. - - Contributed to the GNU project by Niels Möller - -Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. - -This file is part of the GNU MP Library. - -The GNU MP Library is free software; you can redistribute it and/or modify -it under the terms of either: - - * the GNU Lesser General Public License as published by the Free - Software Foundation; either version 3 of the License, or (at your - option) any later version. - -or - - * 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. - -or both in parallel, as here. - -The GNU MP Library 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 General Public License -for more details. - -You should have received copies of the GNU General Public License and the -GNU Lesser General Public License along with the GNU MP Library. If not, -see https://www.gnu.org/licenses/. */ +/********************************************************************************/ +/* */ +/* mini-gmp, a minimalistic implementation of a GNU GMP subset. */ +/* */ +/* Contributed to the GNU project by Niels Möller */ +/* */ +/* Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. */ +/* */ +/* This file is part of the GNU MP Library. */ +/* */ +/* The GNU MP Library is free software; you can redistribute it and/or modify */ +/* it under the terms of either: */ +/* */ +/* * the GNU Lesser General Public License as published by the Free */ +/* Software Foundation; either version 3 of the License, or (at your */ +/* option) any later version. */ +/* */ +/* or */ +/* */ +/* * 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. */ +/* */ +/* or both in parallel, as here. */ +/* */ +/* The GNU MP Library 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 General Public License */ +/* for more details. */ +/* */ +/* You should have received copies of the GNU General Public License and the */ +/* GNU Lesser General Public License along with the GNU MP Library. If not, */ +/* see https://www.gnu.org/licenses/. */ +/* */ +/* File modified by CEA (Commissariat à l'énergie atomique et aux */ +/* énergies alternatives). */ +/* */ +/********************************************************************************/ /* NOTE: All functions in this file which are not declared in mini-gmp.h are internal, and are not intended to be compatible diff --git a/src/plugins/e-acsl/contrib/libgmp/mini-gmp.h b/src/plugins/e-acsl/contrib/libgmp/mini-gmp.h index 4a192c2064f534aebb9df1b4ca1282a52f35ab77..1d9a2a2017ec815f8831bd716a3d76262eff08a5 100644 --- a/src/plugins/e-acsl/contrib/libgmp/mini-gmp.h +++ b/src/plugins/e-acsl/contrib/libgmp/mini-gmp.h @@ -1,32 +1,41 @@ -/* mini-gmp, a minimalistic implementation of a GNU GMP subset. - -Copyright 2011-2015 Free Software Foundation, Inc. - -This file is part of the GNU MP Library. - -The GNU MP Library is free software; you can redistribute it and/or modify -it under the terms of either: - - * the GNU Lesser General Public License as published by the Free - Software Foundation; either version 3 of the License, or (at your - option) any later version. - -or - - * 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. - -or both in parallel, as here. - -The GNU MP Library 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 General Public License -for more details. - -You should have received copies of the GNU General Public License and the -GNU Lesser General Public License along with the GNU MP Library. If not, -see https://www.gnu.org/licenses/. */ +/********************************************************************************/ +/* */ +/* mini-gmp, a minimalistic implementation of a GNU GMP subset. */ +/* */ +/* Contributed to the GNU project by Niels Möller */ +/* */ +/* Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. */ +/* */ +/* This file is part of the GNU MP Library. */ +/* */ +/* The GNU MP Library is free software; you can redistribute it and/or modify */ +/* it under the terms of either: */ +/* */ +/* * the GNU Lesser General Public License as published by the Free */ +/* Software Foundation; either version 3 of the License, or (at your */ +/* option) any later version. */ +/* */ +/* or */ +/* */ +/* * 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. */ +/* */ +/* or both in parallel, as here. */ +/* */ +/* The GNU MP Library 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 General Public License */ +/* for more details. */ +/* */ +/* You should have received copies of the GNU General Public License and the */ +/* GNU Lesser General Public License along with the GNU MP Library. If not, */ +/* see https://www.gnu.org/licenses/. */ +/* */ +/* File modified by CEA (Commissariat à l'énergie atomique et aux */ +/* énergies alternatives). */ +/* */ +/********************************************************************************/ /* About mini-gmp: This is a minimal implementation of a subset of the GMP interface. It is intended for inclusion into applications which diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml index dfccb58523ad7b215193797067e5ed022202693c..45e382a42f8f72c07573373ee6b6d206ed302506 100644 --- a/src/plugins/e-acsl/dup_functions.ml +++ b/src/plugins/e-acsl/dup_functions.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/dup_functions.mli b/src/plugins/e-acsl/dup_functions.mli index cf5a37ce57fb0733626103e375a45677c98fcc83..fa893ceabbea6f91bbe773fde4c3c321ebfd0524 100644 --- a/src/plugins/e-acsl/dup_functions.mli +++ b/src/plugins/e-acsl/dup_functions.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml index b72499902a3414a1bd8ce1c25ec45593b9c71fa8..9c604d2135eca498d0f694ae0eb3980cd5fcc0cc 100644 --- a/src/plugins/e-acsl/env.ml +++ b/src/plugins/e-acsl/env.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli index 429e4937ed1ce7cc10ea772541f2fc2b31b706c7..7fe184e3d026caead108691fab9f09660331006b 100644 --- a/src/plugins/e-acsl/env.mli +++ b/src/plugins/e-acsl/env.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/error.ml b/src/plugins/e-acsl/error.ml index 06157fdaac5ebdb8aa3f8d3d8ceaba30a772768f..6276d7da7f75ca0279007013a092c329ae360ef0 100644 --- a/src/plugins/e-acsl/error.ml +++ b/src/plugins/e-acsl/error.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/error.mli b/src/plugins/e-acsl/error.mli index 1406fc1b8463781fa1d5952095c5b6b3f652f7c6..3e59a8fa0cf462f3d1226abb4eee9195a9aa4981 100644 --- a/src/plugins/e-acsl/error.mli +++ b/src/plugins/e-acsl/error.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/exit_points.ml b/src/plugins/e-acsl/exit_points.ml index 9b05b9d91f03a77df342092c57d6db486bc49bed..fb8a42b86785130afbea388174cef06b8f1c3a37 100644 --- a/src/plugins/e-acsl/exit_points.ml +++ b/src/plugins/e-acsl/exit_points.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/exit_points.mli b/src/plugins/e-acsl/exit_points.mli index 9a32fe9e352920995354a8bd7bae8b6b7937e396..b130c98c686235f0223618a0bdc7e7f63ecc163d 100644 --- a/src/plugins/e-acsl/exit_points.mli +++ b/src/plugins/e-acsl/exit_points.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/functions.ml b/src/plugins/e-acsl/functions.ml index 45d20854ac4cae659dc8be8ee5f7dcd9f454806b..22c8f1cd994c47f7df914141c2fb5fe8096186f6 100644 --- a/src/plugins/e-acsl/functions.ml +++ b/src/plugins/e-acsl/functions.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli index 21b3849a83bbd2e08d350c3c6bc894590ff90421..7c65ec95fd4bd979c382d7ab939848d5919ed952 100644 --- a/src/plugins/e-acsl/functions.mli +++ b/src/plugins/e-acsl/functions.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/gmpz.ml b/src/plugins/e-acsl/gmpz.ml index 7f8e1b6e06ad31765eecb623298e5c482b38676a..ea9e81f9486f8b67d9f192df29f8b2ff47bbeade 100644 --- a/src/plugins/e-acsl/gmpz.ml +++ b/src/plugins/e-acsl/gmpz.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/gmpz.mli b/src/plugins/e-acsl/gmpz.mli index 453ca4b33922a91675069eddedecc33386446a4f..503d9887391538af619d68add5c8f95da59f680f 100644 --- a/src/plugins/e-acsl/gmpz.mli +++ b/src/plugins/e-acsl/gmpz.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/headers/close-source/CEA_LGPL_OR_PROPRIETARY.E_ACSL b/src/plugins/e-acsl/headers/close-source/CEA_LGPL_OR_PROPRIETARY.E_ACSL new file mode 100644 index 0000000000000000000000000000000000000000..7387695e04be306cbd81a9eeb6ccf17efe3b3696 --- /dev/null +++ b/src/plugins/e-acsl/headers/close-source/CEA_LGPL_OR_PROPRIETARY.E_ACSL @@ -0,0 +1,10 @@ + +This file is part of the Frama-C's E-ACSL plug-in. + +Copyright (C) 2012-2018 + CEA (Commissariat à l'énergie atomique et aux énergies + alternatives) + +All rights reserved. +Contact CEA LIST for licensing. + diff --git a/src/plugins/e-acsl/headers/close-source/MODIFIED_DLMALLOC b/src/plugins/e-acsl/headers/close-source/MODIFIED_DLMALLOC new file mode 100644 index 0000000000000000000000000000000000000000..216b3e540f1f03b186ef2909330729fc54645ba3 --- /dev/null +++ b/src/plugins/e-acsl/headers/close-source/MODIFIED_DLMALLOC @@ -0,0 +1,14 @@ + +This is a version (aka dlmalloc) of malloc/free/realloc written by +Doug Lea and released to the public domain, as explained at +http://creativecommons.org/publicdomain/zero/1.0/ Send questions, +comments, complaints, performance data, etc to dl@cs.oswego.edu + +Version 2.8.6 Wed Aug 29 06:57:58 2012 Doug Lea +Note: There may be an updated version of this malloc obtainable at + ftp://gee.cs.oswego.edu/pub/misc/malloc.c + Check before installing! + +File modified by CEA (Commissariat à l'énergie atomique et aux + énergies alternatives). + diff --git a/src/plugins/e-acsl/headers/close-source/MODIFIED_LIB_GMP b/src/plugins/e-acsl/headers/close-source/MODIFIED_LIB_GMP new file mode 100644 index 0000000000000000000000000000000000000000..6ca6c4f658f0705c1a491e350a80421c323c226d --- /dev/null +++ b/src/plugins/e-acsl/headers/close-source/MODIFIED_LIB_GMP @@ -0,0 +1,36 @@ + + mini-gmp, a minimalistic implementation of a GNU GMP subset. + + Contributed to the GNU project by Niels Möller + +Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. + +This file is part of the GNU MP Library. + +The GNU MP Library is free software; you can redistribute it and/or modify +it under the terms of either: + + * the GNU Lesser General Public License as published by the Free + Software Foundation; either version 3 of the License, or (at your + option) any later version. + +or + + * 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. + +or both in parallel, as here. + +The GNU MP Library 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 General Public License +for more details. + +You should have received copies of the GNU General Public License and the +GNU Lesser General Public License along with the GNU MP Library. If not, +see https://www.gnu.org/licenses/. + +File modified by CEA (Commissariat à l'énergie atomique et aux + énergies alternatives). + diff --git a/src/plugins/e-acsl/headers/close-source/MODIFIED_SPARETIMELABS b/src/plugins/e-acsl/headers/close-source/MODIFIED_SPARETIMELABS new file mode 100644 index 0000000000000000000000000000000000000000..98f92575c04e48b1f47c95d55caa89e6b30d1ee1 --- /dev/null +++ b/src/plugins/e-acsl/headers/close-source/MODIFIED_SPARETIMELABS @@ -0,0 +1,35 @@ + +Copyright (c) 2004,2012 Kustaa Nyholm / SpareTimeLabs + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the Kustaa Nyholm or SpareTimeLabs nor the names +of its contributors may be used to endorse or promote products derived +from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +File modified by CEA (Commissariat à l'énergie atomique et aux + énergies alternatives). + diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt new file mode 100644 index 0000000000000000000000000000000000000000..93668ad32c431bbf0771245d907c532e2c9b9adc --- /dev/null +++ b/src/plugins/e-acsl/headers/header_spec.txt @@ -0,0 +1,99 @@ +E_ACSL.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +INSTALL: .ignore +Makefile.in: CEA_LGPL_OR_PROPRIETARY.E_ACSL +README: .ignore +VERSION: .ignore +builtins.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +builtins.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +configure.ac: CEA_LGPL_OR_PROPRIETARY.E_ACSL +contrib/libdlmalloc/dlmalloc.c: MODIFIED_DLMALLOC +contrib/libgmp/mini-gmp.c: MODIFIED_LIB_GMP +contrib/libgmp/mini-gmp.h: MODIFIED_LIB_GMP +doc/Changelog: .ignore +doc/doxygen/doxygen.cfg.in: .ignore +dup_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +dup_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +env.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +env.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +error.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +error.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +gmpr.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +gmpr.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +gmpz.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +gmpz.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +lfunctions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +lfunctions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +license/CEA_LGPL: .ignore +license/LGPLv2.1: .ignore +license/SPARETIMELABS: .ignore +license/headache_config.txt: .ignore +literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +local_config.ml: .ignore +local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +main.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +man/e-acsl-gcc.sh.1: CEA_LGPL_OR_PROPRIETARY.E_ACSL +misc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +misc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +mmodel_analysis.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +mmodel_analysis.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +options.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +options.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +quantif.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +quantif.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +rte.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +rte.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +scripts/e-acsl-gcc.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL +scripts/testrun.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/bittree_model/e_acsl_bittree.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/bittree_model/e_acsl_bittree_api.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_alias.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_assert.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_bits.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_floating_point.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_format.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_gmp_api.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_leak.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_libc_replacements.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_malloc.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_printf.h: MODIFIED_SPARETIMELABS +share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_safe_locations.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_shexec.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_string.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_stubs_for_real.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_temporal.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/e_acsl_trace.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/segment_model/e_acsl_segment_mmodel.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/segment_model/e_acsl_segment_tracking.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +share/e-acsl/segment_model/e_acsl_shadow_layout.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL +temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +tests/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +tests/test_config.in: .ignore +translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +translate_lfunctions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +translate_lfunctions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +visit.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +visit.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL diff --git a/src/plugins/e-acsl/headers/open-source/CEA_LGPL_OR_PROPRIETARY.E_ACSL b/src/plugins/e-acsl/headers/open-source/CEA_LGPL_OR_PROPRIETARY.E_ACSL new file mode 100644 index 0000000000000000000000000000000000000000..c081974e6b385f65f99272b11af814bbd41b628d --- /dev/null +++ b/src/plugins/e-acsl/headers/open-source/CEA_LGPL_OR_PROPRIETARY.E_ACSL @@ -0,0 +1,19 @@ + +This file is part of the Frama-C's E-ACSL plug-in. + +Copyright (C) 2012-2018 + CEA (Commissariat à l'énergie atomique et aux énergies + alternatives) + +you can redistribute it and/or modify it under the terms of the GNU +Lesser General Public License as published by the Free Software +Foundation, version 2.1. + +It is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU Lesser General Public License for more details. + +See the GNU Lesser General Public License version 2.1 +for more details (enclosed in the file licenses/LGPLv2.1). + diff --git a/src/plugins/e-acsl/headers/open-source/MODIFIED_DLMALLOC b/src/plugins/e-acsl/headers/open-source/MODIFIED_DLMALLOC new file mode 100644 index 0000000000000000000000000000000000000000..216b3e540f1f03b186ef2909330729fc54645ba3 --- /dev/null +++ b/src/plugins/e-acsl/headers/open-source/MODIFIED_DLMALLOC @@ -0,0 +1,14 @@ + +This is a version (aka dlmalloc) of malloc/free/realloc written by +Doug Lea and released to the public domain, as explained at +http://creativecommons.org/publicdomain/zero/1.0/ Send questions, +comments, complaints, performance data, etc to dl@cs.oswego.edu + +Version 2.8.6 Wed Aug 29 06:57:58 2012 Doug Lea +Note: There may be an updated version of this malloc obtainable at + ftp://gee.cs.oswego.edu/pub/misc/malloc.c + Check before installing! + +File modified by CEA (Commissariat à l'énergie atomique et aux + énergies alternatives). + diff --git a/src/plugins/e-acsl/headers/open-source/MODIFIED_LIB_GMP b/src/plugins/e-acsl/headers/open-source/MODIFIED_LIB_GMP new file mode 100644 index 0000000000000000000000000000000000000000..6ca6c4f658f0705c1a491e350a80421c323c226d --- /dev/null +++ b/src/plugins/e-acsl/headers/open-source/MODIFIED_LIB_GMP @@ -0,0 +1,36 @@ + + mini-gmp, a minimalistic implementation of a GNU GMP subset. + + Contributed to the GNU project by Niels Möller + +Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. + +This file is part of the GNU MP Library. + +The GNU MP Library is free software; you can redistribute it and/or modify +it under the terms of either: + + * the GNU Lesser General Public License as published by the Free + Software Foundation; either version 3 of the License, or (at your + option) any later version. + +or + + * 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. + +or both in parallel, as here. + +The GNU MP Library 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 General Public License +for more details. + +You should have received copies of the GNU General Public License and the +GNU Lesser General Public License along with the GNU MP Library. If not, +see https://www.gnu.org/licenses/. + +File modified by CEA (Commissariat à l'énergie atomique et aux + énergies alternatives). + diff --git a/src/plugins/e-acsl/headers/open-source/MODIFIED_SPARETIMELABS b/src/plugins/e-acsl/headers/open-source/MODIFIED_SPARETIMELABS new file mode 100644 index 0000000000000000000000000000000000000000..98f92575c04e48b1f47c95d55caa89e6b30d1ee1 --- /dev/null +++ b/src/plugins/e-acsl/headers/open-source/MODIFIED_SPARETIMELABS @@ -0,0 +1,35 @@ + +Copyright (c) 2004,2012 Kustaa Nyholm / SpareTimeLabs + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the Kustaa Nyholm or SpareTimeLabs nor the names +of its contributors may be used to endorse or promote products derived +from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +File modified by CEA (Commissariat à l'énergie atomique et aux + énergies alternatives). + diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml index 0971117c11a657386e47b4b8ae80b1a1f4190a14..0f68e4bc8d08c10f1733746e5490093f7ead11c9 100644 --- a/src/plugins/e-acsl/interval.ml +++ b/src/plugins/e-acsl/interval.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli index aa62d2d8f71345473f12694cff146075ae29c024..3d5fd8b3be2ecf03cadcd64b8290c38fddd3fa30 100644 --- a/src/plugins/e-acsl/interval.mli +++ b/src/plugins/e-acsl/interval.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/keep_status.ml b/src/plugins/e-acsl/keep_status.ml index 8eba16000772372c0476d09c2cc4f08fc02a697d..69da42233489b929b8025a7f71693ced59b58002 100644 --- a/src/plugins/e-acsl/keep_status.ml +++ b/src/plugins/e-acsl/keep_status.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/keep_status.mli b/src/plugins/e-acsl/keep_status.mli index a952d47eaeeae6aa8938ba780d11d77c6b134cf8..fb780c54aa0870d6c3f11c1286090f8a5d8f3c7d 100644 --- a/src/plugins/e-acsl/keep_status.mli +++ b/src/plugins/e-acsl/keep_status.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml index 89949e3c7276fac39a3bb4f6b455711f7cadb443..d8c90534dff4829adb75f1c158ed3b170279a6bd 100644 --- a/src/plugins/e-acsl/label.ml +++ b/src/plugins/e-acsl/label.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/label.mli b/src/plugins/e-acsl/label.mli index 7d636c85b18513ad77fae941c971bcf54ba6743e..3db8fa96dd9b275410fb0cfa3468ecd1b4694a11 100644 --- a/src/plugins/e-acsl/label.mli +++ b/src/plugins/e-acsl/label.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/license/headache_config.txt b/src/plugins/e-acsl/license/headache_config.txt index 3c7dcc850357bcbfb33638b3a07e80fdc6489b94..9bb003875b043426b796ecc87f2378b392f3f60d 100644 --- a/src/plugins/e-acsl/license/headache_config.txt +++ b/src/plugins/e-acsl/license/headache_config.txt @@ -8,10 +8,10 @@ # C source # ############ | ".*\.h" -> frame open:"/*" line:"*" close:"*/" +| ".*\.i" -> frame open:"/*" line:"*" close:"*/" | ".*\.c" -> frame open:"/*" line:"*" close:"*/" | ".*\.ast" -> frame open:"//" line:" " close:" " | ".*\.cc" -> frame open:"/*" line:"*" close:"*/" -| "perfcount.c.in" -> frame open: "/*" line: "*" close: "*/" ####### # Asm # @@ -27,23 +27,49 @@ ############ # 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.*" | ".*\.sh" -> frame open:"#" line:"#" close:"#" | ".*\.sh" -> skip match:"#!.*" +| "frama-c" -> frame open:"#" line:"#" close:"#" +| ".*frama-c" -> skip match:"#!.*" +| "frama-c-config" -> frame open:"#" line:"#" close:"#" +| ".*frama-c-config" -> skip match:"#!.*" +| "frama-c-script" -> frame open:"#" line:"#" close:"#" +| ".*frama-c-script" -> skip match:"#!.*" +| "frama-c-gui" -> frame open:"#" line:"#" close:"#" +| ".*frama-c-gui" -> skip match:"#!.*" +| "frama-c-gui.byte" -> frame open:"#" line:"#" close:"#" +| ".*frama-c-gui.byte" -> skip match:"#!.*" +| "frama-c.byte" -> frame open:"#" line:"#" close:"#" +| ".*frama-c.byte" -> skip match:"#!.*" +| "frama-c.top" -> frame open:"#" line:"#" close:"#" +| ".*frama-c.top" -> skip match:"#!.*" + +################ +# Perl scripts # +################ +| ".*\.perl" -> frame open:"#" line:"#" close:"#" +| "flamegraph.pl" -> frame open:"#" line:"#" close:"#" +| ".*flamegraph.pl" -> skip match:"#!.*" ######################### -# MS-Windows Ressources # +# MS-Windows Resources # ######################### | ".*\.rc" -> frame open:"#" line:"#" close:"#" ############# # man pages # ############# -| ".*\.[1-9]" -> frame open:".\\\"" line: " " close:"" +| ".*\.[1-9]" -> frame open:".\\\"" line: "-" close:"" ############# # Why files # @@ -51,22 +77,52 @@ | ".*\.why" -> frame open: "(*" line: "*" close: "*)" | ".*\.why\.src" -> frame open: "(*" line: "*" close: "*)" +############# +# Alt-Ergo files # +############# +| ".*\.mlw" -> frame open: "(*" line: "*" close: "*)" + ############# # Coq files # ############# | ".*\.v" -> frame open: "(*" line: "*" close: "*)" +############# +# WP files # +############# +| ".*\.driver" -> frame open: "/*" line: "*" close: "*/" + +##################### +# Why3 driver files # +##################### +| ".*\.drv" -> frame open: "(*" line: "*" close: "*)" + ######## # HTML # ######## -| ".*\.htm.*" -> frame open: "<!--" line: " " close: "-->" +| ".*\.htm.*" -> frame open: "<!--" line: "-" close: "-->" + +####### +# DTD # +####### +| ".*\.dtd" -> frame open: "<!--" line: " " close: "-->" + +####### +# XSL # +####### +| ".*\.xsl" -> frame open: "<!--" line: " " close: "-->" ####### # CSS # ####### | ".*\.css" -> frame open: "/*" line: "*" close: "*/" # plug-in's ocamldoc introductions -| "intro_.*\.txt" -> frame open: "@ignore" line: " " close: "" +| "intro_.*\.txt" -> frame open: "#*" line: "*" close: "#" + +########## +# PROLOG # +########## +| ".*\.pl" -> frame open: "%" line: "%" close: "%" ############## # Emacs Lisp # diff --git a/src/plugins/e-acsl/literal_strings.ml b/src/plugins/e-acsl/literal_strings.ml index b90fb4167ee433d612f4cacda9f6232eb30d59a1..77b1cdcfcc41022856ddb9ae933f24e52f3065d4 100644 --- a/src/plugins/e-acsl/literal_strings.ml +++ b/src/plugins/e-acsl/literal_strings.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/literal_strings.mli b/src/plugins/e-acsl/literal_strings.mli index 5551aac2a248cea81b14429238971b696125440d..d73cc6e2f14f69faf5b96122d86cc05dc2788ad5 100644 --- a/src/plugins/e-acsl/literal_strings.mli +++ b/src/plugins/e-acsl/literal_strings.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/local_config.mli b/src/plugins/e-acsl/local_config.mli index b6617a392cce276e90562340e4435245720a6c42..6374af51bc59a8f33297791f584842456eed57f1 100644 --- a/src/plugins/e-acsl/local_config.mli +++ b/src/plugins/e-acsl/local_config.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml index b359b7beb1d82d9b23977ef0977a608a08ab8379..2d0551e2996ae010c3e11d2f9be4326acf5088f3 100644 --- a/src/plugins/e-acsl/loops.ml +++ b/src/plugins/e-acsl/loops.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/loops.mli b/src/plugins/e-acsl/loops.mli index 1f2d658a8e25528cc3367cbb4906ba003e331271..3a5dfa381468c79c7c9e42ae34e250c50b1f93cb 100644 --- a/src/plugins/e-acsl/loops.mli +++ b/src/plugins/e-acsl/loops.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml index e1d7ac2aa2dcf8f8f236d26d2953d0307c320593..a78c2863e62dd5301a104926ac05be8593e04f48 100644 --- a/src/plugins/e-acsl/main.ml +++ b/src/plugins/e-acsl/main.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 index b79512e1353d31675a1a33e83aea7f924a36dd79..601728e0c01a4c18161f8e28d7583cc8b5f7e464 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -1,8 +1,8 @@ +.\"------------------------------------------------------------------------ .\" +.\" This file is part of the Frama-C's E-ACSL plug-in. .\" -.\" This file is part of Frama-C. -.\" -.\" Copyright (C) 2007-2018 +.\" Copyright (C) 2012-2018 .\" CEA (Commissariat à l'énergie atomique et aux énergies .\" alternatives) .\" @@ -18,7 +18,7 @@ .\" See the GNU Lesser General Public License version 2.1 .\" for more details (enclosed in the file licenses/LGPLv2.1). .\" -.\" +.\"------------------------------------------------------------------------ .TH E-ACSL-GCC.SH 1 2016-02-02 diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml index e4971d0f5b55a7cab2a72775d894c97c49a62946..55ef595b98fab51cb9aeba6dc56b0d38bdd36171 100644 --- a/src/plugins/e-acsl/misc.ml +++ b/src/plugins/e-acsl/misc.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli index 6c61e732290df1b6af59e95e6286c2a3ad648e23..c78ce82424117f87449cc622e59f022bd66557ec 100644 --- a/src/plugins/e-acsl/misc.mli +++ b/src/plugins/e-acsl/misc.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml index cdecfdfdef955b1cb1605332e352eac41bdf1525..1c3f78ee9e689d3689e5d01f7b467058dba62a3c 100644 --- a/src/plugins/e-acsl/mmodel_analysis.ml +++ b/src/plugins/e-acsl/mmodel_analysis.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/mmodel_analysis.mli b/src/plugins/e-acsl/mmodel_analysis.mli index 5db4477e49252448d1b2aa75a589f54096061f52..ebf5c7f09f8e9eafd3e9ec203fa5caca2ecca65b 100644 --- a/src/plugins/e-acsl/mmodel_analysis.mli +++ b/src/plugins/e-acsl/mmodel_analysis.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml index 7652bd6715c7b1fe2107a10077b8921b6bd524b5..93797ae0bde404f5271926e849a3cd48c2c786ca 100644 --- a/src/plugins/e-acsl/options.ml +++ b/src/plugins/e-acsl/options.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli index d4b10ab5aa454bb0a61a75c8cfc47af2c8a1735a..6e1347e43d75d5a85c7b1a45d6b8f486d95a6cbb 100644 --- a/src/plugins/e-acsl/options.mli +++ b/src/plugins/e-acsl/options.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/prepare_ast.ml b/src/plugins/e-acsl/prepare_ast.ml index 909d6666996977466a39d7e32b204fd78effe81b..4113123a9da2afb6f98f1997a2b84d7b6f4f8532 100644 --- a/src/plugins/e-acsl/prepare_ast.ml +++ b/src/plugins/e-acsl/prepare_ast.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/prepare_ast.mli b/src/plugins/e-acsl/prepare_ast.mli index c35114f2e2710f5248acc418d37291d3fbf6f5f0..c2db62e1ea87f389e9522aba28f00fa8356d49cf 100644 --- a/src/plugins/e-acsl/prepare_ast.mli +++ b/src/plugins/e-acsl/prepare_ast.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml index fa8fc69a5ef68fe8f93d9ae7f14cafd5a645804f..30a72c560b535dc9ac25dc99a64a3b4d6a5d5cc4 100644 --- a/src/plugins/e-acsl/quantif.ml +++ b/src/plugins/e-acsl/quantif.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/quantif.mli b/src/plugins/e-acsl/quantif.mli index d8e8b9819c91d418be5d6f9b207e7f7dd8f2f58e..099a6a4c7431d7a16c2587f5d2093264aac114a1 100644 --- a/src/plugins/e-acsl/quantif.mli +++ b/src/plugins/e-acsl/quantif.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/rte.ml b/src/plugins/e-acsl/rte.ml index 8a3a4e3c31b433d40d7c2605b4adec102fa80b8e..5f12d7aa07774f5524449815a5a4da19cd046b21 100644 --- a/src/plugins/e-acsl/rte.ml +++ b/src/plugins/e-acsl/rte.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/rte.mli b/src/plugins/e-acsl/rte.mli index 8b3ce9563b006cc096a4e06ff1a1570385289f0f..4af8130be29737ecc29f0b5ccf5338566a28662c 100644 --- a/src/plugins/e-acsl/rte.mli +++ b/src/plugins/e-acsl/rte.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 332d6914bf3e3aaa8cfebcb1b5c8ca1551315c09..71cbb9b1ee61824dc2b57ce67809313f5249fb0d 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -1,9 +1,9 @@ #!/bin/sh -e ########################################################################## # # -# This file is part of Frama-C. # +# This file is part of the Frama-C's E-ACSL plug-in. # # # -# Copyright (C) 2007-2018 # +# Copyright (C) 2012-2018 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh index e37333cf358c1c551109b56b96b32e5baa1fda5e..865545f6a0fb430b904307e4228497256ed62ed4 100755 --- a/src/plugins/e-acsl/scripts/testrun.sh +++ b/src/plugins/e-acsl/scripts/testrun.sh @@ -1,9 +1,9 @@ #!/bin/sh -e ########################################################################## # # -# This file is part of Frama-C. # +# This file is part of the Frama-C's E-ACSL plug-in. # # # -# Copyright (C) 2007-2018 # +# Copyright (C) 2012-2018 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h index 773d9a51c3ea7c6cf0f18dd4049c1284987069bc..d581f762e9d7614755c9a05369eb2bfa614a5f19 100644 --- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h +++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h index 78d0154a4824627b4fcb9157f7f06a30f7014562..ae566998e006910950415c72be7e6506449b4f72 100644 --- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h +++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c index b8eb72ebb954dda2a8486441f98c5e86ea1da4aa..eafd0b80772ba11cbc38559fbe2a34258ae325c0 100644 --- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c +++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.h b/src/plugins/e-acsl/share/e-acsl/e_acsl.h index dc4ca8a67b702e98f7bc2555b3ab4f054d2f80ff..1045095a0b66c632681a5b6493fe74dbadb0ceb4 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h index e42f6f1f47b6b7698ba277d99dc754063b1c8d03..17518ac0333574bd6a084f5eede66c14899a642c 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h index d8a9bd51d861a5d115c7d115b732d99a32a1e816..81496109beefc1199eddfcb5c800a1708c295d05 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h index fc6c2a8fafffc31ad349085cbb72dd797dd7e2ff..f13e46264b7b6d3641142422e3d88870ac973f9d 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h index 1df4b3f8ae9eaaa5dc646ed794ef14471e0ba280..2073a9aa1f32003748176887f29d355c24f23828 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h index 5d6f87bbdd3a713b2c7b10764aeeb3d7ef206a12..8c6a654616130dd1d821301afb567da0a63b4a7c 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_format.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_format.h index ba032670bbd2d7356f5662e9fc70b66003d29ba1..fa78e400828db3547a83888f89e58e5e8eee447c 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_format.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_format.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h index f7840e0effdb5206c7657784313bedae2bbb7cb6..89d73da70643aaa34f8e8ab6e4ab669c61da2ee9 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_leak.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_leak.h index 7ff5cae7692d05eacbf9d93c36e63831de7814f3..2b2f517986b940539192ee572dcefadefcb1c065 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_leak.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_leak.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_libc_replacements.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_libc_replacements.h index d12d18f39c85df8c0524d96f31429d972d6db0bb..0ef0a734af48c90cb852f3c2a565f2447064a32f 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_libc_replacements.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_libc_replacements.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h index af99763c4303e610f9fc20a6a39bc680886f984e..c216fba3fadd0487360883484698cd5d59a0a2b0 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h index e439fdd5420ae01445a1c40fe9c48d39b0f4a531..729e8a1d633f1523679017d1180ad82622e0965e 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h @@ -31,6 +31,9 @@ /* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE */ /* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ /* */ +/* File modified by CEA (Commissariat à l'énergie atomique et aux */ +/* énergies alternatives). */ +/* */ /****************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c index c023812a87b7c830472d27c9d101f4d2b9d21ae8..2d5d3668076182414bcd4f60d586221bccbd6bfb 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h index 340222cd3ac6dfb74384438d69d23910ca4a5b87..d98a944cc10831639161c033795ba7d590c7c4ac 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_shexec.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_shexec.h index 86515d9bc3a14cd8a0098f98dbccd743ed436aa5..fea42b6d1e5d5764c24a3bbdda82d3ac3e698052 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_shexec.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_shexec.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h index 801a4712a29deac6f4bcdc06a89e253e349f9396..c0e694b58157f227929ff61420d7e3da2d004096 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h index 48a17f54c631722a536136a875c1959c0c802068..6caa803e1b127d577f3689fa8ae51426a4dd629d 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h @@ -16,7 +16,7 @@ /* GNU Lesser General Public License for more details. */ /* */ /* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file license/LGPLv2.1). */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ /* */ /**************************************************************************/ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h index a99a4900e207c02004f8b78af1587e0f8e4aa6df..107f12ea88cbfddb823d56c49c9b304e7ab924a3 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h @@ -16,7 +16,7 @@ /* GNU Lesser General Public License for more details. */ /* */ /* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file license/LGPLv2.1). */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ /* */ /**************************************************************************/ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_trace.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_trace.h index 6025027bd4d51d6d5c6f78461aca723680af0661..4ba3454d2663531e1c1a76947ef13722308d9f48 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_trace.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_trace.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c index 279c8c66137938dc81b44cabc1a4ff82d9ca6b79..580274d9b85e203cb38f453c9e5070b3e65ce820 100644 --- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c +++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h index c8248552b4aec1d6760c973c10ff83270a9c9c56..100e167734f7aa1fc08a372c2eadfa09f53deabb 100644 --- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h +++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h index 3ee6db579bfd8cf8c34b2ad7cfe77f7aa426c110..0822602dd21d5f9d00fc85b207601619f8be2276 100644 --- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h +++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h @@ -1,8 +1,8 @@ /**************************************************************************/ /* */ -/* This file is part of Frama-C. */ +/* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2007-2018 */ +/* Copyright (C) 2012-2018 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml index eab40b42849ad27b450b1f843e96fcc9cae72cd9..4d75476b7e8742628e9dac83f2b9050c3670ce77 100644 --- a/src/plugins/e-acsl/temporal.ml +++ b/src/plugins/e-acsl/temporal.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/temporal.mli b/src/plugins/e-acsl/temporal.mli index fb4d81db317342e1680c1d18331f91c8e969945d..bd2e1606a1eb3c8e4be6a1a911657f735140dfb4 100644 --- a/src/plugins/e-acsl/temporal.mli +++ b/src/plugins/e-acsl/temporal.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/tests/print.ml b/src/plugins/e-acsl/tests/print.ml index 669460520589f349a6936776696445f80305a23f..4cd4e8bfd8407702c8e826719b7553644b671ec2 100644 --- a/src/plugins/e-acsl/tests/print.ml +++ b/src/plugins/e-acsl/tests/print.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml index e57580f53f2b1e0e7d48607b4cc9d63856081456..037ac3a4dbfc5d726e86a1ae6933835663e69c90 100644 --- a/src/plugins/e-acsl/translate.ml +++ b/src/plugins/e-acsl/translate.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli index 4f8540341fa2d6340d09325272825dbe46866080..7e58df3a032e13208d514afd53d1f698124138c6 100644 --- a/src/plugins/e-acsl/translate.mli +++ b/src/plugins/e-acsl/translate.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml index 8a8dee64fba5c203d3ed2193d07cdf0d20d3273f..fa789522b48a1c4128f88db21b8e54e54eba712b 100644 --- a/src/plugins/e-acsl/typing.ml +++ b/src/plugins/e-acsl/typing.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli index e8a74d55ae836bdb349a116b739b0607c80e43b2..4195ec14f10a235721c0f99a692de9b75a1314d3 100644 --- a/src/plugins/e-acsl/typing.mli +++ b/src/plugins/e-acsl/typing.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index 91933f67a107917c3db8381f5b77ad4c65eedad2..fa1a961c16f0594b790b9d18dcf277dd91276995 100644 --- a/src/plugins/e-acsl/visit.ml +++ b/src/plugins/e-acsl/visit.ml @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/src/plugins/e-acsl/visit.mli b/src/plugins/e-acsl/visit.mli index 8e536081b3009c7a793555b9b3069b264964dbab..ff9d8edb1239b408b4b8db9340deedc7743e4ad0 100644 --- a/src/plugins/e-acsl/visit.mli +++ b/src/plugins/e-acsl/visit.mli @@ -1,8 +1,8 @@ (**************************************************************************) (* *) -(* This file is part of Frama-C. *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) (* *) -(* Copyright (C) 2007-2018 *) +(* Copyright (C) 2012-2018 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *)