diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO index 961365f414f0a902d9babcdd8d2beb80da635b90..9cee0e19010d7c0435f4feac617bf055443d2f96 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 f87476d001dcf09e39bbf001a411837bade7db51..86f502d3e1064a149aacfaf68033751c8c36e1c9 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 e7f5c845ff6fc2c2d31858e46bb4c3c1c0c19d2e..6fc70d29a623f1acc6be2e184735a2deebc36774 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 56540f32d9b47da4d48779f16f0a7d856e22ad88..7834eed82ce82df6b7327448eeffea83d336deb1 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 b8229dd16473b656dd05835396ae46ae19904bc9..c34c7b6d75f3f884ba5a101561713ca40e2ae5b4 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 a53c01337d8fcb758eea5ee4ea610d63d9770696..a7a5726555ab5c0f53ea223b0c82e1d59847e204 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 55ceb6261f913ce8a7f6c0311c9a6bdfa33ec9a5..c137029c5a1c92c494497304be758b36258027e0 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 9f9130fbf8e751cf949a4709f8e70fe23671a9e3..02ad1554c768a6ff90894395e167f81d2d41291b 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 9ed4896f605197f071fbb7c679f45a4bca4efe24..75fd745243d34b147597a016bcbce4bb44b28abd 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