diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf
index 8534716381f305bdef9d38c7ad0760a3ceafc63f..ac563be3a3d94f432b37248d9c003ee6e8fd5f75 100644
Binary files a/src/plugins/e-acsl/doc/memory_model/article.pdf and b/src/plugins/e-acsl/doc/memory_model/article.pdf differ
diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex
index da83949aa83a29e4cfd7d1c4fe9100b492349f3a..17c22b46e5ec4f3386ad99da93f5393143cf6638 100644
--- a/src/plugins/e-acsl/doc/memory_model/article.tex
+++ b/src/plugins/e-acsl/doc/memory_model/article.tex
@@ -1,5 +1,5 @@
-\documentclass[a4paper,11pt,twocolumn]{article}
+\documentclass[a4paper,11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
@@ -46,9 +46,8 @@
aboveskip=0.7cm,
belowskip=0.5cm,
escapebegin={\lstsmallmath}, escapeend={\lstsmallmathend},
- emph={let,and,match,function,with,in,assert,true,false,None,Some,fun,
- int,char,void,return,size\_t,unsigned,long,struct,if,then,else,raise,type,
- method,module,end,rec,ref,val,list,for,while,break,const,short},
+ emph={int,char,void,return,size\_t,unsigned,long,struct,if,,else,for,while,
+ break,const,short},
emphstyle=\textbf
}
@@ -64,7 +63,7 @@
\begin{document}
\title{Code generation for memory monitoring}
-\author{...}
+\author{Guillaume Petiot}
\date{\today}
\maketitle
@@ -93,64 +92,76 @@ properties. \textsc{Acsl}-annotated C programs can be dealt with
\textsc{Frama-C} \cite{Frama-C}, a framework for modular analysis of C.
\textsc{Frama-C} provides a plug-in generating executable C code from
\textsc{E-Acsl} annotations, used by the implementation discussed in this paper.
+
+
+\section{Related work}
+
+
+\section{Stored information}
+
+
Memory blocks (as defined above) held properties such as their base address and
their size. \textsc{E-Acsl} provides five annotations to retrieve useful
information about blocks:
\begin{description}
-\item[$\backslash$base\_addr(p)] \hfill \\
- returns the base address of the block containing the pointer $p$
-\item[$\backslash$block\_length(p)] \hfill \\
- returns the size (in bytes) of the block containing the pointer $p$
-\item[$\backslash$offset(p)] \hfill \\
- returns the offset between $p$ and $\backslash$base\_addr($p$)
-\item[$\backslash$valid(s)] \hfill \\
+\item[${\tt \backslash base\_addr(p)}$]
+ returns the base address of the block containing pointer $p$
+\item[${\tt \backslash block\_length(p)}$]
+ returns the size (in bytes) of the block containing $p$
+\item[${\tt \backslash offset(p)}$]
+ returns the offset between $p$ and ${\tt \backslash base\_addr(p)}$
+\item[${\tt \backslash valid\_read(s)}$]
+ whether reading $*s$ is safe
+\item[${\tt \backslash valid(s)}$]
whether reading and writing $*s$ is safe
-\item[$\backslash$initialized(s)] \hfill \\
- whether the variable stored at the address $s$ has been initialized
+\item[${\tt \backslash initialized(s)}$]
+ whether $s$ has been initialized
\end{description}
Our contribution allowed the \textsc{E-Acsl} plug-in to generate executable C
code from these five annotations, thus checking these five memory properties
during execution.
-
-
-\section{Stored information}
-
For each block, we need to store the following information: the base address
(address of the first element within the block), the size (in bytes), the
-validity status (whether reading and writing the block is safe) and the
-initialization status for each byte of the block.
-Figure~\ref{fig:block_descr} illustrates the data structure (we call it
-{\em block descriptor}) chosen to store this information.
-
-
-\begin{figure}[h]
- \begin{lstlisting}
- struct _block {
- char * ptr;
- size_t size;
- int valid;
- unsigned char * init_ptr;
- unsigned long init_cpt;
- };
- \end{lstlisting}
- \caption{Block descriptor}
- \label{fig:block_descr}
-\end{figure}
-
-
-$init\_ptr$ is an array of booleans that is dynamically allocated only if
-needed. If it has been allocated, it contains a boolean for each byte of the
-block: the $n^{th}$ boolean indicates whether the $n^{th}$ byte has been
-initialized.
-
-$init\_cpt$ counts the number of initialized bytes within the block. If
-$init\_cpt = 0$ (none) or $init\_cpt = size$ (all) then $init\_ptr$ is freed.
-So, when none or all of the bytes have been initialized (the most common cases),
-the memory space needed for the block descriptor itself is reduced. This
-consistency is maintained when adding/removing an element.
+validity status (whether reading or writing the block is safe) and the
+initialization status for each byte of the block. We call {\em block descriptor}
+the data structure storing this information.
+
+%Figure~\ref{fig:block_descr} illustrates the data structure (we call it
+%{\em block descriptor}) chosen to store this information.
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+% struct _block {
+% char * ptr;
+% size_t size;
+% int valid;
+% unsigned char * init_ptr;
+% unsigned long init_cpt;
+% };
+% \end{lstlisting}
+% \caption{Block descriptor}
+% \label{fig:block_descr}
+%\end{figure}
+
+To keep the memory space occupied by this structure low, whenever none or all of
+the bytes of a memory block have been initialized (the two most common cases),
+the initialization array is freed; an integer field counting initialized bytes
+is used instead.
+
+%$init\_ptr$ is an array of booleans that is dynamically allocated only if
+%needed. If it has been allocated, it contains a boolean for each byte of the
+%block: the $n^{th}$ boolean indicates whether the $n^{th}$ byte has been
+%initialized.
+
+%$init\_cpt$ counts the number of initialized bytes within the block. If
+%$init\_cpt = 0$ (none) or $init\_cpt = size$ (all) then $init\_ptr$ is freed.
+%So, when none or all of the bytes have been initialized (the most common cases),
+%the memory space needed for the block descriptor itself is reduced. This
+%consistency is maintained when adding/removing an element.
\section{Global architecture}
@@ -165,21 +176,50 @@ consistency is maintained when adding/removing an element.
\tikzstyle{service}=[rounded corners,rectangle,inner sep=2mm,fill=gray!40]
\scalebox{0.85}{
\begin{tikzpicture}
- \node[service,rectangle,inner sep=4mm] (eacsl) at (\colB{},\rowA{}) {
- E-ACSL plug-in};
- \node [inner sep=4mm,draw](lib) at (\colB{},\rowB{})
- {Monitoring functions};
+ \node[inner sep=4mm,draw] (eacsl) at (\colB{},\rowA{})
+ {Instrumented {C} code};
+ \node[inner sep=4mm,draw](lib)at(\colB{},\rowB{}){Monitoring functions};
\node[inner sep=4mm,draw](sdda) at (\colB{},\rowC{}){Common interface};
- \node [matrix of nodes,rectangle,draw,column sep=4mm,inner sep=2.5mm]
- (sddc) at (\colB{},\rowD{}) {
- \node[service](p) at (0,0) {{\em Bittree}}; \pgfmatrixnextcell
- \node at (0,0) {or}; \pgfmatrixnextcell
- \node[service] at (0,0) { Linked list }; \pgfmatrixnextcell
- \node at (0,0) {\dots};\\
+ \node[inner sep=4mm,draw](bt) at (-1.5,\rowD{}){{\em Bittree}};
+ \node[inner sep=4mm,draw](ll) at (1.5,\rowD{}){Linked list};
+
+ \node[service] at (8,\rowA{})
+ {translated from \textsc{Acsl} specification};
+
+ \node [matrix of nodes,column sep=2mm,inner sep=2mm,draw] (mf) at
+ (8,\rowB{}) {
+ \node[service] at (0,0){$malloc$};\pgfmatrixnextcell
+ \node[service] at (0,0){$calloc$};\pgfmatrixnextcell
+ \node[service] at (0,0){$realloc$};\pgfmatrixnextcell
+ \node[service] at (0,0){$free$};\\
+ \node[service] at (0,0){$storeBlock$};\pgfmatrixnextcell
+ \node[service] at (0,0){$deleteBlock$};\pgfmatrixnextcell
+ \node[service] at (0,0){$initialize$};\pgfmatrixnextcell
+ \node[service] at (0,0){$valid$};\\
+ \node[service] at (0,0){$offset$};\pgfmatrixnextcell
+ \node[service] at (0,0){$blockLength$};\pgfmatrixnextcell
+ \node[service] at (0,0){$baseAddr$};\pgfmatrixnextcell
+ \node[service] at (0,0){$initialized$};\\
};
+
+ \node [matrix of nodes,column sep=2mm,inner sep=2mm,draw] (ci) at
+ (8,\rowC{}) {
+ \node[service] at (0,0){$add$};\pgfmatrixnextcell
+ \node[service] at (0,0){$remove$};\pgfmatrixnextcell
+ \node[service] at (0,0){$find$};\\
+ };
+
+ %\node [matrix of nodes,rectangle,draw,column sep=4mm,inner sep=2.5mm]
+ %(sddc) at (\colB{},\rowD{}) {
+ % \node at (0,0) {{\em Bittree}}; \pgfmatrixnextcell
+ % \node at (0,0) {or}; \pgfmatrixnextcell
+ % \node at (0,0) { Linked list }; \pgfmatrixnextcell
+ % \node at (0,0) {\dots};\\
+ %};
\path [<->,thick] (eacsl) edge (lib);
\path [<->,thick] (lib) edge (sdda);
- \path [<->,thick] (sdda) edge (sddc);
+ \path [<-,thick] (sdda) edge (bt);
+ \path [loosely dashed,thick] (sdda) edge (ll);
\end{tikzpicture}
}
\end{center}
@@ -189,12 +229,11 @@ consistency is maintained when adding/removing an element.
Interactions between the components of our solution are displayed by
-Figure~\ref{fig:lib}. A data structure (see
-Section~\ref{section:bittree}) stores the block descriptors. The library
-functions (see Section~\ref{section:lib}) add, remove or modify the block
-descriptors. The \textsc{E-Acsl} plug-in then perform an instrumentation (see
-Section~\ref{section:instru}) to generate executable C code. The generated code
-uses the monitoring functions of this library.
+Figure~\ref{fig:lib}. Informations about block descriptors are stored in an
+arbitrary data structure $S$ (see Section~\ref{section:bittree}). The
+\textsc{E-Acsl} plug-in performs an instrumentation to generate executable C
+code invoking monitoring functions (see Section~\ref{section:lib}) relying on
+the data structure $S$.
\section{Concrete data structure used: {\em bittree}}
@@ -218,6 +257,20 @@ this may be quite common. Self-balanced binary search trees are dismissed
because of the numerous add/remove operations implying numerous costly balancing
operations.
+\begin{figure}[h]
+ \begin{center}
+ \tikz[grow=right,level 2/.style={sibling distance=1em},level distance=3cm]
+ \node {0010 ****}
+ child { node {0010 0111} }
+ child { node {0010 1***}
+ child { node {0010 1001} }
+ child { node {0010 1101} }
+ };
+ \caption{Example of bittree}
+ \label{fig:bittree}
+ \end{center}
+\end{figure}
+
We choose to use the {\em Patricia tries} \cite{Patricia-tries} structure, which
is efficient even if the tree is unbalanced. The prefix used by a node (not a
leaf) is the greatest common prefix (on 32 or 64 bits) of its two children.
@@ -233,28 +286,6 @@ ${\tt 0010\,****}$. The $*$ means that this bit is meaningless.
Figure~\ref{fig:insertion} shows that a new node (with a new prefix) is added
when a block descriptor is inserted.
-Figure~\ref{fig:deletion} shows an example of deletion of a 8-bit block
-descriptor. Patricia tries being compact prefix trees, a node having an
-only child is deleted. So ${\tt 0010\,1***}$ becomes useless and is replaced by
-its child ${\tt 0010\,1001}$. Deleting useless nodes, or only storing useful
-ones for routing, keeps the tree exploration efficient. A 32-bit (respectively
-64-bit) bittree has a worst-case depth of 33 (respectively 65) nodes.
-
-
-\begin{figure}[h]
- \begin{center}
- \tikz[grow=right,level 2/.style={sibling distance=1em},level distance=3cm]
- \node {0010 ****}
- child { node {0010 0111} }
- child { node {0010 1***}
- child { node {0010 1001} }
- child { node {0010 1101} }
- };
- \caption{Example of bittree}
- \label{fig:bittree}
- \end{center}
-\end{figure}
-
\begin{figure}[h]
\begin{center}
\tikz[grow=right,level 2/.style={sibling distance=1em},level distance=3cm]
@@ -273,6 +304,13 @@ ones for routing, keeps the tree exploration efficient. A 32-bit (respectively
\end{center}
\end{figure}
+Figure~\ref{fig:deletion} shows an example of deletion of a 8-bit block
+descriptor. Patricia tries being compact prefix trees, a node having an
+only child is deleted. So ${\tt 0010\,1***}$ becomes useless and is replaced by
+its child ${\tt 0010\,1001}$. Deleting useless nodes, or only storing useful
+ones for routing, keeps the tree exploration efficient. A 32-bit (respectively
+64-bit) bittree has a worst-case depth of 33 (respectively 65) nodes.
+
\begin{figure}[h]
\begin{center}
\tikz[grow=right,level 2/.style={sibling distance=1em},level distance=3cm]
@@ -315,7 +353,7 @@ This algorithm is used by the final version of our implementation and is named
These experiments justify the choice of bittrees over linked lists and binary
search trees. We implemented the classic {\em merge sort} algorithm, and added
extra allocations/deallocations to put each data structure to the test.
-The program has been instrumented (see Section~\ref{section:instru}) to call our
+The program has been instrumented to call our
monitoring functions (see Section~\ref{section:lib}). The execution time of the
instrumented program using each data structure has been measured (in
micro-seconds) and is plotted against the number of calls to a function $store$
@@ -328,6 +366,7 @@ of the greatest common prefix computation (see Sub-section~\ref{section:gcpc}).
\begin{figure}[h]
+\begin{center}
\hspace{-0.5in}
\begin{tikzpicture}
\begin{axis}[xlabel={Number of calls to $store$}, ylabel={Time ($\mu$s)},
@@ -342,6 +381,7 @@ of the greatest common prefix computation (see Sub-section~\ref{section:gcpc}).
\end{tikzpicture}
\caption{Execution time plotted against the number of calls to $store$}
\label{fig:experiments}
+\end{center}
\end{figure}
@@ -364,7 +404,7 @@ linked lists exceed our 24-hour timeout.
This section presents the functions used for adding/removing/retrieving
in formations about block descriptors into our data structure (bittree). These
functions will be automatically inserted in the source code by the
-instrumentation step (see Section~\ref{section:instru}).
+instrumentation performed by the \textsc{E-Acsl} plug-in.
\subsection{Automatic allocation}
@@ -373,191 +413,236 @@ Automatic allocation functions keep track of all non-dynamically allocated
variables (but occupying memory space nevertheless), such as formal parameters,
local variables or global variables.
-\begin{lstlisting}[caption=Automatic allocation functions]
-void * _store_block
- (void * ptr, size_t size);
-void _delete_block(void * ptr);
-\end{lstlisting}
-
-
-\subsection{Dynamic allocation}
-These functions have to be used instead of those of the standard library
-({\em stdlib.h}).
-\begin{lstlisting}[caption=Dynamic allocation functions]
-void * _malloc(size_t size);
-void * _realloc
- (void * ptr, size_t size);
-void * _calloc
- (size_t nbr, size_t size);
-void _free(void * ptr);
-\end{lstlisting}
-
-
-\subsection{Initialization}
+\begin{figure}[h]
+ \begin{center}
-These functions have to be used for each assignment, to update the
-initialization status of a block descriptor. ${\tt \_initialize(ptr, size)}$
-marks the $size$ first bytes starting from $ptr$ as initialized.
-${\tt \_full\_init(ptr)}$ marks all the bytes of $ptr$ as initialized at once.
-It is designed to avoid multiple calls to ${\tt \_initialize}$ whenever it is
-possible and improves efficiency of the instrumented program.
+ %\tikz[grow=right,level 2/.style={sibling distance=1em},level distance=3cm]
+ %\node {0010 ****}
+ %child { node {0010 0111} }
+ %child { node {0010 1001} };
+ \begin{tikzpicture}
+ \node at (-3,0) {
+\begin{lstlisting}
+{ // begin of scope of v
+ T v;
+ §\highl{$storeBlock (v, sizeof (T))$}§
+ ...
+ §\highl{$deleteBlock (v)$}§
+} // end of scope of v
+\end{lstlisting}};
+
+ \path[draw, fill=gray!20] (1,-1.5)--(2,1.5)--(3,-1.5)--cycle;
+ \node at (2,-0.5) {{\em bittree}};
+ \node at (0.4,0.3) {$add$};
+ \draw[->] (0,0) -- (1, 0);
+ \node at (0.4,-.7) {$remove$};
+ \draw[->] (0,-1) -- (1, -1);
+ \end{tikzpicture}
+ \end{center}
+ \caption{store and delete block}
+\end{figure}
-\begin{lstlisting}[caption=Initialization functions]
-void _initialize
- (void * ptr, size_t size);
-void _full_init(void * ptr);
-\end{lstlisting}
-\subsection{Interrogation}
+%\begin{lstlisting}[caption=Automatic allocation functions]
+%void * _store_block(void * ptr, size_t size);
+%void _delete_block(void * ptr);
+%\end{lstlisting}
-These functions are used to retrieve information about the block descriptors
-and match the \textsc{E-Acsl} annotations we are trying to support:
-${\tt \backslash valid}$, ${\tt \backslash base\_addr}$,
-${\tt \backslash block\_length}$, ${\tt \backslash offset}$ and
-${\tt \backslash initialized}$.
-
-\begin{lstlisting}[caption=Interrogation functions]
-int _valid
- (void * ptr, size_t size);
-void * _base_addr(void * ptr);
-size_t _block_length(void * ptr);
-int _offset
- (void * ptr, size_t size);
-int _initialized
- (void * ptr, size_t size);
-\end{lstlisting}
-
-${\tt \_valid(ptr, size)}$ returns 1 if it is safe to read/write $size$ bytes
-starting from $ptr$, 0 otherwise. ${\tt \_base\_addr(ptr)}$ returns the base
-address of the block containing $ptr$ if such a block exists, NULL otherwise.
-${\tt \_block\_length(ptr)}$ returns the size (in bytes) of the block containing
-$ptr$ if such a block exists, 0 otherwise. ${\tt \_offset(ptr)}$ returns the
-offset between $ptr$ and the base address of the block containing $ptr$ if such
-a block exists, -1 otherwise. ${\tt \_initialized(ptr, size)}$ returns 1 if the
-$size$ first bytes starting from $ptr$ are initialized, 0 otherwise.
-
-
-\section{Instrumentation}
-\label{section:instru}
-
-This section presents the instrumentation performed by the \textsc{E-Acsl}
-plug-in to monitor the memory used by a program. The generated instrumented code
-uses the previously defined functions (see previous section).
-
-For each global variable, calls to ${\tt \_store\_block}$ and
-${\tt \_full\_init}$ are inserted at the beginning of the $main$ function, and a
-call to ${\tt \_delete\_block}$ at the end (see Figure~\ref{fig:globals}). For
-each formal parameter and local variable, a call to ${\tt \_store\_block}$ is
-inserted at the beginning of their scope block and a call to
-${\tt \_delete\_block}$ at the end of their scope block (see
-Figure~\ref{fig:formals} and Figure~\ref{fig:locals}). Calls to
-${\tt \_full\_init}$ and ${\tt \_initialize}$ are inserted on assignments (see
-Figure~\ref{fig:init}), and \textsc{E-Acsl} annotations are translated to the
-corresponding functions which result is tested by an assertion (see
-Figure~\ref{fig:annot}).
+\subsection{Dynamic allocation}
+These functions have to be used instead of $malloc$, $realloc$, $calloc$ and
+$free$ from the standard library.
-\begin{figure}[h]
- \begin{lstlisting}
-int * p;
-p = §\highl{\_malloc}§(32);
-§\highl{\_free}§(p);
- \end{lstlisting}
- \caption{Dynamic allocation instrumentation}
- \label{fig:alloc-dyn}
-\end{figure}
+%\begin{lstlisting}[caption=Dynamic allocation functions]
+%void * _malloc(size_t size);
+%void * _realloc(void * ptr, size_t size);
+%void * _calloc(size_t nbr, size_t size);
+%void _free(void * ptr);
+%\end{lstlisting}
-\begin{figure}[h]
- \begin{lstlisting}
-{
- int* p;
- §\highl{\_store\_block(\&p, sizeof(int*));}§
- ...
- §\highl{\_delete\_block(\&p);}§
-}
- \end{lstlisting}
- \caption{Local variable instrumentation}
- \label{fig:locals}
-\end{figure}
-
+\subsection{Initialization}
-\begin{figure}[h]
- \begin{lstlisting}
-int g;
+These functions have to be used for each assignment, to update the
+initialization status of a block descriptor. $initialize(ptr, size)$
+marks the $size$ bytes starting from $ptr$ as initialized.
+$fullInit(ptr)$ marks all the bytes of $ptr$ as initialized at once.
+It is designed to avoid multiple calls to $initialize$ whenever it is
+possible and improves efficiency of the instrumented program.
-int main() {
- §\highl{\_store\_block(\&g, sizeof(int));}§
- §\highl{\_full\_init(\&g);}§
- ...
- §\highl{\_delete\_block(\&g);}§
- ...
- return 0;
-}
- \end{lstlisting}
- \caption{Global variable instrumentation}
- \label{fig:globals}
-\end{figure}
+%\begin{lstlisting}[caption=Initialization functions]
+%void _initialize(void * ptr, size_t size);
+%void _full_init(void * ptr);
+%\end{lstlisting}
-\begin{figure}[h]
- \begin{lstlisting}
-void f (int i) {
- §\highl{\_store\_block(\&i);}§
- §\highl{\_full\_init(\&i);}§
- ...
- §\highl{\_delete\_block(\&i);}§
-}
- \end{lstlisting}
- \caption{Formal parameter instrumentation}
- \label{fig:formals}
-\end{figure}
+\subsection{Interrogation}
-\begin{figure}[h]
- \begin{lstlisting}
-int i;
-i = 4;
-§\highl{\_full\_init(\&i);}§
-
-int t [10];
-t[2] = 4;
-§\highl{\_initialize((t+2), sizeof(int));}§
- \end{lstlisting}
- \caption{Assignment instrumentation}
- \label{fig:init}
-\end{figure}
+These functions are used to retrieve information about the block descriptors
+and match the \textsc{E-Acsl} annotations we are trying to support:
+${\tt \backslash valid}$, ${\tt \backslash valid\_read}$,
+${\tt \backslash base\_addr}$, ${\tt \backslash block\_length}$,
+${\tt \backslash offset}$ and ${\tt \backslash initialized}$.
+
+%\begin{lstlisting}[caption=Interrogation functions]
+%int _valid(void * ptr, size_t size);
+%void * _base_addr(void * ptr);
+%size_t _block_length(void * ptr);
+%int _offset(void * ptr, size_t size);
+%int _initialized(void * ptr, size_t size);
+%\end{lstlisting}
+
+$valid(ptr, size)$ returns 1 if it is safe to read/write $size$ bytes starting
+from $ptr$, 0 otherwise. $baseAddr(ptr)$ returns the base address of the block
+containing $ptr$ if such a block exists, NULL otherwise. $blockLength(ptr)$
+returns the size (in bytes) of the block containing $ptr$ if such a block
+exists, 0 otherwise. $offset(ptr)$ returns the offset between $ptr$ and the base
+address of the block containing $ptr$ if such a block exists, -1 otherwise.
+$initialized(ptr, size)$ returns 1 if the $size$ first bytes starting from
+$ptr$ are initialized, 0 otherwise.
+
+
+%\section{Instrumentation}
+%\label{section:instru}
+
+%This section presents the instrumentation performed by the \textsc{E-Acsl}
+%plug-in to monitor the memory used by a program. The generated instrumented code
+%uses the previously defined functions (see previous section).
+
+%For each global variable, calls to ${\tt \_store\_block}$ and
+%${\tt \_full\_init}$ are inserted at the beginning of the $main$ function, and a
+%call to ${\tt \_delete\_block}$ at the end (see Figure~\ref{fig:globals}). For
+%each formal parameter and local variable, a call to ${\tt \_store\_block}$ is
+%inserted at the beginning of their scope block and a call to
+%${\tt \_delete\_block}$ at the end of their scope block (see
+%Figure~\ref{fig:formals} and Figure~\ref{fig:locals}). Calls to
+%${\tt \_full\_init}$ and ${\tt \_initialize}$ are inserted on assignments (see
+%Figure~\ref{fig:init}), and \textsc{E-Acsl} annotations are translated to the
+%corresponding functions which result is tested by an assertion (see
+%Figure~\ref{fig:annot}).
+
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+%int * p;
+%p = §\highl{\_malloc}§(32);
+%§\highl{\_free}§(p);
+% \end{lstlisting}
+% \caption{Dynamic allocation instrumentation}
+% \label{fig:alloc-dyn}
+%\end{figure}
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+%{
+% int* p;
+% §\highl{\_store\_block(\&p, sizeof(int*));}§
+% ...
+% §\highl{\_delete\_block(\&p);}§
+%}
+% \end{lstlisting}
+% \caption{Local variable instrumentation}
+% \label{fig:locals}
+%\end{figure}
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+%int g;
+
+%int main() {
+% §\highl{\_store\_block(\&g, sizeof(int));}§
+% §\highl{\_full\_init(\&g);}§
+% ...
+% §\highl{\_delete\_block(\&g);}§
+% ...
+% return 0;
+%}
+% \end{lstlisting}
+% \caption{Global variable instrumentation}
+% \label{fig:globals}
+%\end{figure}
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+%void f (int i) {
+% §\highl{\_store\_block(\&i);}§
+% §\highl{\_full\_init(\&i);}§
+% ...
+% §\highl{\_delete\_block(\&i);}§
+%}
+% \end{lstlisting}
+% \caption{Formal parameter instrumentation}
+% \label{fig:formals}
+%\end{figure}
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+%int i;
+%i = 4;
+%§\highl{\_full\_init(\&i);}§
+
+%int t [10];
+%t[2] = 4;
+%§\highl{\_initialize((t+2), sizeof(int));}§
+% \end{lstlisting}
+% \caption{Assignment instrumentation}
+% \label{fig:init}
+%\end{figure}
+
+
+%\begin{figure}[h]
+% \begin{lstlisting}
+%int p[12];
+%//@ assert \valid (p+2);
+%§\highl{assert(\_valid((p+2), sizeof(int)));}§
+% \end{lstlisting}
+% \caption{Annotation instrumentation}
+% \label{fig:annot}
+%\end{figure}
+
+
+\section{Experimental results}
\begin{figure}[h]
- \begin{lstlisting}
-int p[12];
-//@ assert \valid (p+2);
-§\highl{assert(\_valid((p+2), sizeof(int)));}§
- \end{lstlisting}
- \caption{Annotation instrumentation}
- \label{fig:annot}
-\end{figure}
+ \centering
+ \begin{tabular}{|c|c|c|c|c|c|c|}
+ \hline
+ & alarms & $\tau_{exec}$ & mutants & mutation & test cases
+ & assert violations \\
+ \hline
+ $p_1$ & 19 & 63s & 6 & pointer arith. & 57 & 156/186 (83.8 \%) \\
+ \hline
+ $p_2$ & 8 & 28s & 2 & pointer arith. & 27 & 52/54 (96.3 \%) \\
+ \hline
+ \end{tabular}
+ \caption{Experimental results}
+\end{figure}~\\
\section{Conclusion}
-We implemented an efficient data structure (bittree) (see
-Section~\ref{section:bittree}) to store the block descriptors and functions (see
-Section~\ref{section:lib}) relying on this structure to perform memory
+We implemented an efficient data structure (bittree) to store the block
+descriptors and functions relying on this structure to perform memory
monitoring.
We also defined and implemented into the \textsc{E-Acsl} plug-in the
-instrumentation (see Section~\ref{section:instru}) to perform on a C source code
-to monitor the memory. This allows the runtime checking of the following
-\textsc{E-Acsl} annotations: ${\tt \backslash base\_addr}$,
-${\tt \backslash block\_length}$, ${\tt \backslash offset}$,
-${\tt \backslash valid}$ and ${\tt \backslash initialized}$.
+instrumentation to perform on a C source code to monitor the memory. This allows
+the runtime checking of the following \textsc{E-Acsl} annotations:
+${\tt \backslash base\_addr}$, ${\tt \backslash block\_length}$,
+${\tt \backslash offset}$, ${\tt \backslash valid}$,
+${\tt \backslash valid\_read}$ and ${\tt \backslash initialized}$.
\begin{scriptsize}