diff --git a/src/plugins/e-acsl/README b/src/plugins/e-acsl/README
index ca18a9b20ad73ce06ff12493b2ac36eaf1da3583..c56f736f056dde5d5a3d8aa86345504af5bb36d3 100644
--- a/src/plugins/e-acsl/README
+++ b/src/plugins/e-acsl/README
@@ -21,7 +21,7 @@
This package contains the Frama-C's E-ACSL plug-in. It takes as input an
annotated C program and returns the same program in which annotations have
been converted into C code dedicated to runtime assertion checking: this code
-fails at runtime if and only if the annotation is violated at runtime.
+fails at runtime if the annotation is violated at runtime.
Annotations must be written in a subset of ACSL (ANSI/ISO C Specification
Language), namely E-ACSL (Executable ANSI/ISO C Specification Language). E-ACSL
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 3a0c895251d649fe543940f98c87fbb2cfaf5d05..261adb19591b84eb97cab54d93b8ed32b3b177c5 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -1,5 +1,8 @@
MAIN=main
-DEPS_MODERN=eacslversion.tex biblio.bib macros.tex
+DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
+ introduction.tex \
+ provides.tex \
+ limitations.tex
default: main.pdf
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 1634215d40d8dc3e0a05269a31c6d46d8fed5612..163658f1bcc6ceab054b880cafa4fd3ce1b83580 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -3,7 +3,7 @@
author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
Armand Puccetti and Virgile Prevosto and Julien Signoles and
Boris Yakobowski},
- year = 2013,
+ year = apr,
month = may,
note = {\url{http://frama-c.cea.fr/download/user-manual.pdf}}
}
@@ -29,9 +29,9 @@
author = {Baudin, Patrick and Filli\^{a}tre, Jean-Christophe and
March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
- month = sep,
- title = {{ACSL: ANSI/ISO C Specification Language. Version 1.6}},
- year = {2012}
+ month = apr,
+ title = {{ACSL: ANSI/ISO C Specification Language. Version 1.7}},
+ year = {2013}
}
@manual{acsl-implem,
@@ -44,6 +44,34 @@
year = {2012}
}
+@manual{eacsl,
+ author = {Julien Signoles},
+ title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.7},
+ year = 2013,
+ month = may,
+ note = {URL: http://frama-c.com/download/ e-acsl/e-acsl.pdf}
+}
+
+@manual{eacsl-implem,
+ author = {Julien Signoles},
+ title = {E-ACSL Version 1.7.
+ Implementation in Frama-C Plug-in E-ACSL version 0.2},
+ year = 2013,
+ month = may,
+ note = {URL: http://frama-c.com/download/e-acsl/ e-acsl-implementation.pdf}}
+}
+
+@inproceedings{sac13,
+ author = {Micka\"{e}l Delahaye and Nikolai Kosmatov and Julien Signoles},
+ title = {Common Specification Language for Static and Dynamic Analysis of
+ {C} Programs},
+ booktitle = {the 28th Annual ACM Symposium on Applied Computing ({SAC})},
+ publisher = {ACM},
+ year = 2013,
+ month = mar,
+ pages = {1230--1235},
+}
+
@misc{slicing,
author = {Patrick Baudin and Anne Pacalet},
title = {Slicing plug-in},
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
new file mode 100644
index 0000000000000000000000000000000000000000..875ce86c4dcaab210ebec636e789d28035aebdac
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -0,0 +1,14 @@
+\chapter{Introduction}
+
+\framac~\cite{userman,sefm12} is a modular analysis framework for the C language
+which supports the ACSL specification language~\cite{acsl}. This manual
+documents the \eacsl plug-in of \framac. This plug-in automatically translates
+an annotated C code into a \C code which fails at runtime if an annotation is
+violated. If no annotation is violated, the behavior of the new program is
+exactly the same than the one of the original program.
+
+Annotations must be written in the \eacsl specification
+language~\cite{eacsl,sac13} which is a subset of \acsl. This plug-in is still in
+a preliminary state: some parts of E-ACSL are not yet supported. Which \eacsl
+annotations are currently handled by the \eacsl plug-in is documented in a
+separated document~\cite{eacsl-implem}.
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6364cd48d8bdca3ed259ed4f9db266a83cd56bcf
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -0,0 +1,9 @@
+\chapter{Known limitations}
+
+\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
+\end{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index 7b6164d578bf513e77869157f65826036da056fa..2af7723511c8e67f4814f6b81bdfb6c1f9812a8a 100644
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index c65213626b1ae38fd3e529fd2f78ddf46d3debec..3edf8c1769b2d2b6d78a8bc2d310e01c8f0e08e6 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -42,8 +42,8 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
This is the user manual of the \framac plug-in
\eacsl\footnote{\url{http://frama-c.com/eacsl}}. The content of this document
corresponds to its version \eacslversion (\today) compatible with the version
-\fcversion of \framac~\cite{userman}. However the development of the \eacsl
-plug-in is still ongoing: features described here may still evolve in the
+\fcversion of \framac~\cite{userman,sefm12}. However the development of the
+\eacsl plug-in is still ongoing: features described here may still evolve in the
future.
%% \section*{Acknowledgements}
@@ -53,27 +53,13 @@ future.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{itemize}
-\item Introduction
-\item What the Plug-in Provides
-\item Parameterizing the Plug-in
-\item Limitations
-\end{itemize}
-
-%% \include{user-intro}
-%% \include{user-overview}
-%% \include{user-start}
-%% \include{user-plugins}
-%% \include{user-sources}
-%% \include{user-analysis}
-%% \include{user-properties}
-%% \include{user-services}
-%% \include{user-gui}
-%% \include{user-errors}
+\include{introduction}
+\include{provides}
+\include{limitations}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\appendix
+%%\appendix
%% \include{user-changes}
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
new file mode 100644
index 0000000000000000000000000000000000000000..316c878558df180f183a3bae3524281bcb95d461
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -0,0 +1,19 @@
+\chapter{What the Plug-in Provides}
+
+\begin{itemize}
+\item simple example illustrating project generation and how to handle this
+ project to effectively verify annotations at runtime with GCC.
+ (-e-acsl-project)
+\item takes care of architecture (32, 64 bits)
+\item memory model (linking issue)
+\item GMP (linking issue)
+\item incomplete program
+ \begin{itemize}
+ \item function without code
+ \item program without main
+ \end{itemize}
+\item customizing e\_acsl\_assert
+\item combining E-ACSL with others Frama-C analysis
+ (e-acsl-prepare and -e-acsl-valid)
+\item verbosing policy
+\end{itemize}