From 989a6e4f361af91f0b6c7cc259ae8ea54c835c91 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Tue, 28 Nov 2017 10:43:04 +0100 Subject: [PATCH] update copyright and convert ISO-8859 to UTF-8 --- src/plugins/e-acsl/TODO | 4 ++-- src/plugins/e-acsl/doc/userman/main.tex | 2 +- src/plugins/e-acsl/interval.mli | 2 +- src/plugins/e-acsl/license/CEA_LGPL | 4 ++-- src/plugins/e-acsl/scripts/e-acsl-gcc.comp | 2 +- src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h | 2 +- src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h | 2 +- src/plugins/e-acsl/typing.ml | 2 +- src/plugins/e-acsl/typing.mli | 2 +- 9 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO index 961365f414f..9cee0e19010 100644 --- a/src/plugins/e-acsl/TODO +++ b/src/plugins/e-acsl/TODO @@ -5,11 +5,11 @@ - [Bernard] implement a function e_acsl_trace_behavior(char *bhv_name) {} which would be called anytime a behavior is activated - [Yannick] Logic functions -- [Nikolaï] temporal memory properties +- [Nikolaï] temporal memory properties - memory profiling - [Guillaume] add the RTE annotations generated by E-ACSL in the Frama-C annotation table (possibly through a new command line option) -- [David Mentré] support of tset +- [David Mentré] support of tset - [Guillaume] when a verification fails at runtime, possibility of seeing the values of each involved left-values (cf Boogaloo@RV'13). - [Everyone] provide the compilation scripts of the generated program diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex index f87476d001d..86f502d3e10 100644 --- a/src/plugins/e-acsl/doc/userman/main.tex +++ b/src/plugins/e-acsl/doc/userman/main.tex @@ -26,7 +26,7 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\ \end{tabular} \vfill \begin{flushleft} - \textcopyright 2013-2016 CEA LIST + \textcopyright 2013-2017 CEA LIST %% %% This work has been supported by the `Hi-Lite' FUI project (FUI AAP 9). \end{flushleft} diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli index e7f5c845ff6..6fc70d29a62 100644 --- a/src/plugins/e-acsl/interval.mli +++ b/src/plugins/e-acsl/interval.mli @@ -29,7 +29,7 @@ (see module {!Interval.Env}). It implement Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour - devenir plus rapide, plus précis et plus mince". + devenir plus rapide, plus précis et plus mince". Example: consider a variable [x] of type [int] on a (strange) architecture in which values of type [int] belongs to the interval \[-128;127\] and a diff --git a/src/plugins/e-acsl/license/CEA_LGPL b/src/plugins/e-acsl/license/CEA_LGPL index 56540f32d9b..7834eed82ce 100644 --- a/src/plugins/e-acsl/license/CEA_LGPL +++ b/src/plugins/e-acsl/license/CEA_LGPL @@ -1,8 +1,8 @@ This file is part of the Frama-C's E-ACSL plug-in. -Copyright (C) 2012-2016 - CEA (Commissariat à l'énergie atomique et aux énergies +Copyright (C) 2012-2017 + CEA (Commissariat à l'énergie atomique et aux énergies alternatives) you can redistribute it and/or modify it under the terms of the GNU diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp index b8229dd1647..c34c7b6d75f 100644 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp @@ -2,7 +2,7 @@ # # # This file is part of the Frama-C's E-ACSL plug-in. # # # -# Copyright (C) 2012-2016 # +# Copyright (C) 2012-2017 # # 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 a53c01337d8..a7a5726555a 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 @@ -2,7 +2,7 @@ /* */ /* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2012-2015 */ +/* Copyright (C) 2012-2017 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ 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 55ceb6261f9..c137029c5a1 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 @@ -2,7 +2,7 @@ /* */ /* This file is part of the Frama-C's E-ACSL plug-in. */ /* */ -/* Copyright (C) 2012-2015 */ +/* Copyright (C) 2012-2017 */ /* 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 9f9130fbf8e..02ad1554c76 100644 --- a/src/plugins/e-acsl/typing.ml +++ b/src/plugins/e-acsl/typing.ml @@ -23,7 +23,7 @@ open Cil_types (* Implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour - devenir plus rapide, plus précis et plus mince". *) + devenir plus rapide, plus précis et plus mince". *) let dkey = Options.dkey_typing diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli index 9ed4896f605..75fd745243d 100644 --- a/src/plugins/e-acsl/typing.mli +++ b/src/plugins/e-acsl/typing.mli @@ -25,7 +25,7 @@ required casts. It is based on interval inference of module {!Interval}. It implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour - devenir plus rapide, plus précis et plus mince". + devenir plus rapide, plus précis et plus mince". Example: consider a variable [x] of type [int] and a variable [y] of type char on a (strange) architecture in which values of type [int] belongs to -- GitLab