[E-ACSL] do not call __clean when not required + ongoing manual

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},
+}
+  

src/plugins/e-acsl/doc/userman/limitations.tex

-\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}

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}
 

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"

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

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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: