diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index e5e2195db58a135d2561bcee6b1700c18761511a..dfee6e09e378a2341b54cde794f11e659dbd2281 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -122,3 +122,11 @@
   year      = {2006},
   pages     = {25-37},
 }
+
+@article{rv13,
+  author = {Nikolaï Kosmatov and Guillaume Petiot and Julien Signoles},
+  title  = {{Optimized Memory Monitoring for Runtime Assertion Checking of C
+             Programs}},
+  note = {Submitted for publication},
+}
+  
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 11a17baf6c88d4b1597d87632f36f9986df0e220..c217294ec2cac9aca538c050a6d148570b96123b 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -1,10 +1,38 @@
-\chapter{Known limitations}
+\chapter{Known Limitations}
+
+The development of the \eacsl plug-in is still ongoing. First, the whole \eacsl
+reference manual~\cite{eacsl} is not yet supported. Which annotations are
+already translated into \C code and which are not is defined in a separated
+document~\cite{eacsl-implem}. Second, even if we do our best, bugs may exist. If
+you find a new one, please report it on the bug tracking system (see Chapter 10
+of the \framac User Manual~\cite{userman}). Third, there are some additional
+known limitations, which could be annoying for the user in some cases, but are
+hard to lift. Thus they could be there for a while. Lifting them could be part
+of commercial supports\footnote{Contact us or read
+  \url{http://frama-c.com/support.html} for additional details.}.
+
+\section{Undefined Value}
+\index{Undefined value}
 
 \begin{itemize}
-\item of course, annotations that are not yet translated~\cite{eacsl-implem}
-\item function without code
-\item recursive functions
-\item function pointers
-\item complex control flow graph
-\item read KNOWN\_BUGS
+\item use of undefined values are not tracked in annotations
+\item missing guards for \lstinline+\offset+, \lstinline+\block_length+ and
+  \lstinline+texbase_addr+ (\lstinline+offset(p)+ must ensures that $p$ is
+  valid)
 \end{itemize}
+
+\section{Function without Code}
+\index{Function!Without code}
+
+\section{Recursive Function}
+\index{Function!Recursive}
+
+\section{Variadic Function}
+\index{Function!Variadic}
+
+\begin{itemize}
+\item Not yet duplicated
+\end{itemize}
+
+\section{Function Pointer}
+\index{Function!Pointer}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index a16788b2dcc5997af7b36390343f98de4b6d35dd..e7026255c6fa2b4fa8580057dfe1e0345623d765 100644
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 8f3eb0c39279d55416e0f1f27232194657a0560a..65643aa020f3054d9fb79006319bbba5f27009c8 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -3,25 +3,32 @@
 This chapter is the core of this manual and describes how to use the
 plug-in. First, Section~\ref{sec:run} shows how to run the plug-in on a trivial
 example and how to execute the generated code with a standard \C compiler to
-detect invalid annotations at runtime. Then, Section~\ref{sec:custom} introduces
-how to customize the plug-in. Next, Section~\ref{sec:exec} provides additional
-details on the execution of the generated code. Section~\ref{sec:rte} explains
-how the plug-in handles potential runtime errors in the generated code, while
-Section~\ref{sec:incomplete} focus on how to deal with incomplete programs,
-\emph{i.e.} in which some functions have no body or in which there are no main
-function. After, Section~\ref{sec:combine} explains how to combine the plug-in
-with other plug-ins of \framac. Finally, Section~\ref{sec:verbose} details the
-verbosing policy of the plug-in.
+detect invalid annotations at runtime. Then, Section~\ref{sec:exec} provides
+additional details on the execution of the generated code. Section~\ref{sec:rte}
+explains how the plug-in handles potential runtime errors in the generated
+code. Next, Section~\ref{sec:incomplete} focus on how to deal with incomplete
+programs, \emph{i.e.} in which some functions have no body or in which there are
+no main function. After, Section~\ref{sec:combine} explains how to combine the
+plug-in with other plug-ins of \framac. Finally, Section~\ref{sec:custom}
+introduces how to customize the plug-in, while Section~\ref{sec:verbose} details
+the verbosing policy of the plug-in.
 
 \section{Simple Example}
 \label{sec:run}
 
-The main option of the plug-in is \optiondef{-}{e-acsl}. Consider the following
-program.
+This Section is a mini-tutorial which explains from scratch how to detect at
+runtime that an \eacsl annotation is violated thanks to the use of the plug-in.
+
+\subsection{Running \eacsl}
+
+Consider the following simple program in which the first assertion is valid
+while the second one is not.
 
 \listingname{first.i}
 \cinput{examples/first.i}
-Running \eacsl on this file is then pretty simple:
+
+Running \eacsl on this file just consists in adding the option
+\optiondef{-}{e-acsl} to the \framac command line:
 \begin{shell}
 \$ frama-c -e-acsl first.i
 [kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
@@ -42,7 +49,7 @@ Section~\ref{sec:exec}.
 Then \eacsl takes the annotated \C code as input and
 translates it into a new \framac project named \texttt{e-acsl}\footnote{The
   notion of \emph{project} is explained in Section 8.1 of the \framac user
-  manual~\cite{userman}.}. By default, the option \optionuse{-}{eacsl} does
+  manual~\cite{userman}.}. By default, the option \optionuse{-}{e-acsl} does
 nothing more. It is however possible to have a look at the generated code on the
 \framac GUI. It is also possible through the command line thanks to the kernel
 options \optionuse{-}{then-on} and \optionuse{-}{print}:
@@ -107,7 +114,6 @@ int main(void)
   /*@ assert x == 1; */
   e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
   __retres = 0;
-  __clean();
   return __retres;
 }
 \end{shell}
@@ -117,27 +123,28 @@ constant declarations and global \acsl annotations that are not in the initial
 file \texttt{first.i}. That is a part of the included \eacsl library. You can
 safely ignore it right now. The translated \texttt{main} function of
 \texttt{first.i} is displayed at the end. Two lines have been added. The first
-one is just after the unique \eacsl annotation.
+one is just after the first \eacsl annotation, while the second one is just
+after the second one.
 
 \begin{ccode}
   /*@ assert x == 0; */
   e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
+  /*@ assert x == 1; */
+  e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
 \end{ccode}
 
-It is a function call to \texttt{e\_acsl\_assert}\codeidx{e\_acsl\_assert} from
-the \eacsl library. This call performs the dynamic verification that the
-corresponding assertion is valid. More precisely, it checks that its first
-argument (here \texttt{x == 0} corresponding to the annotation) is not equal to
-0 and fails otherwise. The extra arguments are only used to display nice user
-feedback as shown later in Section~\ref{sec:exec}.
+They are function calls to \texttt{e\_acsl\_assert}\codeidx{e\_acsl\_assert}
+which is defined in the \eacsl library. Each call performs the dynamic
+verification that the corresponding assertion is valid. More precisely, it
+checks that its first argument (here \texttt{x == 0} or \texttt{x == 1}
+corresponding to the annotations) is not equal to 0 and fails otherwise. The
+extra arguments are only used to display nice user feedback as shown later in
+Section~\ref{sec:exec}.
 
-The second additional line is the call to \texttt{\_\_clean}\codeidx{\_\_clean}
-(once again from the \eacsl library) just before the \texttt{return}
-statement. This call is required to clean potential extra allocations done by
-the \eacsl library (actually none in this example).
+\subsection{Executing the generated code}
 
 By using the option \optionuse{-}{ocode} of \framac, we can redirect the
-generate code into a \C file as follows.
+generated code into a \C file as follows.
 
 \begin{shell}
 \$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
@@ -152,21 +159,12 @@ The failing predicate is:
 x == 1.
 \end{shell}
 
-\section{Customizing the Plug-in}
-\label{sec:custom}
-
-\begin{itemize}
-\item -e-acsl-project
-\item -e-acsl-check
-\item -eacsl-share
-\end{itemize}
-
 \section{Execution Environment of the Generated Code}
 \label{sec:exec}
 
 \begin{itemize}
 \item takes care of architecture (32, 64 bits)
-\item memory model (linking issue)
+\item memory model (linking issue)~\cite{rv13}
 \item GMP (linking issue)
 \item customizing e\_acsl\_assert
 \end{itemize}
@@ -194,6 +192,15 @@ x == 1.
 \item -e-acsl-prepare
 \end{itemize}
 
+\section{Customizing the Plug-in}
+\label{sec:custom}
+
+\begin{itemize}
+\item -e-acsl-project
+\item -e-acsl-check
+\item -eacsl-share
+\end{itemize}
+
 \section{Verbosing Policy}
 \label{sec:verbose}
 
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 3fa1ed3f482a2014546f5557a6718a6b2fea0cde..4289d1aeb326589de3552238458eddc1f85ea4e9 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -57,10 +57,12 @@ module Env: sig
   val add_init: kernel_function -> Varinfo.Hptset.t option -> unit
   val mem_init: kernel_function -> Varinfo.Hptset.t option -> bool
   val find: kernel_function -> Varinfo.Hptset.t option Stmt.Hashtbl.t 
-  module StartData: Dataflow.StmtStartData with type data = Varinfo.Hptset.t option
+  module StartData: 
+    Dataflow.StmtStartData with type data = Varinfo.Hptset.t option
   val is_consolidated: unit -> bool
   val consolidate: Varinfo.Hptset.t -> unit
   val consolidated_mem: varinfo -> bool
+  val is_empty: unit -> bool
 end = struct
 
   let current_kf = ref (Kernel_function.dummy ())
@@ -128,6 +130,20 @@ end = struct
 
   let is_consolidated () = !is_consolidated_ref
 
+  let is_empty () =
+    try
+      Kernel_function.Hashtbl.iter
+	(fun _ h -> 
+	  Stmt.Hashtbl.iter
+	    (fun _ set -> match set with
+	    | None -> ()
+	    | Some s -> if not (Varinfo.Hptset.is_empty s) then raise Exit)
+	    h)
+	tbl;
+      true
+    with Exit ->
+      false
+
   let clear () = 
     Kernel_function.Hashtbl.clear tbl;
     consolidated_set := Varinfo.Hptset.empty;
@@ -657,6 +673,8 @@ let old_must_model_vi bhv ?kf ?stmt vi =
   Options.Full_mmodel.get ()
   || must_model_vi ?kf ?stmt (Cil.get_original_varinfo bhv vi)
 
+let use_model () = not (Env.is_empty ())
+
 (*
 Local Variables:
 compile-command: "make"
diff --git a/src/plugins/e-acsl/pre_analysis.mli b/src/plugins/e-acsl/pre_analysis.mli
index c8f415f9c37f0824e76dfeb7a244e1630a2b1291..c7b016026d8b73b11ac6841ac56a443e98865eff 100644
--- a/src/plugins/e-acsl/pre_analysis.mli
+++ b/src/plugins/e-acsl/pre_analysis.mli
@@ -31,6 +31,9 @@ val init_mpz: unit -> unit
 val reset: unit -> unit
 (** Must be called to redo the analysis *)
 
+val use_model: unit -> bool
+(** Is one variable monitored (at least)? *)
+
 val must_model_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
 (** [must_model_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
     [stmt] in the given function [kf] must be tracked by the memory model
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index b300b4a90b03ee203087ccde6f8f09f6fac00087..1279d95f8e573c0aef9576ef767e64f2d28881f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -76,8 +76,6 @@ tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid.
 tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid.
 tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
 tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 41c2bc784f55fdf9e47b48c658827376cdf140e3..8e73c5319694bce36b7b100428a26523da6bc07f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -34,8 +34,6 @@ tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid.
 tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid.
 tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
 tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index 9215287caed3380e3031a4efb8d34e313d920974..cc1a00b9e52d49449c5497ea85304b0465f5b9fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -22,8 +22,6 @@ tests/e-acsl-runtime/array.i:15:[value] Assertion got status unknown.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 433107f15d98a825bc4af9c5426e76c4f73a511a..11d57291c45ff5b25c078ebda06755e811cdb1a8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -31,8 +31,6 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
 tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
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 7dfd9be7ba81c920e2adaa07b036b4ef16fa15d3..6b4160ab4f5f40013db880d964f6b0152d8d5c32 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
@@ -52,8 +52,6 @@
 [value] using specification for function __full_init
 [value] using specification for function __literal_string
 [value] using specification for function printf
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
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 7dfd9be7ba81c920e2adaa07b036b4ef16fa15d3..6b4160ab4f5f40013db880d964f6b0152d8d5c32 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
@@ -52,8 +52,6 @@
 [value] using specification for function __full_init
 [value] using specification for function __literal_string
 [value] using specification for function printf
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index 82cc5bc52903ccf63bc4c61d3dae941e4f18e132..a1a3020c004486c2486843d274ba6e01be20397f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -22,8 +22,6 @@ tests/e-acsl-runtime/cast.i:15:[value] Assertion got status valid.
 tests/e-acsl-runtime/cast.i:16:[value] Assertion got status valid.
 tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 9127149ae578c398e728f44813816355dc775d1a..8f2c5529f0b334b21244d9dbd24a40cf0f176d2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -43,8 +43,6 @@ share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition
 [value] using specification for function __gmpz_get_ui
 share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
 tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index 093118660c176a509a13bd2406d271b889443ec1..a12c59b85ff7aab398d5ca45d3f9a85f754627a6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -52,8 +52,6 @@ tests/e-acsl-runtime/comparison.i:26:[value] Assertion got status valid.
 tests/e-acsl-runtime/comparison.i:27:[value] Assertion got status valid.
 tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
 tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 75f4fda28abc557b8977e6491627147c87408ac6..fd74490b3a836b576bdf51471f1340bf3f2b8cec 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -36,8 +36,6 @@ tests/e-acsl-runtime/comparison.i:26:[value] Assertion got status valid.
 tests/e-acsl-runtime/comparison.i:27:[value] Assertion got status valid.
 tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
 tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
index 98a5da439f08e6d2d45e0d1416eb7bbdaabdd830..a00d94a5c13dc54cb932c8a1494f942b4bd20f24 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
@@ -14,8 +14,6 @@
   __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __memory_size ∈ [--..--]
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index 98a5da439f08e6d2d45e0d1416eb7bbdaabdd830..a00d94a5c13dc54cb932c8a1494f942b4bd20f24 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -14,8 +14,6 @@
   __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __memory_size ∈ [--..--]
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index 6efc09c45f9f918629764c49402dce9fcdc544b4..f344f86c77a036c8912c7ef53d588817388054cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -79,8 +79,6 @@ tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: pos
 tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated.
 tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid.
 tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function f:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 38c24c42cda88cc3d9a74409f4709ff950ace984..4095e8e8f248d4da882d8de62384827a47c65b7f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -63,8 +63,6 @@ tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: pos
 tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated.
 tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid.
 tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function f:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 32c909ea76865515beb81bdca414d0d655dc5c81..f81cd5c4507f5d1599432764c652b4be7c89e159 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -104,7 +102,6 @@ int main(void)
   e_acsl_assert(4 / y == 2,(char *)"Assertion",(char *)"main",
                 (char *)"4/y == 2",33);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
index 7951ab45651169fe71c19049cd1bfbec68ba1eb9..db6551fc4c8f8a8244265c072e2106bcfcbf4309 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
@@ -134,8 +134,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -702,7 +700,6 @@ int main(void)
     __gmpz_clear(__e_acsl_56);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index 2cb5a1becaa512185b09b1796753c69a8e8dc548..6d7334bb1b3dc1cdb1b5dd93129d0648ce7f6fb9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -66,7 +64,6 @@ int main(void)
   e_acsl_assert(T1[1] != T2[1],(char *)"Assertion",(char *)"main",
                 (char *)"T1[1] != T2[1]",16);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
index 733f2aed30c37729b0c648286b53c1b210599ebf..0824b1835fc648c2049e98fa73e531f8822fcb2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
@@ -50,8 +50,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -108,7 +106,6 @@ int main(void)
     __gmpz_clear(__e_acsl_4);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
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 0fb8963aa8e478632ddf7fd77c41e8e1ee5075aa..73315d4218615f33c0d4d7a88fe7de0fd2a51f3a 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
@@ -69,8 +69,6 @@ extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
 
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -101,7 +99,6 @@ int main(void)
   __literal_string((void *)__e_acsl_literal_string);
   printf(__e_acsl_literal_string,x,t[0],t[i]);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
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 0fb8963aa8e478632ddf7fd77c41e8e1ee5075aa..73315d4218615f33c0d4d7a88fe7de0fd2a51f3a 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
@@ -69,8 +69,6 @@ extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
 
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -101,7 +99,6 @@ int main(void)
   __literal_string((void *)__e_acsl_literal_string);
   printf(__e_acsl_literal_string,x,t[0],t[i]);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 9904c081be8cf982bb1d1339ab214db4257e6d72..8e08c6a542f3cd303649e46d7c4b8681cd9fab82 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -67,7 +65,6 @@ int main(void)
                 (char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
                 20);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
index c13552cebb9406f8844afd0b1d1affbe0a243c98..678d661b508ba1b3283f3ed21a47bbbe678b6729 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
@@ -75,8 +75,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -187,7 +185,6 @@ int main(void)
     __gmpz_clear(__e_acsl_cast_8);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 10a9ae302de368279f30a1cdc0df7477f9dd94c8..c7b845b7b87bdd23ebf18fb44d9f1557fd91d3a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -40,8 +40,6 @@ extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
 
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -112,7 +110,6 @@ int main(void)
   e_acsl_assert(1 != -2,(char *)"Assertion",(char *)"main",(char *)"1 != -2",
                 29);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index 2dd28772e462e7e86dc3d9a84e3e3012b70742d0..e058ae1281c33b605672859c58af7d9cb67322e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -75,8 +75,6 @@ extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
 
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -343,7 +341,6 @@ int main(void)
     __gmpz_clear(__e_acsl_neg_6);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index e760f254d26c5dbd0b10468a1f5eb33f6441dce4..8f4a9de6f63aebfad7b6f2fc7e363e8e500d5ded 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -47,7 +45,6 @@ int main(void)
     /*@ assert \false; */
     e_acsl_assert(0,(char *)"Assertion",(char *)"main",(char *)"\\false",8);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
index e760f254d26c5dbd0b10468a1f5eb33f6441dce4..8f4a9de6f63aebfad7b6f2fc7e363e8e500d5ded 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -47,7 +45,6 @@ int main(void)
     /*@ assert \false; */
     e_acsl_assert(0,(char *)"Assertion",(char *)"main",(char *)"\\false",8);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 1fc792e0c37c8f1f047fbc86764aa5919b45c9b3..087b3740e9c8a44650ceb5b24a380d69c4000a49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -351,7 +349,6 @@ int main(void)
   __e_acsl_m();
   __e_acsl_n();
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
index 222e697f71e1994630c6a6844971ad1a87b04f94..563457ac4c0691a989a12ab26f6780812abd3675 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -67,8 +67,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -768,7 +766,6 @@ int main(void)
   __e_acsl_m();
   __e_acsl_n();
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 7a057561eb271177cecfaf17e1c0a69f1c4609f0..04746fe08b6b98657275d45b02a402669a2fcb11 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -51,8 +51,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -91,7 +89,6 @@ int main(void)
     __gmpz_clear(__e_acsl);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index 2df187c7929c93a437ad8e1866d59f0c116d19bb..2621d3046fdcbe47a9418fe288aa304616d96870 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -61,8 +61,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -128,7 +126,6 @@ int main(void)
     __gmpz_clear(__e_acsl_5);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index 51a00d96d814bff451a415e7747c493d108b0d95..aca285a01c3a8d494ffdf4dd5cc3358b623095fe 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -62,7 +60,6 @@ int main(void)
     }
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
index ab0778af061bf2ee4ce7ad2a8d7282174dcea9a1..3be9888f60daed3b2f49eee32ce1b6d473400fbf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
@@ -50,8 +50,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -114,7 +112,6 @@ int main(void)
     }
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index ccac293a0dc47e6f0bc70afbd98bef75d8a8e02a..8ca7ecc921ec3bccee6b862530b15aaa860fbbdf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -76,7 +74,6 @@ int main(void)
   __retres = __e_acsl_main();
   e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"main",
                 (char *)"X == 3",9);
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
index a00b658612eacc8581827bca4f383db0020af7db..c3ec0786cc155f66528376c452bcb32e333b0604 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -50,8 +50,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -137,7 +135,6 @@ int main(void)
                   (char *)"X == 3",9);
     __gmpz_clear(__e_acsl_X);
     __gmpz_clear(__e_acsl);
-    __clean();
     return __retres;
   }
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index f52c93260c1341f94fc5d0ec2a5c86de83ccd4f1..80f02cb85ca30dd7f5c2bfd7ca4ee497cccabefb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -193,7 +191,6 @@ int main(void)
                   (char *)"main",(char *)"(x!=0&&y!=0) == (x!=0)",30);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
index fce174c34d5142622fab78c115d4e1e7d62865ff..620d46cb791f23f88cf6504583b5dfb092be5aba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
@@ -77,8 +77,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -744,7 +742,6 @@ int main(void)
     __gmpz_clear(__e_acsl_49);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 1d8f35b075e1222b3fd916ebb56fa1a6b2e47d83..1132ef85eab8fc873961e4ab405ff235be0de57d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -197,7 +195,6 @@ int main(void)
   e_acsl_assert(found == 0,(char *)"Assertion",(char *)"main",
                 (char *)"found == 0",36);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
index 9b70bcfdd6ce2547c6bc487aa30a89f806ceb919..793814aa907d7c5a3f7d04292527a438cadd81f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -79,8 +79,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -398,7 +396,6 @@ int main(void)
     __gmpz_clear(__e_acsl_2);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index dc3e01f74048ba51e7569931a159417234846562..59d45aafae40be9152f1e72c6a47842ca6b9ca94 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -86,7 +84,6 @@ int main(void)
                   (char *)"x >= 1",11);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
index edad0b3115fe94327cd3817c09fe8460422cc21b..f798075624ac148fe0720583809ae9d4e74aaf78 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
@@ -50,8 +50,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -178,7 +176,6 @@ int main(void)
     __gmpz_clear(__e_acsl_6);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index fec032c38393a1123c3b4be9d5c7076c4ef9339e..1bc9012567ae53999ee1ef0e2f182cabfce782af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -50,7 +48,6 @@ int main(void)
     e_acsl_assert(x != 0,(char *)"Assertion",(char *)"main",(char *)"x != 0",
                   9);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
index fc3adb9948c4f198b3e83a0a485b2ceb8a20dc80..94958c4cf84621811049f1316eb713b0a6948d29 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
@@ -50,8 +50,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -94,7 +92,6 @@ int main(void)
     }
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index dcf4e8ae8ac1ddfd750b9bdb9e59da9c07dc47c0..781f248536ddc51d738d1fd6a3b46bbdb5f666a1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -45,7 +43,6 @@ int main(void)
   e_acsl_assert((void *)0 == (void *)0,(char *)"Assertion",(char *)"main",
                 (char *)"\\null == (void *)0",8);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
index dcf4e8ae8ac1ddfd750b9bdb9e59da9c07dc47c0..781f248536ddc51d738d1fd6a3b46bbdb5f666a1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -45,7 +43,6 @@ int main(void)
   e_acsl_assert((void *)0 == (void *)0,(char *)"Assertion",(char *)"main",
                 (char *)"\\null == (void *)0",8);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index e9fbeb377ccc8f13edcc0bc991c4ba0249bd6c7e..0573dd7bc66d74bd54ad2b42974790fbe12929f9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -34,8 +34,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -52,7 +50,6 @@ int main(void)
   e_acsl_assert(false != true,(char *)"Assertion",(char *)"main",
                 (char *)"false != true",13);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
index 0e05c2ad2e78ed5dfa0639adf7c122a0a9add293..ce8d5c5ded1bd68a3b3e2749d2cea4cc9965e147 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
@@ -54,8 +54,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -91,7 +89,6 @@ int main(void)
     __gmpz_clear(__e_acsl_3);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index efffa80fa16c04784d1f4ac4c5e358047d0482d0..340f7be31a7c0954a39c0eda10e25af29388652d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -227,7 +225,6 @@ int main(void)
                   27);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
index 433da33e2ada84ae52782e98ab86f80bffd7d0f0..3d4106718d5b6415c18cd5c983d90d62c7cb738f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -105,8 +105,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -671,7 +669,6 @@ int main(void)
     __gmpz_clear(__e_acsl_x_7);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index 395b9ad9031405f6d98125e8f94153a3185ced73..865e184c2f0cd8b46968d8c673cf672cbc29e211 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -102,7 +100,6 @@ int main(void)
   __e_acsl_g(Y);
   __e_acsl_h();
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
index e927b04f98f5532459f433cfe89b768a3c1ce265..96a739b8a393b26b67c1afcd819842964d73dd5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
@@ -71,8 +71,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -185,7 +183,6 @@ int main(void)
   __e_acsl_g(Y);
   __e_acsl_h();
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index c20896ea2a1c8dcdb0f543a035e170d366a2a641..f4235f2d41416048ec2c65322bc3967905f428cf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -48,7 +46,6 @@ int main(void)
   e_acsl_assert(4 == 4,(char *)"Assertion",(char *)"main",
                 (char *)"sizeof(int) == sizeof(x)",10);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
index 5ab7bfcda082aefa694ec97d7c0aaf51e912b94d..3e21d415824133b8e7a39ebbdf5653fd9a1518a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
@@ -50,8 +50,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -79,7 +77,6 @@ int main(void)
     __gmpz_clear(__e_acsl_sizeof_2);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index e9e6ac009e7ebc1880631519ea95c39da21bba51..5464655b6a1c928398d4f713cb4ce27aa6485df2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -142,7 +140,6 @@ int main(void)
     e_acsl_assert(x == 7,(char *)"Postcondition",(char *)"main",
                   (char *)"x == 7",47);
   }
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
index f5fefb3fd3eb62a1698528376135f018f08a0c0c..b90185e00f29ff156795d6b3044fb9a74f306752 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
@@ -67,8 +67,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -412,7 +410,6 @@ int main(void)
     __gmpz_clear(__e_acsl_x_13);
     __gmpz_clear(__e_acsl_21);
   }
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index 50ecf913687bd02d765b2f6f666b6160b877d0b5..e5f2afc873bdf96422ad8050665cab57ba262c06 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -47,7 +45,6 @@ int main(void)
   /*@ assert \true; */
   e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"\\true",10);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
index 50ecf913687bd02d765b2f6f666b6160b877d0b5..e5f2afc873bdf96422ad8050665cab57ba262c06 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
@@ -30,8 +30,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -47,7 +45,6 @@ int main(void)
   /*@ assert \true; */
   e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"\\true",10);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
index 351227afff088e6237d029c636e0737c81cc405c..2cc49bb5891e26c3e39d361f390363eb574269a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
@@ -31,8 +31,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -48,7 +46,6 @@ int main(void)
   e_acsl_assert((int)x == 0,(char *)"Assertion",(char *)"main",
                 (char *)"x == 0",11);
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
index fcdc81e2bb1492a492d76ba319617026fff95007..ef6b75f265646019e39c62e58f3eeb713d7f7985 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
@@ -61,8 +61,6 @@ axiomatic
   
   }
  */
-extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
-
 extern size_t __memory_size;
 
 /*@
@@ -89,7 +87,6 @@ int main(void)
     __gmpz_clear(__e_acsl);
   }
   __retres = 0;
-  __clean();
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 21eb72b12c6834976ccf439a3e3f6a16077b9082..2c30e867176dacb3f5ad51a07725164985ae6cf6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -33,8 +33,6 @@ share/e-acsl/e_acsl_gmp.h:70:[value] Function __gmpz_init_set_str: precondition
 share/e-acsl/e_acsl_gmp.h:72:[value] Function __gmpz_init_set_str: postcondition got status valid.
 share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status unknown.
 tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 45dd10f93281c73807be27ee9ee749bbefca8f68..6765c95a66b0d6dcb2d777dafc99a02e1d8b4d35 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -30,8 +30,6 @@ share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 0646e5d771e25d04cf3d179c48ff9afc9c0f8fff..52c3db63cb26efde6f83c1e7a2c6fcddc76b70e7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -28,8 +28,6 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index e1cc0dfebece0158de86b042173be16e9ae0c9a6..80c5d0ecb6be6fb640f5b179498aa7567def2209 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -19,8 +19,6 @@ tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index c92b132746347d41842040b51dede52db0c8d50a..0b45603e0e87bab65c349da42f13afebd94d7feb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -28,8 +28,6 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
 tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
index f7b6742423e5bdbfd2f7c344e89e649e8df272a2..eb59e4d0012287bd7d863fc02a03dd60973b4e61 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
@@ -19,8 +19,6 @@ tests/e-acsl-runtime/labeled_stmt.i:12:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index a7d57a71db8b6914a2eccf697d3f161647766e36..a574c5fdfff7baf7388bb769c5f717b1f1bf97cc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -52,8 +52,6 @@ tests/e-acsl-runtime/lazy.i:27:[value] Assertion got status valid.
 tests/e-acsl-runtime/lazy.i:28:[value] Assertion got status valid.
 tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
 tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index ff86726ad1825ac01dd8ccffad49939400e71c16..6f16aa0bebc8b665e9680493173afe365ccd4a71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -35,8 +35,6 @@ tests/e-acsl-runtime/lazy.i:27:[value] Assertion got status valid.
 tests/e-acsl-runtime/lazy.i:28:[value] Assertion got status valid.
 tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
 tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index c969fdd0617a5a5c8bb64ffde2ceed39bc51729b..c49a4b6f97f86748cf04211adce273eed9b475cc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -61,8 +61,6 @@ tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavi
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
 tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function search:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index e51c5749cb0a50b02449401685df005a0c729bf3..8edb0321c315a2b8e306339c3dd70ced96e10b90 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -33,8 +33,6 @@ tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavi
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
 tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function search:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index bdf626d79eb227a6ca9641659043003c26049343..229d8ac206ef167c4782d10a2431b365cdc9f397 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -26,8 +26,6 @@ share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index 866b18f0c4c59ee6ac5dd232c0ff0451fe58f082..3e80f6e83986befc2ae8f485b555e6c19fc67f33 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index a88daa868d044e046a3a90c27fbbcb164a844874..0e28b4653ee5f66a81d6c116a191f062fe891b2d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -26,8 +26,6 @@ share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index f18bf135aed2b1e259134d6534e9627a621f177c..56bdd7362f414e2d611c627f44358496e3af699f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
index 6363e5a58b9d3d9643104bf03bf2434b636e192d..c042fe69fcb078a52d870a06a33974f83312d55e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index 6363e5a58b9d3d9643104bf03bf2434b636e192d..c042fe69fcb078a52d870a06a33974f83312d55e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 8b914934925bce24eaddb3f2a2379c868e9cb317..39d083368d75980d9fe1b6e304819b9d384ae7cc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -27,8 +27,6 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
 tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index 23b14eb409e9fd784ae794b92165a8e54a297c8c..2a1a78825cdb0fd6be1b4c73dbf0c11f9c009ef3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -18,8 +18,6 @@ tests/e-acsl-runtime/other_constants.i:12:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index 98903d53a4f9021ec3cf069705b77f53184b6927..73930483c06ba07e38ebfe5a7dd2bbded0259722 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -64,8 +64,6 @@ share/e-acsl/e_acsl_gmp.h:154:[value] Function __gmpz_tdiv_q: precondition got s
 share/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_mul: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:146:[value] Function __gmpz_mul: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:147:[value] Function __gmpz_mul: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
index fdfeaf7591cd757110cadb3b2932d76645bfbe62..f19b328379c18485c24d91cd6984bd7e1b4a89af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
@@ -32,8 +32,6 @@ tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time
 tests/e-acsl-runtime/quantif.i:27:[value] Assertion got status unknown.
 tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
 tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index de5c7f26189c59ad8d5c58d3e6d58838765a86e4..c0a51f1dc786c3c555366f00bbefc5c6c009dfc3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -42,8 +42,6 @@ tests/e-acsl-runtime/result.i:18:[value] Function g: postcondition got status va
 tests/e-acsl-runtime/result.i:18:[value] Function __e_acsl_g: postcondition got status valid.
 tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status valid.
 tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function f:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index b8f05822b2d8d8f66c8a4bc9e6b25cef33e3ab21..c7db4b6ed48e3133926fd4830dbbd4da236dfdad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -23,8 +23,6 @@ tests/e-acsl-runtime/result.i:18:[value] Function g: postcondition got status va
 tests/e-acsl-runtime/result.i:18:[value] Function __e_acsl_g: postcondition got status valid.
 tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status valid.
 tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function f:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index d9c936ab3eb7eaa0b37e1270b955132ac365885b..e4f845add22e5c1f222f209397fcc7c0a01801d8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -26,8 +26,6 @@ share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index fb53bb1ce68bd012bd9f3bcb5f1af48bd638bf24..e3c63d217fa2c49fedd84950b30a61381159e30a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index 4b780be609df28bbe0d3d583a91691d4f8c9dc8b..126371015b5938e0f32fb95b16cb214a464bafdf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -32,8 +32,6 @@ share/e-acsl/e_acsl_gmp.h:37:[value] Function __gmpz_init: postcondition got sta
 share/e-acsl/e_acsl_gmp.h:131:[value] Function __gmpz_add: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:132:[value] Function __gmpz_add: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:133:[value] Function __gmpz_add: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index 0b1b0395e95bdc04ea847155216351433201e291..1f8ba2d72bbee40d9a833d3a795f7921660be9df 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -16,8 +16,6 @@
   __memory_size ∈ [--..--]
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
index 1236bc50ccc10ad10ffdf462a81977beae146f1f..55c61e4a85e8372a3c79f9be7867d5a466ddc1c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 1236bc50ccc10ad10ffdf462a81977beae146f1f..55c61e4a85e8372a3c79f9be7867d5a466ddc1c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 25938e08d6ea6e0202edccfa8437c2aedfc9a3c8..c22597fd92f9ff4d0937121a0e860928e1d87dc5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -30,8 +30,6 @@ share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
index ae9de465d6992233091c873570f27a05b2249f29..fb99d2b57df5588831bf989304f65a8028dc4b58 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
@@ -17,8 +17,6 @@
 tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
-[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 929c08ae3454bf2b9305fcba3f54bf343d6b334a..5a37b9aedc25ddad90e1ede55bf74bf2967bf2c2 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -213,30 +213,31 @@ class e_acsl_visitor prj generate = object (self)
 	      Globals.Functions.replace_by_definition 
 		spec fundec Location.unknown;
 	      let cil_fct = GFun(fundec, Location.unknown) in
-	      match main_fct with
-	      | Some main ->
-		let exp = Cil.evar ~loc:Location.unknown vi in
-		let stmt = 
-		  Cil.mkStmtOneInstr ~valid_sid:true 
-		    (Call(None, exp, [], Location.unknown))
-		in
-		vi.vreferenced <- true;
-		main.sbody.bstmts <- stmt :: main.sbody.bstmts;
-		let new_globals =
-		  List.fold_right
-		    (fun g acc -> match g with
-		    | GFun({ svar = vi }, _) when Varinfo.equal vi main.svar -> 
-		      acc
-		    | _ -> g :: acc)
-		    f.globals
-		    [ cil_fct; GFun(main, Location.unknown) ]
-		in
-		f.globals <- new_globals
-	      | None -> 
-		Kernel.warning "no entry point specified:@ \
+	      if Pre_analysis.use_model () then
+		match main_fct with
+		| Some main ->
+		  let exp = Cil.evar ~loc:Location.unknown vi in
+		  let stmt = 
+		    Cil.mkStmtOneInstr ~valid_sid:true 
+		      (Call(None, exp, [], Location.unknown))
+		  in
+		  vi.vreferenced <- true;
+		  main.sbody.bstmts <- stmt :: main.sbody.bstmts;
+		  let new_globals =
+		    List.fold_right
+		      (fun g acc -> match g with
+		      | GFun({ svar = vi }, _) when Varinfo.equal vi main.svar -> 
+			acc
+		      | _ -> g :: acc)
+		      f.globals
+		      [ cil_fct; GFun(main, Location.unknown) ]
+		  in
+		  f.globals <- new_globals
+		| None -> 
+		  Kernel.warning "no entry point specified:@ \
 you must call function `%s' by yourself" 
-		  fname;
-		f.globals <- f.globals @ [ cil_fct ]
+		    fname;
+		  f.globals <- f.globals @ [ cil_fct ]
 	    in
 	    Project.on prj build_initializer ()
 	end;
@@ -508,7 +509,7 @@ you must call function `%s' by yourself"
 	  (* JS: should be done in the new project? *)
 	  let env = deallocate_function env kf in
 	  let b, env = Env.pop_and_get env stmt ~global_clear:true Env.After in
-	  if is_main then begin
+	  if is_main && Pre_analysis.use_model () then begin
 	    let stmts = b.bstmts in
 	    let l = List.rev stmts in
 	    match l with
@@ -616,8 +617,10 @@ you must call function `%s' by yourself"
 	    (* keep the return (enclosed in a generated block) at the end;
 	       preceded by clean if any *)
 	    let init, tl = 
-	      if self#is_main kf then [ potential_clean; ret ], tl
-	      else [ ret ], l
+	      if self#is_main kf && Pre_analysis.use_model () then
+		[ potential_clean; ret ], tl
+	      else
+		[ ret ], l
 	    in
 	    blk.bstmts <-
 	      List.fold_left (fun acc v -> v :: acc) (add_locals init) tl