[E-ACSL] detailled outline of user manual

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

src/plugins/e-acsl/doc/userman/Makefile

 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
 

src/plugins/e-acsl/doc/userman/biblio.bib

@@ -3,7 +3,7 @@
   author = {Loc 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},

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

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

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

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

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}
 

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

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