Merge branch 'stable/sulfur' into 'master'

Stable/sulfur

See merge request frama-c/e-acsl!176

src/plugins/e-acsl/Makefile.in

@@ -264,7 +264,7 @@ EACSL_LICENSE_FILES = \
   license/headache_config.txt license/LGPLv2.1
 
 EACSL_MISC_FILES = \
-  configure.ac Makefile.in INSTALL README VERSION .depend
+  configure.ac Makefile.in INSTALL README VERSION
 
 EACSL_SHARE_FILES = share/e-acsl/*.[ch] share/e-acsl/*/*.[ch]
 
@@ -281,7 +281,7 @@ PLUGIN_DISTRIB_EXTERNAL:=\
 EACSL_DISTRIB_FILES:= $(PLUGIN_DISTRIB_EXTERNAL) $(EACSL_OCAML_FILES)
 
 # BE CAREFUL: manually remove all *.ml* files which should not be released!
-e-acsl-distrib: .depend
+e-acsl-distrib:
 	$(PRINT_TAR) tmp-distrib
 	$(TAR) cf tmp.tar $(EACSL_DISTRIB_FILES)
 	$(PRINT_MAKING) export directories

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

src/plugins/e-acsl/doc/Changelog

@@ -20,26 +20,31 @@
 ###############################################################################
 
 -* e-acsl-gcc   [2017/11/28] Several files may be given to e-acsl-gcc.sh
-	        (as specified).
+                (as specified).
 -* E-ACSL       [2017/11/27] Fix 'segmentation fault' of the generated monitor
-	        whenever the main as a precondition depending on the memory
-	        model.
+                whenever the main as a precondition depending on the memory
+                model.
 -* E-ACSL       [2017/11/27] Restore behavior of option -e-acsl-valid broken
-	        since Phosphorus (included).
+                since Phosphorus (included).
+
+#############################
+Plugin E-ACSL Sulfur-20171101
+#############################
+
 -* E-ACSL       [2017/10/25] Fix bug #2303 about unnamed formals in
-	        annotated functions.
+                annotated functions.
 -  e-acsl-gcc   [2017/06/10] Add --free-valid-address option to e-acsl.gcc.sh.
 -  e-acsl-gcc   [2017/05/29] Add --fail-with-code option to e-acsl.gcc.sh.
 -  e-acsl-gcc   [2017/05/19] Add --temporal option to e-acsl.gcc.sh.
 -  E-ACSL       [2017/05/19] New detection of temporal errors in E-ACSL
-	        through -e-acsl-temporal-validity (disabled by default).
+                through -e-acsl-temporal-validity (disabled by default).
 -  e-acsl-gcc   [2017/03/26] Add --weak-validity option to e-acsl.gcc.sh.
 -  e-acsl-gcc   [2017/03/26] Add --rt-verbose option to e-acsl.gcc.sh.
 -  e-acsl-gcc   [2017/03/26] Add --keep-going option to e-acsl.gcc.sh allowing
-	        a program to continue execution after an assertion failure.
+                a program to continue execution after an assertion failure.
 -  e-acsl-gcc   [2017/03/26] Add --stack-size and --heap-size options to
-	        e-acsl-gcc.sh allowing to change the default sizes of the
-	        respective shadow spaces.
+                e-acsl-gcc.sh allowing to change the default sizes of the
+                respective shadow spaces.
 
 #################################
 Plugin E-ACSL Phosphorus-20170515

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}

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

src/plugins/e-acsl/license/CEA_LGPL

 
 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

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)                                                  #
 #                                                                        #

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)                                                  */
 /*                                                                        */

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)                                                  */
 /*                                                                        */

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
 

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