diff --git a/src/plugins/e-acsl/doc/memory_model/Makefile b/src/plugins/e-acsl/doc/memory_model/Makefile
deleted file mode 100644
index 82d6409e3a29ddbb9fa39e67c07bcd88a84829ae..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/Makefile
+++ /dev/null
@@ -1,19 +0,0 @@
-
-BIB=biblio.bib
-
-all: article
-
-article: article.pdf
-
-article.dvi: article.tex $(BIB)
- latex $^
- bibtex article
- latex $^
- latex $^
-
-article.pdf: article.dvi
- dvipdf article.dvi
-
-clean:
- rm *.toc *.aux *.pdf *.log *.bbl *.blg *.dvi *.nav *.out *.snm
-
diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf
deleted file mode 100644
index 9442066c1b36e315776d69c92986282a8635b8e5..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/doc/memory_model/article.pdf and /dev/null differ
diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex
deleted file mode 100644
index 4c206402d7ad9784da3010402606dcb78d6f8cf4..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/article.tex
+++ /dev/null
@@ -1,763 +0,0 @@
-
-\documentclass[a4paper,11pt]{article}
-
-\usepackage[utf8]{inputenc}
-\usepackage[T1]{fontenc}
-\usepackage[dvips]{graphicx}
-%\usepackage{framed}
-\usepackage{latexsym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{listings}
-\usepackage{courier}
-\usepackage{caption}
-\usepackage[normalem]{ulem}
-\usepackage{pgfplots}
-\usepackage{booktabs,colortbl}
-\usepackage{hyperref}
-\usepackage{url}
-\usepackage{etex}
-\usepackage{pstricks-add}
-\usepackage{paralist}
-\usepackage[nounderscore]{syntax}
-\usepackage{tikz}
-\usetikzlibrary{matrix,shapes,shapes.multipart,backgrounds,calc,fit}
-
-%\definecolor{shadecolor}{gray}{0.9}
-
-\setlength{\fboxsep}{1.5pt}
-\newcommand{\highl}{\colorbox{gray!30}}
-
-\lstloadlanguages{C}
-
-\def\lstsmallmath{\leavevmode\ifmmode \scriptstyle \else \fi}
-\def\lstsmallmathend{\leavevmode\ifmmode \else \fi}
-\lstset {
- escapechar=§,
- %frame=shadowbox,
- %rulesepcolor=\color{black},
- showspaces=false,showtabs=false,tabsize=2,
- numberstyle=\tiny,numbers=left,
- stringstyle=\color{sh_string},
- keywordstyle = \color{sh_keyword}\bfseries,
- commentstyle=\color{sh_comment}\itshape,
- captionpos=b,
- xleftmargin=0.7cm,
- aboveskip=0.7cm,
- belowskip=0.5cm,
- escapebegin={\lstsmallmath}, escapeend={\lstsmallmathend},
- emph={int,char,void,return,size\_t,unsigned,long,struct,if,,else,for,while,
- break,const,short},
- emphstyle=\textbf
-}
-
-\tikzstyle{leaf}=[rounded corners,rectangle,inner sep=1mm,fill=gray!40]
-
-
-\captionsetup[lstlisting]{
- singlelinecheck=false,
- margin=40pt,
- font={bf,footnotesize}
-}
-
-
-
-\begin{document}
-
-\title{Code generation for memory monitoring}
-\author{Nikolaï Kosmatov \and Guillaume Petiot \and Julien Signoles}
-\date{\today}
-
-\maketitle
-
-
-
-\begin{abstract}
-We present:\\
-* framework for memory monitoring\\
-* instrumentation of {C} programs\\
-* ...
-\end{abstract}
-
-
-\section{Introduction}
-
-
-Memory accesses from a pointer or an array are not safe in C, thus trying to
-access an element of an array out of valid range or an invalid pointer may cause
-a segmentation fault during execution.
-
-C compilers such as \textsc{Gcc} do not provide detection mechanisms for this
-kind of errors. We propose an automatic code instrumentation, so that the
-generated code will perform memory monitoring and will be able to check
-memory properties during execution (runtime checking).
-We consider as readable and writable memory: global variables, dynamically
-allocated memory, and formal parameters and local variables of each function. We
-decided to use the term ``block'' to nominate these four cases.
-
-\textsc{E-Acsl} is an executable subset of \textsc{Acsl} \cite{ACSL}, a formal
-specification language for C using source code annotations to express
-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}
-
-* ask Pascal ? *
-
-\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[${\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[${\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.
-
-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 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}
-
-\newcommand{\colB}{0}
-\newcommand{\rowA}{7}
-\newcommand{\rowB}{5}
-\newcommand{\rowC}{3}
-\newcommand{\rowD}{1}
-\begin{figure}[h]
- \begin{center}
- \tikzstyle{service}=[rounded corners,rectangle,inner sep=1mm,fill=gray!40]
- \scalebox{0.85}{
- \begin{tikzpicture}
- \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[inner sep=4mm,draw](bt) at (-2,\rowD{}){{\em Patricia trie}};
- \node[inner sep=4mm,draw](ll) at (2,\rowD{}){Linked list};
-
- \node[service] (eacsl2) 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 (bt);
- \path [->,loosely dashed,thick] (sdda) edge (ll);
- \path [<->] (eacsl) edge (eacsl2);
- \path [<->] (lib) edge (mf);
- \path [<->] (sdda) edge (ci);
- \end{tikzpicture}
- }
- \end{center}
- \caption{Global architecture}
- \label{fig:lib}
-\end{figure}
-
-
-Interactions between the components of our solution are displayed by
-Figure~\ref{fig:lib}. Informations about block descriptors are stored in an
-arbitrary data structure $S$ (see Section~\ref{section:patricia-trie}). 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 Patricia trie}}
-\label{section:patricia-trie}
-
-In this section we discuss the choice of the concrete data structure used to
-store the block descriptors.
-
-We need a data structure with a good time and space complexity, indeed we may
-have to often add or remove a block descriptor in the structure. The structure
-has to be sorted: we want to access to a block descriptor by its base address,
-and also to its predecessor and successor. Thus, hash-tables will not fit.
-We also unconsidered the linked lists, due to the linear worst-case complexity.
-The (unbalanced) binary search trees provide a linear worst-case complexity too
-when the base address of inserted elements are monotonically increasing, and
-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,sibling distance=1.4em,level distance=3cm]
- \node {0010 ****}
- child { node[leaf] {0010 0111} }
- child { node {0010 1***}
- child { node[leaf] {0010 1001} }
- child { node[leaf] {0010 1101} }
- };
- \caption{Example of Patricia trie}
- \label{fig:bittree}
- \end{center}
-\end{figure}
-
-We choose to use the {\em Patricia trie} \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.
-The block descriptors are held on leaves. Other nodes just do the routing from
-the root to a block descriptor.
-
-%Patricia tries are usually used on strings and characters, so we named
-%``bittree'' the structure used in this article.
-
-For example on 8-bit addresses, Figure~\ref{fig:bittree} shows
-a Patricia trie storing three block descriptors (identified by their addresses:
-${\tt 0010\,0111}$, ${\tt 0010\,1001}$ and ${\tt 0010\,1101})$. The greatest
-common prefix of ${\tt 0010\,1001}$ and ${\tt 0010\,1101}$ is ${\tt 0010\,1***}$
-and the greatest common prefix of ${\tt 0010\,0111}$ and ${\tt 0010\,1***}$ is
-${\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.
-
-\begin{figure}[h]
- \begin{center}
- \tikz[grow=right,level 2/.style={sibling distance=1.4em},level distance=3cm]
- \node {0010 ****}
- child { node {0010 011*}
- child { node[leaf] {0010 0110} }
- child { node[leaf] {0010 0111} }
- }
- child { node {0010 1***}
- child { node[leaf] {0010 1001} }
- child { node[leaf] {0010 1101} }
- };
- \caption{Patricia trie after adding ${\tt 0010\,0110}$ into the trie of
- Fig.~\ref{fig:bittree}}
- \label{fig:insertion}
- \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) trie has a worst-case depth of 33 (respectively 65) nodes.
-
-\begin{figure}[h]
- \begin{center}
- \tikz[grow=right,sibling distance=1.4em,level distance=3cm]
- \node {0010 ****}
- child { node[leaf] {0010 0111} }
- child { node[leaf] {0010 1001} };
- \caption{Patricia trie after deleting ${\tt 0010\,1101}$ from the trie of
- Fig.~\ref{fig:bittree}}
- \label{fig:deletion}
- \end{center}
-\end{figure}
-
-
-\subsection{Greatest common prefix computation}
-\label{section:gcpc}
-
-The greatest common prefix of $A$ and $B$ can be naively computed by:
-$X = \lnot (A \oplus B)$ (where $\oplus$ is the XOR operator) to keep bits in
-common, then each bit of $X$ on the right side of a 0 is set to 0. The obtained
-mask is then applied to $A$ or $B$. For example, considering
-$A = {\tt 0110\,0111}$ and $B = {\tt 0111\,1111}$,
-$X = \lnot (A \oplus B) = {\tt 1110\,0111}$, setting each bit on the right side
-of a 0 to 0 we get ${\tt 1110\,0000}$. We apply this mask to $A$ and get the
-greatest common prefix of $A$ and $B$: ${\tt 011*\,****}$.
-
-%This algorithm is
-%used by the first version of out implementation and is named {\em Bittree-naive}
-%in the experiments.
-
-We optimized this algorithm by firstly computing all of the 65 or 33 different
-masks (from {\tt 0x0} to {\tt0xf$\dots$f}) and storing them in an array. Then we
-use a dichotomic search to find the mask corresponding to the greatest common
-prefix: if $A$ and $B$ have a 32-bit common prefix, do they have a 48-bit common
-prefix ? Otherwise, do they have a 16-bit common prefix ? And so on. This search
-takes at most 6 (respectively 5) steps on 64-bit (respectively 32-bit) tries.
-
-%This algorithm is used by the final version of our implementation and is named
-%{\em Bittree-opti} in the experiments.
-
-
-%\subsection{Experiments}
-
-%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 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$
-%(adding an element to the data structure). Figure~\ref{fig:experiments}
-%displays the results of the experiments.
-%The reference time is the execution time of the program without any
-%instrumentation. Bittree-naive and Bittree-opti are using two different versions
-%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)},
-% legend entries={List, Tree, Bittree-naive, Bittree-opti, Reference time}
-% ]
-% \addplot table {timeList.dat};
-% \addplot table {timeTree.dat};
-% \addplot table {timeBTn.dat};
-% \addplot table {timeBTo.dat};
-% \addplot table {timeNone.dat};
-% \end{axis}
-% \end{tikzpicture}
-% \caption{Execution time plotted against the number of calls to $store$}
-% \label{fig:experiments}
-%\end{center}
-%\end{figure}
-
-
-
-%The last but one measurement, the merge sort applied to 50,000 elements
-%(4,889,819 calls to $store$), has a reference time of 0.07s. It runs 32s with
-%the optimized bittree, 118s with the naive bittree, 7 hours 15 minutes with the
-%binary search trees and 19 hours 15 minutes with linked lists.
-%Our last measurement, the merge sort applied to 100,000 elements
-%(10,279,851 calls to $store$) has a reference time of 0.19s. It runs 72s with
-%the optimized bittree, 252s with the naive bittree, but binary search trees and
-%linked lists exceed our 24-hour timeout.
-
-
-
-\section{Monitoring functions}
-\label{section:lib}
-
-
-This section presents the functions used for adding/removing/retrieving in
-formations about block descriptors into our data structure (Patricia trie).
-These functions will be automatically inserted in the source code by the
-instrumentation performed by the \textsc{E-Acsl} plug-in.
-
-
-\subsection{Automatic allocation}
-
-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{figure}[h]
- \begin{center}
- \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)--(2,.5)--(3,-1)--cycle;
- \node at (2,-0.5) {{\em trie}};
- \node at (0,0.3) {$add(v)$};
- \draw[->] (-.4,0) -- (.6, 0);
- \node at (0,-.7) {$remove(v)$};
- \draw[->] (-.4,-1) -- (.6, -1);
- \end{tikzpicture}
- \end{center}
- \caption{$storeBlock$ and $deleteBlock$}
-\end{figure}
-
-
-
-%\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 $malloc$, $realloc$, $calloc$ and
-$free$ from the standard library.
-
-
-
-\begin{figure}[h]
- \begin{center}
- \begin{tikzpicture}
- \node at (-3,0) {
-\begin{lstlisting}
- T* v;
- v = §\highl{$malloc (sizeof (N));$}§
- ...
- §\highl{$free (v);$}§
-\end{lstlisting}};
-
- \path[draw, fill=gray!20] (3,-1)--(4,.5)--(5,-1)--cycle;
- \node at (4,-0.5) {{\em trie}};
- \node at (1.9,0.3) {$add(v)$};
- \draw[->] (1.5,0) -- (2.5, 0);
- \node at (1.9,-.7) {$remove(v)$};
- \draw[->] (1.5,-1) -- (2.5, -1);
- \end{tikzpicture}
- \end{center}
- \caption{$malloc$ and $free$}
-\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}
-
-
-\subsection{Initialization}
-
-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.
-
-
-\begin{figure}[h]
- \begin{center}
- \begin{tikzpicture}
- \node at (-3,0) {
-\begin{lstlisting}
- v = (T)x;
- §\highl{$initialize (v, sizeof (T));$}§
-\end{lstlisting}};
-
- \path[draw, fill=gray!20] (2.5,-1)--(3.5,.5)--(4.5,-1)--cycle;
- \node at (3.5,-0.5) {{\em trie}};
- \node at (1.4,0) {$find(v)$};
- \draw[->] (1,-0.3) -- (2,-0.3);
- \draw[->] (4.5,0) .. controls(4.7,-.2) .. (4.5,-.4);
- \node at (5.8,-.2) {$update(v)$};
- \end{tikzpicture}
- \end{center}
- \caption{$initialize$}
-\end{figure}
-
-
-%\begin{lstlisting}[caption=Initialization functions]
-%void _initialize(void * ptr, size_t size);
-%void _full_init(void * ptr);
-%\end{lstlisting}
-
-
-\subsection{Interrogation}
-
-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.
-
-
-\begin{figure}[h]
- \begin{center}
- \begin{tikzpicture}
- \node at (-3,0) {
-\begin{lstlisting}
- //@ assert §${\tt \backslash valid(p+i)}$§;
- §\highl{$assert (valid (p+i));$}§
-\end{lstlisting}};
-
- \path[draw, fill=gray!20] (3,-1)--(4,.5)--(5,-1)--cycle;
- \node at (4,-0.5) {{\em trie}};
- \node at (1.9,0) {$find(v)$};
- \draw[<->] (1.5,-0.3) -- (2.5,-0.3);
- \end{tikzpicture}
- \end{center}
- \caption{$valid$ assertion checking}
-\end{figure}
-
-
-%\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}
-
-We used mutational testing to stress our library. The program under test is
-previously annotated (its specification is expressed in \textsc{Acsl}
-\cite{ACSL}. The program under test is supposed correct, we want to show that
-\textsc{E-Acsl} is able to spot the specification violations of
- ``mutated programs'' (that do not match the specification anymore).\\
-
-We used a test generator granting path coverage \cite{PathCrawler}
-to generate test cases. We then use \textsc{E-Acsl} to instrument the program
-under test and the test cases, to generate calls to our monitoring framework.
-We the check that the instrumented original program (supposed correct)
-successfully pass each of those tests. We then generate mutated programs,
-obtained by modifying an element in the syntactic tree. The mutations used for
-these experiments are: numerical-arithmetic operator modification,
-pointer-arithmetic operator modification, comparison operator modification
-and logic ($land$ and $lor$) operator modification. Then each mutant program is
-instrumented by \textsc{E-Acsl}.\\
-
-Finally, each pair ($test case$, $mutant$) is executed. The results are
-displayed in Fig.~\ref{fig:exp}. We consider a mutant ``killed'' if there is at
-least one test case provoking a runtime error and this error has been found by
-\textsc{E-Acsl}.
-
-\begin{figure}[h]
- \centering
- \begin{tabular}{|c|c|c|c|c|c|c|}
- \hline
- & alarms & time & test cases & mutants & mutants killed \\
- \hline
- $fibonacci$ & 31 & 54s & 38 & 20 & 20 \\
- \hline
- $Bsearch$ & 28 & 63s & 20 & 41 & 41 \\
- \hline
- $Bsort$ & 37 & 273s & 153 & 47 & 45 \\
- \hline
- $Merge$ & 55 & 100s & 19 & 58 & 58 \\
- \hline
- $BubbleSort$ & 31 & 963s & 873 & 44 & 44 \\
- \hline
- $MultiplyMatrix$ & 44 & 146s & 9 & 44 & 44 \\
- \hline
- $get\_sub$ & 165 & 993s & 364 & 53 & 50 \\
- \hline
- \end{tabular}
- \caption{Experimental results}
- \label{fig:exp}
-\end{figure}~\\
-
-
-\section{Conclusion}
-
-
-We implemented an efficient data structure 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 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}
-\bibliographystyle{abbrv}
-\bibliography{biblio}
-\end{scriptsize}
-
-
-
-
-
-\end{document}
-
diff --git a/src/plugins/e-acsl/doc/memory_model/biblio.bib b/src/plugins/e-acsl/doc/memory_model/biblio.bib
deleted file mode 100644
index 00ae5c84e55f3b6b20ecde270847c92c70502fea..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/biblio.bib
+++ /dev/null
@@ -1,52 +0,0 @@
-
-
-@inproceedings{Frama-C,
- author = {Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
- title = {{Frama-C}: A Program Analysis Perspective},
- booktitle = {Proc. of the 10th International Conference on Software Engineering and Formal Methods},
- series = {SEFM '2012},
- month = {October},
- year = {2012},
- location = {Thessaloniki, Greece},
- note = {To appear}
-}
-
-@MISC{ACSL,
- author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean C. and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and Prevosto, Virgile},
- edition = {preliminary},
- keywords = {acsl, frama-c},
- title = {{ACSL}: {ANSI/ISO C Specification Language} preliminary design version 1.5},
- howpublished = "\url{http://frama-c.com/acsl.html}",
- year = {2010}
-}
-
-@article{Patricia-tries,
- author = {Szpankowski, Wojciech},
- title = {Patricia tries again revisited},
- journal = {J. ACM},
- issue_date = {Oct. 1990},
- volume = {37},
- number = {4},
- month = oct,
- year = {1990},
- issn = {0004-5411},
- pages = {691--711},
- numpages = {21},
- url = {http://doi.acm.org/10.1145/96559.214080},
- doi = {10.1145/96559.214080},
- acmid = {214080},
- publisher = {ACM},
- address = {New York, NY, USA},
-}
-
-@inproceedings{PathCrawler,
- author = {Bernard Botella and Micka{\"e}l Delahaye and St{\'e}phane {Hong Tuan Ha} and Nikolai Kosmatov and
- Patricia Mouy and Muriel Roger and Nicky Williams},
- title = {Automating Structural Testing of {C} Programs: Experience with {PathCrawler}},
- booktitle = {AST},
- year = {2009},
- pages = {70-78},
- ee = {http://dx.doi.org/10.1109/IWAST.2009.5069043},
- bibsource = {DBLP, http://dblp.uni-trier.de},
-}
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
deleted file mode 100644
index 12938539bbf92154edb6eed3ca4d068fc46b66b5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
+++ /dev/null
@@ -1,65 +0,0 @@
-/* run.config
- COMMENT: BsearchPrecond
- OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -main Bsearch
-*/
-/* Binary search of a given element in a given ordered array
- returning 1 if the element is present and 0 if not.
- This example is like Bsearch
- but gives an example of
- a precondition coded in C */
-
-/*@ ensures (\exists int i; 0 <= i < 10 && A[i] == elem) <==> \result;
- @*/
-int Bsearch( int A[10], int elem)
-{
- int low, high, mid, found ;
-
- low = 0 ;
- high = 9 ;
- found = 0 ;
- while( ( high > low ) )
- {
- //@ assert high > low;
- mid = (low + high) / 2 ;
- //@ assert mid == (low+high) / 2;
- if( elem == A[mid] ) {
- //@ assert elem == A[mid];
- found = 1;
- //@ assert found == 1;
- }
- if( elem > A[mid] ) {
- //@ assert elem > A[mid];
- low = mid + 1 ;
- //@ assert low == mid + 1;
- }
- else {
- //@ assert elem <= A[mid];
- high = mid - 1;
- //@ assert high == mid - 1;
- }
- }
- //@ assert high <= low;
- mid = (low + high) / 2 ;
- //@ assert mid == (low+high) / 2;
-
- if( ( found != 1) && ( elem == A[mid]) ) {
- //@ assert found != 1 && elem == A[mid];
- found = 1;
- //@ assert found == 1;
- }
-
- return found ;
-}
-
-/* C precondition of function Bsearch
- This must have the name of the tested function suffixed with _precond
- and have the same number of arguments with the same types.
- It must return 1 if the parameter values satisfy the precondition and 0 if not */
-int Bsearch_precond( int A[10], int elem) {
- int i;
- for (i = 0; i < 9; i++){
- if (A[i]>A[i+1])
- return 0 ; /* not ordered by increasing value */
- }
- return 1;
-}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
deleted file mode 100644
index a06b2298d3a8a919db611057f2fb6a01f883417a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
+++ /dev/null
@@ -1,29 +0,0 @@
-:- module(test_parameters).
-
-:- import create_input_val/3 from substitution.
-
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-dom('Bsearch',cont('A',_),[],int([0..100])).
-dom('pathcrawler__Bsearch_precond',A,B,C):-
- dom('Bsearch',A,B,C).
-
-create_input_vals('Bsearch',Ins):-
- create_input_val('elem',int([0..100]),Ins),
- create_input_val(dim('A'),int([10]),Ins),
- true.
-create_input_vals('Bsearch',Ins):-
- create_input_vals('pathcrawler__Bsearch_precond',Ins).
-
-unquantif_preconds('Bsearch',[]).
-quantif_preconds('Bsearch',[]).
-
-strategy('Bsearch',[]).
-strategy('pathcrawler__Bsearch_precond',[]).
-
-precondition_of('Bsearch','pathcrawler__Bsearch_precond').
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
deleted file mode 100644
index 007fede5caf07e1e225e19bd6a6f63967eb8cc27..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
+++ /dev/null
@@ -1,50 +0,0 @@
-/* run.config
- COMMENT: Bsort
- OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -main bsort
-*/
-/* Bubble sort of a given array 'table' of a given length 'l' in descending order. This example is interesting because of its
- - variable dimension input array
- - loop with a variable number of iterations,
- which is limited by limiting the array dimension
- - oracle which does not sort but checks the result is ordered */
-
-/*@ ensures \forall int k; 0 <= k < l-1 ==> table[k] >= table[k+1];
- @*/
-void bsort (int * table, int l)
-{
- int i, temp, nb;
- char fini;
- fini = 0;
- nb = 0;
- //@ assert l >= 0;
- //@ assert fini == 0;
- //@ assert nb == 0;
- while ( !fini && (nb < l-1)){
- //@ assert fini == 0;
- //@ assert nb < l-1;
- fini = 1;
- //@ assert fini == 1;
- for (i=0 ; i<l-1 ; ) {
- //@ assert 0 <= i < l-1;
- if (table[i] < table[i+1]){
- //@ assert table[i] < table[i+1];
- fini = 0;
- //@ assert fini == 0;
- temp = table[i];
- //@ assert temp == table[i];
- table[i] = table[i + 1];
- //@ assert table[i] == table[i+1];
- table[i + 1] = temp;
- //@ assert table[i+1] == temp;
- }
- //@ ghost int old_i = i;
- i++;
- //@ assert old_i + 1 == i;
- }
- //@ assert i >= l-1;
- //@ ghost int old_nb = nb;
- nb++;
- //@ assert old_nb + 1 == nb;
- }
- //@ assert fini == 1 || nb >= l-1;
-}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
deleted file mode 100644
index ad41d5bb9f4b647beee36eb30390da452acad731..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
+++ /dev/null
@@ -1,24 +0,0 @@
-:- module(test_parameters).
-
-:- import create_input_val/3 from substitution.
-
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-dom('bsort',cont('table',_),[],int([-100..100])).
-
-create_input_vals('bsort',Ins):-
- create_input_val(dim('table'),int([0..5]),Ins),
- create_input_val('l',int([0..5]),Ins),
- true.
-
-unquantif_preconds('bsort',[cond(egal,dim('table'),'l',pre)]).
-quantif_preconds('bsort',[]).
-
-strategy('bsort',[]).
-
-precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
deleted file mode 100644
index 415b567a1d426a3b55603c159c464ccb80d7e450..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
+++ /dev/null
@@ -1,44 +0,0 @@
-
-/*@ ensures \forall int i; 0 <= i < length-1 ==> a[i] <= a[i+1];
- @*/
-void bubble_sort(int* a, int length)
-{
- int auf = 1;
- int ab;
- int fixed_auf = 1;
-
-
- for (; auf < length; )
- {
- //@ assert auf < length;
- fixed_auf = auf;
- ab=auf;
-
- while (0 < ab && a[ab] < a[ab-1])
- {
- //@ assert 0 < ab;
- //@ assert a[ab] < a[ab-1];
- //@ ghost int old_1 = a[ab];
- //@ ghost int old_2 = a[ab-1];
- int temp = a[ab];
- a[ab] = a[ab-1];
- a[ab-1] = temp;
-
- //@ assert old_1 == a[ab-1];
- //@ assert old_2 == a[ab];
-
- //@ ghost int old_ab = ab;
- ab = ab-1;
- //@ assert old_ab - 1 == ab;
- }
- //@ assert 0 >= ab || a[ab] >= a[ab-1];
-
- //@ ghost int old_auf = auf;
- auf++;
- //@ assert old_auf + 1 == auf;
-
- fixed_auf = auf;
- }
- //@ assert auf >= length;
-}
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
deleted file mode 100644
index 0ae92b1c264ca21bff1df37a9c291fdca40e8dff..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
+++ /dev/null
@@ -1,21 +0,0 @@
-:- module(test_parameters).
-:- import create_input_val/3 from substitution.
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-dom('bubble_sort',cont('a',_),[],int([-20..20])).
-
-create_input_vals('bubble_sort',Ins):-
- create_input_val(dim('a'),int([0..6]),Ins),
- create_input_val('length',int([0..6]),Ins),
- true.
-
-unquantif_preconds('bubble_sort',[cond(egal,dim('a'),'length',pre)]).
-
-quantif_preconds('bubble_sort',[]).
-strategy('bubble_sort',[]).
-precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
deleted file mode 100644
index 2787cc569d130ad591e4eb666ed68c4101f307c2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
+++ /dev/null
@@ -1,63 +0,0 @@
-/* run.config
- OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -pc-k-path 2 -main Merge
-*/
-
-
-
-
-/*@ ensures \forall int i; 0 <= i < (l1+l2-1) ==> t3[i] <= t3[i+1];
- @*/
-void Merge (int t1[], int t2[], int t3[], int l1, int l2) {
- int i = 0;
- int j = 0;
- int k = 0;
-
- while (i < l1 && j < l2) {
- //@ assert i < l1;
- //@ assert j < l2;
- if (t1[i] < t2[j]) {
- //@ assert t1[i] < t2[j];
- t3[k] = t1[i];
- //@ assert t3[k] == t1[i];
- //@ ghost int tmp = i;
- i++;
- //@ assert tmp + 1 == i;
- }
- else {
- //@ assert t1[i] >= t2[j];
- t3[k] = t2[j];
- //@ assert t3[k] == t2[j];
- //@ ghost int tmp = j;
- j++;
- //@ assert tmp + 1 == j;
- }
- //@ ghost int tmp = k;
- k++;
- //@ assert tmp + 1 == k;
- }
- //@ assert i >= l1 || j >= l2;
- while (i < l1) {
- //@ assert i < l1;
- t3[k] = t1[i];
- //@ assert t3[k] == t1[i];
- //@ ghost int tmp1 = i;
- //@ ghost int tmp2 = k;
- i++;
- //@ assert tmp1 + 1 == i;
- k++;
- //@ assert tmp2 + 1 == k;
- }
- //@ assert i >= l1;
- while (j < l2) {
- //@ assert j < l2;
- t3[k] = t2[j];
- //@ assert t3[k] == t2[j];
- //@ ghost int tmp1 = j;
- //@ ghost int tmp2 = k;
- j++;
- //@ assert tmp1 + 1 == j;
- k++;
- //@ assert tmp2 + 1 == k;
- }
- //@ assert j >= l2;
-}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
deleted file mode 100644
index 44c0551ba13f14061162865add7be382c3340a8e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
+++ /dev/null
@@ -1,77 +0,0 @@
-:- module(test_parameters).
-
-:- import create_input_val/3 from substitution.
-
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-dom('Merge',cont('t1',_),[],int([-10..10])).
-dom('Merge',cont('t2',_),[],int([-10..10])).
-
-create_input_vals('Merge',Ins):-
- create_input_val(dim('t1'),int([0..10]),Ins),
- create_input_val(dim('t2'),int([0..10]),Ins),
- create_input_val(dim('t3'),int([0..20]),Ins),
- create_input_val('l1',int([0..10]),Ins),
- create_input_val('l2',int([0..10]),Ins),
- true.
-
-unquantif_preconds('Merge',
- [cond(supegal,dim('t1'),'l1',pre),
- cond(supegal,dim('t2'),'l2',pre),
- cond(supegal,dim('t3'),+(int(math),'l1','l2'),pre)]).
-quantif_preconds('Merge',[uq_cond([UQV3],
- [cond(supegal,UQV3,1,pre)],
- supegal,
- cont('t1',UQV3),
- cont('t1',-(int(math),UQV3,1))),
- uq_cond([UQV4],
- [cond(supegal,UQV4,1,pre)],
- supegal,
- cont('t2',UQV4),
- cont('t2',-(int(math),UQV4,1)))]).
-
-strategy('Merge',[kpath(2)]).
-
-precondition_of(0,0).
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
deleted file mode 100644
index f730673e890de80424c609cbbcababf061e60e0f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
+++ /dev/null
@@ -1,41 +0,0 @@
-
-#include "stdlib.h"
-
-/*@ requires n >= 3;
- @ requires \valid(t+(0..n-1));
- @ ensures t[0] == 1;
- @ ensures t[1] == 1;
- @ ensures \forall int i; 2 <= i < n ==> t[i-2] + t[i-1] == t[i];
- @*/
-void fibo(int *t, int n) {
- int i;
- t[0] = t[1] = 1;
-
- /*@ loop invariant \forall int k; 2 <= k < i ==> t[k] == t[k-1] + t[k-2];
- @ loop assigns i, *(t+(2..n-1));
- @ loop variant n-i;
- @*/
- for(i = 2; i < n; ) {
- //@ assert 2 <= i < n;
- t[i] = t[i-1] + t[i-2];
- //@ assert t[i] == t[i-1] + t[i-2];
- //@ ghost int old_i = i;
- i++;
- //@ assert old_i + 1 == i;
- }
- //@ assert i >= n;
-}
-
-
-/*@ ensures \result >= x;
- @ assigns \nothing;
- @*/
-int unbounded_random(int x);
-
-void driver() {
- int n = unbounded_random(3);
- int * t = malloc(n * sizeof(int));
- fibo(t, n);
- free(t);
-}
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
deleted file mode 100644
index 04fefca54bd2d9315f7ddef244f53d76ca8ebfb2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
+++ /dev/null
@@ -1,19 +0,0 @@
-:- module(test_parameters).
-:- import create_input_val/3 from substitution.
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-dom('fibo', cont('t',_), [], int([-10..10])).
-create_input_vals('fibo', Ins):-
- create_input_val('n', int([3..40]),Ins),
- create_input_val(dim('t'), int([3..40]),Ins),
- true.
-
-quantif_preconds('fibo',[]).
-unquantif_preconds('fibo',[cond(egal,dim('t'),'n',pre)]).
-strategy('fibo',[]).
-precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
deleted file mode 100644
index df8c2cc629b02a3baa08750f0669c1f0f1bc3638..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
+++ /dev/null
@@ -1,255 +0,0 @@
-/* -*- Last-Edit: Mon Dec 7 10:31:51 1992 by Tarak S. Goradia; -*- */
-
-
-
-#include "stdio.h"
-#include "stdlib.h"
-
-/*
-#include <ctype.h>
-
-typedef char bool;
-# define false 0
-# define true 1
-# define NULL 0
-
-# define MAXSTR 100
-# define MAXPAT MAXSTR
-
-# define ENDSTR '\0'
-# define ESCAPE '@'
-# define CLOSURE '*'
-# define BOL '%'
-# define EOL '$'
-# define ANY '?'
-# define CCL '['
-# define CCLEND ']'
-# define NEGATE '^'
-# define NCCL '!'
-# define LITCHAR 'c'
-# define DITTO -1
-# define DASH '-'
-
-# define TAB 9
-# define NEWLINE 10
-
-# define CLOSIZE 1
-
-typedef char character;
-typedef char string[MAXSTR];
-*/
-
-
-
-/*@ requires \valid_read(j);
- @ behavior b1:
- @ assumes *j >= maxset;
- @ assigns \nothing;
- @ ensures \result == 0;
- @ behavior b2:
- @ assumes *j < maxset;
- @ requires \valid(j);
- @ requires \valid(outset+(*j));
- @ assigns *j, outset[*j];
- @ ensures *j == \old(*j)+1;
- @ ensures outset[*j-1] == c;
- @ ensures \result == 1;
- @ complete behaviors;
- @ disjoint behaviors;
- @*/
-int addstr(char c, char *outset, int *j, int maxset){
- char result;
-
- /* b1 */
- if (*j >= maxset){
- //@ assert *j >= maxset;
- result = 0;
- }
- /* b2 */
- else {
- //@ assert *j < maxset;
- outset[*j] = c;
- //@ ghost int tmp = *j;
- *j = *j + 1;
- //@ assert *j == tmp + 1;
- result = 1;
- }
- return result;
-}
-
-
-/*@ requires \valid_read(i);
- @ requires \valid_read(s+(*i));
- @ behavior b1:
- @ assumes s[*i] != '@';
- @ assigns \nothing;
- @ ensures \result == s[*i];
- @ behavior b2:
- @ assumes s[*i] == '@';
- @ assumes s[*i+1] == '\0';
- @ requires \valid_read(s+(*i+1));
- @ assigns \nothing;
- @ ensures \result == '@';
- @ behavior b3:
- @ assumes s[*i] == '@';
- @ assumes s[*i+1] == 'n';
- @ requires \valid_read(s+(*i+1));
- @ assigns *i;
- @ ensures *i == \old(*i)+1;
- @ ensures \result == 10;
- @ behavior b4:
- @ assumes s[*i] == '@';
- @ assumes s[*i+1] == 't';
- @ requires \valid_read(s+(*i+1));
- @ assigns *i;
- @ ensures *i == \old(*i)+1;
- @ ensures \result == 9;
- @ behavior b5:
- @ assumes s[*i] == '@';
- @ assumes s[*i+1] != '\0';
- @ assumes s[*i+1] != 'n';
- @ assumes s[*i+1] != 't';
- @ requires \valid_read(s+(*i+1));
- @ assigns *i;
- @ ensures *i == \old(*i)+1;
- @ ensures \result == s[*i];
- @ complete behaviors;
- @ disjoint behaviors;
- @*/
-char esc(char *s, int *i){
- char result;
-
- /* b1 */
- if (s[*i] != '@'){
- //@ assert s[*i] != '@';
- result = s[*i];
- }
- else{
- //@ assert s[*i] == '@';
- /* b2 */
- if(s[*i + 1] == '\0'){
- //@ assert s[*i+1] == '\0';
- result = '@';
- }
- else{
- //@ assert s[*i+1] != '\0';
- //@ ghost int tmp = *i;
- *i = *i + 1;
- //@ assert *i == tmp + 1;
- /* b3 */
- if(s[*i] == 'n'){
- //@ assert s[*i] == 'n';
- result = 10;
- }
- else{
- //@ assert s[*i] != 'n';
- /* b4 */
- if(s[*i] == 't'){
- //@ assert s[*i] == 't';
- result = 9;
- }
- /* b5 */
- else{
- //@ assert s[*i] != 't';
- result = s[*i];
- }
- }
- }
- }
- return result;
-}
-
-
-int makesub(char* arg, int from, char delim, char* sub){
- int result;
- int i, j;
- char junk;
- char escjunk;
-
- j = 0;
- i = from;
-
- while ((arg[i] != delim) && (arg[i] != '\0')) {
- //@ assert arg[i] != delim;
- //@ assert arg[i] != '\0';
- if ((arg[i] == (unsigned)('&'))){
- //@ assert arg[i] == '&';
- junk = addstr(-1, sub, &j, 100);
- }
- else {
- //@ assert arg[i] != '&';
- escjunk = esc(arg, &i);
- junk = addstr(escjunk, sub, &j, 100);
- }
-
- //@ ghost int tmp = i;
- i = i + 1;
- //@ assert i == tmp + 1;
- }
- //@ assert arg[i] == delim || arg[i] == '\0';
- /* b1 */
- if (arg[i] != delim){
- //@ assert arg[i] != delim;
- // unreachable
- result = 0;
- }else {
- //@ assert arg[i] == delim;
- junk = addstr('\0', &(*sub), &j, 100);
- /* b2 */
- if (!junk){
- //@ assert !junk;
- result = 0;
- }
- /* b3 */
- else{
- //@ assert junk;
- result = i;
- }
- }
- return result;
-}
-
-
-char getsub(char* arg, char* sub){
- int makeres;
- makeres = makesub(arg, 0, '\0', sub);
- //@ ghost char* tmp_arg = arg;
- //@ ghost char* tmp_sub = sub;
- //@ ghost int verdict = 1;
- /*@ ghost while (*tmp_arg != 0) {
- if(*tmp_arg == '&') {
- if(*tmp_sub != -1){verdict=0;break;}
- tmp_arg++; tmp_sub++;
- }
- else if(*tmp_arg == '@' && *(tmp_arg+1) == '\0') {
- if(*tmp_sub != '@') {verdict=0;break;}
- tmp_arg++; tmp_sub++;
- }
- else if(*tmp_arg == '@' && *(tmp_arg+1) == 'n') {
- if(*tmp_sub != 10) {verdict=0;break;}
- tmp_arg += 2; tmp_sub++;
- }
- else if(*tmp_arg == '@' && *(tmp_arg+1) == 't') {
- if(*tmp_sub != 9) {verdict=0;break;}
- tmp_arg += 2; tmp_sub++;
- }
- else if(*tmp_arg == '@') {
- if(*tmp_sub != *(tmp_arg+1)) {verdict=0;break;}
- tmp_arg += 2; tmp_sub++;
- }
- else {
- if(*tmp_sub != *tmp_arg) {verdict=0;break;}
- tmp_arg++; tmp_sub++;
- }
- } */
-
- //@ assert verdict == 1;
- if(makeres > 0){
- //@ assert makeres > 0;
- return(1);
- }
- else{
- //@ assert makeres <= 0;
- return(0);
- }
-}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
deleted file mode 100644
index 5874b006dad5c90fb1f4b03269df2687d4357694..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
+++ /dev/null
@@ -1,36 +0,0 @@
-
-#include "string.h"
-
-void oracle_getsub(char* Pre_arg, char* arg, char* Pre_sub, char* sub, int r) {
- char* tmp_arg = Pre_arg;
- char* tmp_sub = sub;
- while(*tmp_arg != 0) {
- if(*tmp_arg == '&') {
- if(*tmp_sub != -1) {pathcrawler_verdict_failure();return;}
- tmp_arg++; tmp_sub++;
- }
- else if(*tmp_arg == '@' && *(tmp_arg+1) == '\0') {
- if(*tmp_sub != '@') {pathcrawler_verdict_failure();return;}
- tmp_arg++; tmp_sub++;
- }
- else if(*tmp_arg == '@' && *(tmp_arg+1) == 'n') {
- if(*tmp_sub != 10) {pathcrawler_verdict_failure();return;}
- tmp_arg += 2; tmp_sub++;
- }
- else if(*tmp_arg == '@' && *(tmp_arg+1) == 't') {
- if(*tmp_sub != 9) {pathcrawler_verdict_failure();return;}
- tmp_arg += 2; tmp_sub++;
- }
- else if(*tmp_arg == '@') {
- if(*tmp_sub != *(tmp_arg+1)) {pathcrawler_verdict_failure();return;}
- tmp_arg += 2; tmp_sub++;
- }
- else {
- if(*tmp_sub != *tmp_arg) {pathcrawler_verdict_failure();return;}
- tmp_arg++; tmp_sub++;
- }
- }
-
- pathcrawler_verdict_success();
- return;
-}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
deleted file mode 100644
index a1e94895895e5a07994e9f7754d47b71482aaa01..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
+++ /dev/null
@@ -1,36 +0,0 @@
-:- module(test_parameters).
-
-:- import create_input_val/3 from substitution.
-
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-:- export disable_label_history/1.
-disable_label_history(yes).
-dom('getsub',cont('arg__getsub',_),[],int([-128..127])).
-dom('getsub',cont('sub__getsub',_),[],int([-128..127])).
-% add new array domain e.g.:
-% dom('yourFunName',cont('yourArray',_),[],int([min..max])).
-
-create_input_vals('getsub',Ins):-
- create_input_val(dim('sub__getsub'),int([6..6]),Ins),
- create_input_val(dim('arg__getsub'),int([6..6]),Ins),
- true.
-% add new variable domain e.g.:
-% create_input_val(yourVarName,int([min..max]),Ins),
-
-
-unquantif_preconds('getsub',[cond(egal,cont('sub__getsub',5),0,pre),
- cond(egal,cont('arg__getsub',5),0,pre)]).
-
-quantif_preconds('getsub',[]).
-
-strategy('getsub',[]).
-
-precondition_of(0,0).
-
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c
deleted file mode 100644
index d16390507800e6ee699e2e9dfd3239028d20937b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/matmult.c
+++ /dev/null
@@ -1,57 +0,0 @@
-/* MDH WCET BENCHMARK SUITE. File version $Id: matmult.c,v 1.3 2005/11/11 10:31:26 ael01 Exp $ */
-
-/*----------------------------------------------------------------------*
- * To make this program compile under our assumed embedded environment,
- * we had to make several changes:
- * - Declare all functions in ANSI style, not K&R.
- * this includes adding return types in all cases!
- * - Declare function prototypes
- * - Disable all output
- * - Disable all UNIX-style includes
- *
- * This is a program that was developed from mm.c to matmult.c by
- * Thomas Lundqvist at Chalmers.
- *----------------------------------------------------------------------*/
-
-/*@ requires \valid(A+(0..n-1));
- @ requires \valid(B+(0..n-1));
- @ requires \valid(Res+(0..n-1));
- @ requires \forall int i; 0 <= i < n ==> \valid(A[i]+(0..n-1));
- @ requires \forall int i; 0 <= i < n ==> \valid(B[i]+(0..n-1));
- @ requires \forall int i; 0 <= i < n ==> \valid(Res[i]+(0..n-1));
- @*/
-void
-Multiply(int ** A, int ** B, int ** Res, int n)
-/*
- * Multiplies arrays A and B and stores the result in ResultArray.
- */
-{
- register int Outer, Inner, Index;
-
- //@ ghost int old_Outer = -1;
- for (Outer = 0; Outer < n; Outer++) {
- //@ assert old_Outer != Outer;
- //@ ghost old_Outer = Outer;
- //@ assert 0 <= Outer < n;
- //@ ghost int old_Inner = -1;
- for (Inner = 0; Inner < n; Inner++) {
- //@ assert old_Inner != Inner;
- //@ ghost old_Inner = Inner;
- //@ assert 0 <= Inner < n;
- Res[Outer][Inner] = 0;
- //@ assert Res[Outer][Inner] == 0;
- //@ ghost int old_Index = -1;
- for (Index = 0; Index < n; Index++) {
- //@ assert old_Index != Index;
- //@ ghost old_Index = Index;
- //@ assert 0 <= Index < n;
- //@ ghost int res = Res[Outer][Inner];
- Res[Outer][Inner] += A[Outer][Index] * B[Index][Inner];
- //@ assert Res[Outer][Inner] == res + A[Outer][Index] * B[Index][Inner];
- }
- //@ assert Index == n;
- }
- //@ assert Inner == n;
- }
- //@ assert Outer == n;
-}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl b/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl
deleted file mode 100644
index 7964c5440b786f69285107aadc098c4e6989804b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/experiments/matmult/test_parameters.pl
+++ /dev/null
@@ -1,40 +0,0 @@
-:- module(test_parameters).
-
-:- import create_input_val/3 from substitution.
-
-:- export dom/4.
-:- export create_input_vals/2.
-:- export unquantif_preconds/2.
-:- export quantif_preconds/2.
-:- export strategy/2.
-:- export precondition_of/2.
-
-dom('Multiply',dim(cont('A',_)),[],int([0..100])).
-dom('Multiply',dim(cont('B',_)),[],int([0..100])).
-dom('Multiply',dim(cont('Res',_)),[],int([0..100])).
-dom('Multiply',cont(cont('A',_),_),[],int([-100..100])).
-dom('Multiply',cont(cont('B',_),_),[],int([-100..100])).
-dom('Multiply',cont(cont('Res',_),_),[],int([0])).
-
-create_input_vals('Multiply',Ins):-
- create_input_val(dim('A'),int([0..100]),Ins),
- create_input_val(dim('B'),int([0..100]),Ins),
- create_input_val(dim('Res'),int([0..100]),Ins),
- create_input_val('n',int([2..10]),Ins),
- true.
-
-unquantif_preconds('Multiply',[
- cond(egal,'n',dim('A'),pre),
- cond(egal,'n',dim('B'),pre),
- cond(egal,'n',dim('Res'),pre)
-]).
-quantif_preconds('Multiply',[
- uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)],
- egal,'n',dim(cont('A',I))),
- uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)],
- egal,'n',dim(cont('B',I))),
- uq_cond([I],[cond(supegal,I,0,pre),cond(inf,I,'n',pre)],
- egal,'n',dim(cont('Res',I)))
-]).
-strategy('Multiply',[]).
-precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/table_article.dat b/src/plugins/e-acsl/doc/memory_model/table_article.dat
deleted file mode 100644
index 9af5a718760a1491bf3e58280a6421b24e846853..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/table_article.dat
+++ /dev/null
@@ -1,8 +0,0 @@
-store None List Tree Bittree-naive Bittree-opti
-5317 65 20988 7463 78738 24021
-32193 434 847482 251187 566245 151996
-69351 1011 3847986 1127598 1247885 354525
-405877 6475 121097172 34152290 8146124 2293326
-861765 14270 545608598 161718277 17995678 5128649
-4889819 77806 69300000000 26100000000 118501581 32517688
-10279851 193393 -1 -1 252910501 72682398
diff --git a/src/plugins/e-acsl/doc/memory_model/timeBTn.dat b/src/plugins/e-acsl/doc/memory_model/timeBTn.dat
deleted file mode 100644
index bdb496a05d9c6ceab85965e83eed80b51e69b5f6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/timeBTn.dat
+++ /dev/null
@@ -1,8 +0,0 @@
-nbstores time
-5317 78738
-32193 566245
-69351 1247885
-405877 8146124
-861765 17995678
-4889819 118501581
-10279851 252910501
diff --git a/src/plugins/e-acsl/doc/memory_model/timeBTo.dat b/src/plugins/e-acsl/doc/memory_model/timeBTo.dat
deleted file mode 100644
index 3d8291add147ec33d5fa26ab9b50c5fe39a7c6b7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/timeBTo.dat
+++ /dev/null
@@ -1,8 +0,0 @@
-nbstores time
-5317 24021
-32193 151996
-69351 354525
-405877 2293326
-861765 5128649
-4889819 32517688
-10279851 72682398
diff --git a/src/plugins/e-acsl/doc/memory_model/timeList.dat b/src/plugins/e-acsl/doc/memory_model/timeList.dat
deleted file mode 100644
index cee607c1d4c369d8ea493177e4a3ac3c4a269d97..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/timeList.dat
+++ /dev/null
@@ -1,6 +0,0 @@
-nbstores time
-5317 20988
-32193 847482
-69351 3847986
-405877 121097172
-861765 545608598
diff --git a/src/plugins/e-acsl/doc/memory_model/timeNone.dat b/src/plugins/e-acsl/doc/memory_model/timeNone.dat
deleted file mode 100644
index 14536e44d73d9f5314046ff58b35c35ae00964be..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/timeNone.dat
+++ /dev/null
@@ -1,8 +0,0 @@
-nbstores time
-5317 65
-32193 434
-69351 1011
-405877 6475
-861765 14270
-4889819 77806
-10279851 193393
diff --git a/src/plugins/e-acsl/doc/memory_model/timeTree.dat b/src/plugins/e-acsl/doc/memory_model/timeTree.dat
deleted file mode 100644
index c87b31898341b0945732fcdf2a6f10a3ae7bab41..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/memory_model/timeTree.dat
+++ /dev/null
@@ -1,6 +0,0 @@
-nbstores time
-5317 7463
-32193 251187
-69351 1127598
-405877 34152290
-861765 161718277