diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index fd9f25d08edc7e2c5a8cb881034109122baf471f..3ccc328577bdc92ea5995d33e33a03852983c04f 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -1,3 +1,4 @@
+*~
/*.o
/*.cm*
/*.annot
diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index a64237c6c2e64eec05382f31b04c0850abbc25f6..964bf6c1dbde81cff453b52631d3661949b79ea3 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 e36364a11a131d2df3c14ebc5c25b633eb77da7d..b9125adf22e6fd3b1d23cadd8a3120129e4b7461 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -2,7 +2,7 @@
# #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
-# Copyright (C) 2012-2013 #
+# Copyright (C) 2012-2014 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 52c43259d20ce81419201c39d1f7e96177454053..bd73f47072b1fe4b9914ec14a7f6d47fcc8f816a 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-0.3+dev
+0.4
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index cb00b0fc14c92612e7d0b0922171bc80f30c017d..9c2233d8a3a6bdaa7203da637ecd1254b087c973 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -2,7 +2,7 @@
# #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
-# Copyright (C) 2012-2013 #
+# Copyright (C) 2012-2014 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
@@ -55,17 +55,19 @@ AC_MSG_CHECKING(for Frama-C version)
DEV_VERSION_NUMBER=`echo $FRAMAC_VERSION | sed -e 's/.*-\(.*\)/\1/' `
VERSION_NUMBER=`echo $DEV_VERSION_NUMBER | sed -e 's/\(.*\)+dev/\1/' `
+REQUIRED_NUMBER=20140301
-if test $VERSION_NUMBER -lt 20130601; then
- AC_MSG_ERROR(Frama-C version must be at least Fluorine-20130601.)
-fi
-
-# at the time being, must use the Frama-C development version
-DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
-if test "$DEV" != "+dev"; then
- AC_MSG_ERROR(Frama-C version must be the current SVN version.);
+if test $VERSION_NUMBER -lt $REQUIRED_NUMBER; then
+ AC_MSG_ERROR(Frama-C version must be at least Neon-$REQUIRED_NUMBER.)
else
- AC_MSG_RESULT($FRAMAC_VERSION)
+
+# # at the time being, must use the Frama-C development version
+# DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
+# if test "$DEV" != "+dev"; then
+# AC_MSG_ERROR(Frama-C version must be the current GIT version.);
+# else
+ AC_MSG_RESULT($FRAMAC_VERSION)
+# fi
fi
# OCaml version
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index ed86b92376eb55e87e4e4082c5e58157411437ef..1e53bae42cffb36f91373cc636718c00c7a4d166 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,10 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+###############################
+Plugin E-ACSL 0.4 Neon_20140301
+###############################
+
-* E-ACSL [2014/01/28] Fix bug #1634 occuring in presence of static
addresses.
-* E-ACSL [2013/09/26] Fix incorrectness which may occur in presence
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf
index fcb304e9554c2055aa14752cf856fd8c396df249..8ca398e1785d619f5d6dcaaf07e4b107d2ef01c8 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf
index f692a5c85fe1f7237ed9c82ca60536c44b1a8cba..f91653e290e6453089815156a3ec66c9e1b70970 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf differ
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf
index 0b539ef84e290b5ffab2d23ffaca1f7a7d1392ee..10f75d8cd715b7f3ad55cf6195dd13de3d8c2d13 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index a2c62a9667fc6ccbdd9fcbe7243ffa8c55a56964..b7b857f4e7925cce8eecab9571078c72bb404444 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -1 +1,2 @@
e-acsl.pdf
+e-acsl-implementation.pdf
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 2e6e31df15a05d0ff252af2ee900901c34e37234..fcb5d4578d8a5cf6f3645f2642b1ea52943e6f31 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -4,7 +4,7 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
libraries_modern.tex concl_modern.tex changes_modern.tex \
term_modern.bnf binders_modern.bnf predicate_modern.bnf \
fn_behavior_modern.bnf oldandresult_modern.bnf \
- loc_modern.bnf \
+ loc_modern.bnf memory_modern.bnf \
assertions_modern.bnf loops_modern.bnf st_contracts_modern.bnf \
logic_modern.bnf data_invariants_modern.bnf model_modern.bnf \
ghost_modern.bnf generalinvariants_modern.bnf iterator_modern.bnf \
@@ -18,17 +18,17 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
all: e-acsl
-LANGUAGE_VERSION=1.7-1
-EACSL_VERSION= 0.3
+LANGUAGE_VERSION=1.8
+EACSL_VERSION= 0.4
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install: e-acsl-implementation.pdf e-acsl.pdf
cp -f $^ $(EACSL_DIR)/doc/manuals
- cp -f e-acsl.pdf \
- $(DISTRIB_DIR)/download/e-acsl/e-acsl-$(LANGUAGE_VERSION).pdf
- cp -f e-acsl-implementation.pdf \
- $(DISTRIB_DIR)/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
+ # cp -f e-acsl.pdf \
+ # $(DISTRIB_DIR)/download/e-acsl/e-acsl-$(LANGUAGE_VERSION).pdf
+ # cp -f e-acsl-implementation.pdf \
+ # $(DISTRIB_DIR)/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
@@ -106,7 +106,9 @@ e-acsl.pdf: $(DEPS_MODERN)
e-acsl.tex: e-acsl-implementation.tex Makefile
rm -f $@
- sed -e '/PrintImplementationRq/s/%--//' $^ > $@
+ sed -e '/PrintImplementationRq/s/%--//' \
+ -e '/ColorImplementationRq/s/%--//' \
+ $^ > $@
chmod a-w $@
# version pour le goupe de travail E-ACSL
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 0a33be177e00f7941251fd59f5c2279bd45ab1b1..e2b407e15a02f66b65697f34c83ebbf1d4840def 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -4,6 +4,8 @@
\begin{itemize}
\item \changeinsection{locations}{Fix example \ref{ex:tset}}
+\item \changeinsection{pointers}{Add grammar of memory-related terms and
+ predicates}
\end{itemize}
\subsection{Version 1.7}
diff --git a/src/plugins/e-acsl/doc/refman/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
index bcd7fed2736b657802155bcd2c7166854a3bb46b..8eacf0ee12c8f5c79dec65a1ebc5094e460dc601 100644
--- a/src/plugins/e-acsl/doc/refman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -1 +1 @@
-\newcommand{\eacslversion}{0.3}
+\newcommand{\eacslversion}{0.4}
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
index 51719d3d384b090aface34a61becfd4faa963e13..c0a25d556aa20064bd9f4384fbbfca0e0eaafe18 100644
--- a/src/plugins/e-acsl/doc/refman/macros_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/macros_modern.tex
@@ -106,7 +106,7 @@
%%% Commandes et environnements pour la version relative à l'implementation
\newcommand{\highlightnotimplemented}{%
\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
- {\ul}%
+ {}%
}%
\newcommand{\notimplemented}[2][]{%
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 486e255d88cc2be55ba453aab90828aa19fa7055..6b41fe4bddb49c73557c5dbaaaff2ff6fb77ca8d 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -12,8 +12,7 @@
%Do not touch the following line. It is used in a Makefile hack to
%produce the ACSL document shipped with the Frama-C distribution.
%--\setboolean{PrintImplementationRq}{false}
-
-%\setboolean{ColorImplementationRq}{false}
+%--\setboolean{ColorImplementationRq}{false}
\usepackage{amssymb}
\usepackage{graphicx}
@@ -25,8 +24,8 @@
\usepackage{alltt}
\makeindex
-\newcommand{\acslversion}{1.7\xspace}
-\newcommand{\version}{\acslversion-1\xspace}
+\newcommand{\acslversion}{1.8\xspace}
+\newcommand{\version}{\acslversion\xspace}
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
diff --git a/src/plugins/e-acsl/doc/refman/memory.tex b/src/plugins/e-acsl/doc/refman/memory.tex
new file mode 100644
index 0000000000000000000000000000000000000000..863199e5275dd5d195d156121c6875d2ea220eea
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/memory.tex
@@ -0,0 +1,27 @@
+\begin{syntax}
+ term ::= "\null" ;
+ | "\base_addr" { one-label? } "(" term ")" ;
+ | "\block_length" { one-label? } "(" term ")" ;
+ | "\offset" { one-label? } "(" term ")" ;
+ | { "\allocation" one-label? "(" term ")" };
+ \
+ pred ::= { "\allocable" one-label? "(" term ")" };
+ | { "\freeable" one-label? "(" term ")" };
+ | { "\fresh" two-labels? "(" term, term ")" };
+ | "\valid" { one-label? } "(" location-address ")" ;
+ | "\valid_read" { one-label? } "(" location-address ")";
+ | { "\separated" "(" location-address "," location-addresses ")" };
+ \
+ { one-label } ::= { "{" id "}" } ;
+ \
+ { two-labels } ::= { "{" id, id "}" } ;
+ \
+ location-addresses ::= location-address ("," location-address)*
+ \
+ location-address ::= tset
+\end{syntax}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End:
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 3079971445ff6a6a33ac372bf62e5fd991d46ba7..71de79df78646bec39e0e573533827c748036b15 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -77,8 +77,8 @@ this form of quantifier is limited to \texttt{integer} and its subtype. Thus
there is no guarded quantification over \texttt{float}, \texttt{real}, \C
pointers or logic types.
-\item[\notimplemented{Iterator quantification}] In order to iterate over
- non-integer types, \eacsl introduces a notion of $iterators$ over types:
+\item[{\highlightnotimplemented{Iterator quantification}}] In order to iterate
+ over non-integer types, \eacsl introduces a notion of $iterators$ over types:
standard \acsl unguarded quantifications are only allowed over a type which an
iterator is attached to.
@@ -111,8 +111,8 @@ pointers or logic types.
\cinput{link.c}
\end{example}
-\item[\notimplemented{Unguarded quantification}] They are only allowed over
- boolean and char.
+\item[{\highlightnotimplemented{Unguarded quantification}}] They are only
+ allowed over boolean and char.
\end{description}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -652,6 +652,16 @@ axiomatics.
\except{separation, allocation and deallocation is unsupported}
+Figure~\ref{fig:gram:memory} shows the additional constructs for terms and
+predicates which are related to memory location.
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\linewidth}
+ \input{memory_modern.bnf}
+ \end{minipage}}
+ \caption{Grammar extension of terms and predicates about memory}
+\label{fig:gram:memory}
+\end{figure}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Memory blocks and pointer dereferencing}
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 63a5d85f40efbfa5788f3c699ba4e5290e24d129..65eea28136894647be383f492fc69c1ca6a26a0c 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -14,14 +14,14 @@ default: main.pdf
main.pdf: $(DEPS_MODERN)
-EACSL_VERSION= 0.3
-FC_VERSION= Fluorine-20130601
+EACSL_VERSION= 0.4
+FC_VERSION= Neon-20140301
-EACSL_DIR=$(HOME)/plugins/e-acsl
+EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install:
cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
- cp -f main.pdf \
+# cp -f main.pdf \
$(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 91697bfe925ba5f3e8fe22f58728e0a5d69c27c6..ba3ec142044a61ff72531de4c9c720deae7f93d4 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -4,6 +4,12 @@ This chapter summarizes the changes in this documentation between each \eacsl
release. First we list changes of the last release.
\section*{E-ACSL \eacslversion}
+
+\begin{itemize}
+\item No change
+\end{itemize}
+
+\section*{E-ACSL 0.3}
\begin{itemize}
\item \textbf{Introduction:} reference the \eacsl tutorial.
\item \textbf{Memory-related Annotations:} document the
diff --git a/src/plugins/e-acsl/doc/userman/eacslversion.tex b/src/plugins/e-acsl/doc/userman/eacslversion.tex
index c6157275e0d0057a1ab29ef9c26f2f3c55fea50f..14953a5d923cce7b011879de958b7ec761304507 100644
--- a/src/plugins/e-acsl/doc/userman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/userman/eacslversion.tex
@@ -1,2 +1,2 @@
-\newcommand{\eacslversion}{0.3\xspace}
-\newcommand{\fcversion}{Fluorine-20130601\xspace}
+\newcommand{\eacslversion}{0.4\xspace}
+\newcommand{\fcversion}{Neon-20140301\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
deleted file mode 100644
index f692a5c85fe1f7237ed9c82ca60536c44b1a8cba..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 2bf473c3f6f2611d78e7ace37472dda40d91ef27..5481747bdf1a1e2003589cf1af2797b06805cff0 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 2be5aef8cc6208e03e134c208e2ef6efc5612e2c..e3aaef4d9dfdc6a1d6f674c7e5ddc4d858642004 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 84d1a35f3a4d504a47643e8d789ae95c055306c5..8085d98d89b59db01d1a1a6d3876bde0b7156de1 100644
--- a/src/plugins/e-acsl/error.ml
+++ b/src/plugins/e-acsl/error.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 cf631d133c3d0b80084cb84c00806780e0e4705b..aee8352d33bb13411e6c0d71babff74deb07fe7e 100644
--- a/src/plugins/e-acsl/error.mli
+++ b/src/plugins/e-acsl/error.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/known_bugs/bts1636_memory_leak_literal_strings.i b/src/plugins/e-acsl/known_bugs/bts1636_memory_leak_literal_strings.i
new file mode 100644
index 0000000000000000000000000000000000000000..8817fd839d63c551ae1f1233c36ce9a538729902
--- /dev/null
+++ b/src/plugins/e-acsl/known_bugs/bts1636_memory_leak_literal_strings.i
@@ -0,0 +1,9 @@
+int main(void)
+{
+ char *s;
+ for(int i = 0; i < 10; i++) {
+ s = "012";
+ }
+ /*@ assert s[1] == '1'; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/license/CEA_LGPL b/src/plugins/e-acsl/license/CEA_LGPL
index 2ea979db1e82296f85468f13c3626e6551dcc291..81fb012d3e071bb796f42421dbda7cd119235ea7 100644
--- a/src/plugins/e-acsl/license/CEA_LGPL
+++ b/src/plugins/e-acsl/license/CEA_LGPL
@@ -1,7 +1,7 @@
This file is part of the Frama-C's E-ACSL plug-in.
-Copyright (C) 2012-2013
+Copyright (C) 2012-2014
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 d38108e24adc2d2024f9160a4fe27245c9a207af..2cd271302a16b9fd7aac43275ede4379f70bc2c4 100644
--- a/src/plugins/e-acsl/local_config.mli
+++ b/src/plugins/e-acsl/local_config.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 c36464f3e28acf284fd0e91de542ff224e7803ec..88197b615e94b0143ebd0c811b0bc599a67f60e4 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 ed15bfe89e9b4c1f2c48e65b04b9f25d9ce57237..3ee1b4b7d8fe557774167210d3bf3658ff76accf 100644
--- a/src/plugins/e-acsl/loops.mli
+++ b/src/plugins/e-acsl/loops.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 28fdb37ea4012971d9fc39aa6bd15db9b309663a..4ec28617165680e1397a03a726332aa0c54887a7 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index c15600e5e9f9f312cb6899fa4e23d76e0b088f5b..b76a11696a940a842ba3af158e78ef3f15d0b191 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 44655980f2ef48718658af96ff4cde981a4df380..3f8b599ac848c6b67042c36cdc589f6c28efe17a 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/mpz.ml b/src/plugins/e-acsl/mpz.ml
index f6fedbdd9fa4d959436707903ca3d123dcbb1c7f..a53e01d9ec13c8a6fe7d77eb1fb2e559ea1999a3 100644
--- a/src/plugins/e-acsl/mpz.ml
+++ b/src/plugins/e-acsl/mpz.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/mpz.mli b/src/plugins/e-acsl/mpz.mli
index cebd5bbdac66a1fb3a1abf5d3a8ab932bbe3099c..f355453e9a8c6d0b46bfe9f7327cae2b31cdba5a 100644
--- a/src/plugins/e-acsl/mpz.mli
+++ b/src/plugins/e-acsl/mpz.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 fdce3c110bfd38b1c0a93008b985eeebee7548b2..e43673c5eff5c861a1f1c1798e5d1c4982031d00 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 439cc8b9f25dbead407c6b5a32a9fd14c449ca1d..ac41e7a02716fe76e6c543d2023750ce4eabbc07 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 9d3a014893703cddb86a9bf030eeb7f12a8098a4..31b65d7bab89cb9122f0d0bc7a262606a9431bef 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/pre_analysis.mli b/src/plugins/e-acsl/pre_analysis.mli
index c7b016026d8b73b11ac6841ac56a443e98865eff..7c26f02b61ab2041b50ce39978729e51878f02fe 100644
--- a/src/plugins/e-acsl/pre_analysis.mli
+++ b/src/plugins/e-acsl/pre_analysis.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index 93fc6c3e8f2a28896f30f4940422cec9d7001dc7..0b12c06230ec1a7dd7ea3d16409b25b28732baec 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/pre_visit.mli b/src/plugins/e-acsl/pre_visit.mli
index 13ae14e0b609a29bbd92c0c341d5d423455ba163..83c2c3d6a08e8696022869bd692a1b1aa504b392 100644
--- a/src/plugins/e-acsl/pre_visit.mli
+++ b/src/plugins/e-acsl/pre_visit.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 41d8091739858615b0d5435842d739997bde7b3f..72446d1df06be18ccfbaa79cff7bcc397f95919a 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 06434557ededeac4fa1717dd1716185d29ad89e2..dcbb5554ab79ad17cdebb1c86dada8f2641efa09 100644
--- a/src/plugins/e-acsl/quantif.mli
+++ b/src/plugins/e-acsl/quantif.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 a1a4305f8ae5b71da99d4cb8998c44e12c7c6729..19a8dbdd2554936aaa905a28d6e5d5488a6b96f4 100644
--- a/src/plugins/e-acsl/rte.ml
+++ b/src/plugins/e-acsl/rte.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 309463cbcfd708abc06c16c34aad7f15c9027caa..fdc2410215e9f7af52f2fef55ea7380ba87da12c 100644
--- a/src/plugins/e-acsl/rte.mli
+++ b/src/plugins/e-acsl/rte.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl.c
index 20371706d6d8d5be4c482460bb9e108164e1961f..ea9b69b65cd8b241c3bab27af3e4ee467d52d103 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* 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 87dd0a981bdb7db63662d54a5a8009d749e7caeb..7ec9091f22cad5969a65c4242085a195a26aaa07 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
index 69c84e1bf59dea34e081ff7fb552f30909220fc9..60fdc2b60dbcdd85403c88fc025183bbeea9c33d 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
index 4485dc3166351d3ac88128375499a5530511e2bf..0acb34103b314d7b47120a98491d13f03c5c21e2 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index 31dd8ed5695bd8d91f8e25a4b55d9ec25e3f4911..384dd041d687c81ea33b694b19b2d4fb25e97629 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
index 3738659e58962a4dd0cfa57b07befdb70a369f72..c34c24336c57e6478c7bc6e894ea639a77bfc5c3 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
index dba0d07583aadacfaa05ffb12ff07b76b4ab8b47..6e7668ff4ea17e672d043764fb4a95eb2c9f0642 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index 3a7dc723cd63fe0251ea133a6e26cfed423635e1..f3e115a60ea597d5fb56b4065ab0b769ae7c9d14 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index a0318bfaab9dbdf48780f5256984944a2253e01f..fd788470d8fe588cc9577be6f611db832e7727fe 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index 0dfb43597562d94fde53df8f9ee7229234a27fda..268626ea6935f351ddcba734eacfcf61a05c1e36 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
index dd48e1f437f3fbc7baf84650269323e63e1ba512..ae692c0f82ee7ad7c4d4776e06710c1827466400 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
index 71be201eb5b6a274bf7721b139b1c4f0006ba1ab..c537246d225d15cd26ddfc24ffb29481a72e3937 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
@@ -2,7 +2,7 @@
/* */
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
-/* Copyright (C) 2012-2013 */
+/* Copyright (C) 2012-2014 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
index 73d3ac2b865191eaf0bab61e438854128a8e74b8..877d15f251ecc37cde876cc196034793d12306f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
@@ -18,7 +18,7 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
- __fc_fopen[0..511] ∈ {0}
+ __fc_fopen[0..1] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
index 73d3ac2b865191eaf0bab61e438854128a8e74b8..877d15f251ecc37cde876cc196034793d12306f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
@@ -18,7 +18,7 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
- __fc_fopen[0..511] ∈ {0}
+ __fc_fopen[0..1] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index 7cbe7d91981b3b8f32b4307dd9e44fdbcd322c09..9866acdacf7365137e57b4ad742efa8eb9517266 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
extern FILE *__fc_stdout;
-FILE __fc_fopen[512];
+FILE __fc_fopen[2];
FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index 7cbe7d91981b3b8f32b4307dd9e44fdbcd322c09..9866acdacf7365137e57b4ad742efa8eb9517266 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
extern FILE *__fc_stdout;
-FILE __fc_fopen[512];
+FILE __fc_fopen[2];
FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 15ce901b0d3fed78f783e493cae6a60b0a09e29f..ea0fea0d0e460043dc2c93383f38ba118e2cbf9a 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 dca783d90e3d7707063eb21c778ba6711ed56503..a9dd3da677464049fdcf60b7c1a35f4946405d27 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/translate.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 1aaef3228f6c47c93c7ddbfcaa5c6a22682ac65c..62f35bb1bccafcb98f9e42493db10e36e5e5e2b8 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 1ce906d768926b8bc1835a7c56cf5b0169653744..ae21f7bb4b4daf24c120fbd2bd3342aeffba482d 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 b6e46d9a3b9fa2d0a8b17999461ef33da817439b..5129e021d945cce8b7f6ccda508bb80908dce6da 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* 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 687da3b7d95f3a1b9d61fbc876d63f4d9fdd86f7..160422302f1790aff4ef69f98008b12f88a1b8e9 100644
--- a/src/plugins/e-acsl/visit.mli
+++ b/src/plugins/e-acsl/visit.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
-(* Copyright (C) 2012-2013 *)
+(* Copyright (C) 2012-2014 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)