diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index b96e6ebf47ffe00f08d8114a388bddf9a8c9f1d7..15a0d50d2b998cd5b013d2e06f1badb027db8efa 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -30,7 +30,7 @@ install: e-acsl-implementation.pdf e-acsl.pdf
cp -f e-acsl-implementation.pdf \
$(DISTRIB_DIR)/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
-include support/MakeLaTeXModern
+include $(EACSL_DIR)/doc/support/MakeLaTeXModern
eacslversion.tex: Makefile
rm -f $@
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 4eaaf13e2e817a6789593f247481411ea2a0457e..7a06076bd560dedaca17476adcf1c47af53b70e0 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -56,7 +56,7 @@
CEA LIST, Software Reliability Laboratory\\
\vfill
\begin{flushleft}
- \textcopyright 2011-2012 CEA LIST
+ \textcopyright 2011-2013 CEA LIST
This work has been supported by the `Hi-Lite' FUI project (FUI AAP 9).
\end{flushleft}
diff --git a/src/plugins/e-acsl/doc/refman/support/MakeLaTeXModern b/src/plugins/e-acsl/doc/support/MakeLaTeXModern
similarity index 100%
rename from src/plugins/e-acsl/doc/refman/support/MakeLaTeXModern
rename to src/plugins/e-acsl/doc/support/MakeLaTeXModern
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..3a0c895251d649fe543940f98c87fbb2cfaf5d05
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -0,0 +1,80 @@
+MAIN=main
+DEPS_MODERN=eacslversion.tex biblio.bib macros.tex
+
+default: main.pdf
+
+main.pdf: $(DEPS_MODERN)
+
+EACSL_VERSION= 0.1+dev
+FC_VERSION= Fluorine-20130501
+
+EACSL_DIR=$(HOME)/plugins/e-acsl
+DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
+install: e-acsl-manual.pdf
+ cp -f $^ $(EACSL_DIR)/doc/manuals
+ cp -f main.pdf
+ $(DISTRIB_DIR)/download/e-acsl/e-acsl-$(EACSL_VERSION).pdf
+
+include $(EACSL_DIR)/doc/support/MakeLaTeXModern
+
+eacslversion.tex: Makefile
+ rm -f $@
+ echo '\\newcommand{\\eacslversion}{$(EACSL_VERSION)\\xspace}' > $@
+ echo '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}' >> $@
+ chmod a-w $@
+
+%.1: %.mp
+ mpost -interaction=batchmode $<
+
+%.mps: %.1
+ mv $< $@
+
+%.pp: %.tex pp
+ ./pp -utf8 $< > $@
+
+%.pp: %.c pp
+ ./pp -utf8 -c $< > $@
+
+%.tex: %.ctex pp
+ rm -f $@
+ ./pp $< > $@
+ chmod a-w $@
+
+%.bnf: %.tex transf
+ rm -f $@
+ ./transf $< > $@
+ chmod a-w $@
+
+%_modern.bnf: %.tex transf
+ rm -f $@
+ ./transf -modern $< > $@
+ chmod a-w $@
+
+%.ml: %.mll
+ ocamllex $<
+
+%.pdf: %.tex
+ pdflatex $*
+ makeindex $*
+ bibtex $*
+ pdflatex $*
+ pdflatex $*
+
+%.cmo: %.ml
+ ocamlc -c $<
+
+pp: pp.ml
+ ocamlopt -o $@ str.cmxa $^
+
+transf: transf.cmo transfmain.cmo
+ ocamlc -o $@ $^
+
+transfmain.cmo: transf.cmo
+
+.PHONY: clean
+
+clean:
+ rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
+ *.haux *.hbbl *.htoc \
+ *.cb* *.cm? *.bbl *.blg *.idx *.ind *.ilg \
+ transf trans.ml pp.ml pp
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
new file mode 100644
index 0000000000000000000000000000000000000000..1634215d40d8dc3e0a05269a31c6d46d8fed5612
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -0,0 +1,84 @@
+@manual{userman,
+ title = {Frama-C User Manual},
+ author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
+ Armand Puccetti and Virgile Prevosto and Julien Signoles and
+ Boris Yakobowski},
+ year = 2013,
+ month = may,
+ note = {\url{http://frama-c.cea.fr/download/user-manual.pdf}}
+}
+
+@manual{plugin-dev-guide,
+ author = {Julien Signoles and Loïc Correnson and Matthieu Lemerre and
+ Virgile Prevosto},
+ title = {{Frama-C Plug-in Development Guide}},
+ year = 2013,
+ month = apr,
+ note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
+}
+
+@manual{value,
+ author = {Pascal Cuoq and Boris Yakobowski and Virgile Prevosto},
+ title = {{Frama-C}'s value analysis plug-in},
+ year = 2013,
+ month = apr,
+ note = {\mbox{\url{http://frama-c.cea.fr/download/value-analysis.pdf}}},
+}
+
+@manual{acsl,
+ 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}
+}
+
+@manual{acsl-implem,
+ author = {Baudin, Patrick and Pascal Cuoq 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 ---
+ Frama-C Oxygen implementation.},
+ year = {2012}
+}
+
+@misc{slicing,
+ author = {Patrick Baudin and Anne Pacalet},
+ title = {Slicing plug-in},
+ note = {\mbox{\url{http://frama-c.com/slicing.html}}},
+}
+
+@manual{wp,
+ author = {Loïc Correnson and Zaynah Dargaye and Anne Pacalet},
+ title = {{Frama-C}'s {WP} plug-in},
+ year = 2013,
+ month = apr,
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-wp-manual.pdf}}},
+}
+
+@manual{rte,
+ author = {Philippe Herrmann and Julien Signoles},
+ title = {Annotation Generation: {Frama-C}'s {RTE} plug-in},
+ year = 2013,
+ month = apr,
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-rte-manual.pdf}}},
+}
+
+@inproceedings{fmics12,
+ author = {Loïc Correnson and Julien Signoles},
+ title = {{Combining Analysis for C Program Verification}},
+ booktitle = {{Formal Methods for Industrial Critical Systems (FMICS)}},
+ year = 2012,
+ month = August,
+}
+
+@inproceedings{sefm12,
+ author = {Pascal Cuoq and Florent Kirchner and Nikolai Kosmatov and Virgile
+ Prevosto and Julien Signoles and Boris Yakobowski},
+ title = {{Frama-C, A software Analysis Perspective}},
+ booktitle = {{Software Engineering and Formal Methods (SEFM)}},
+ year = 2012,
+ month = oct,
+}
diff --git a/src/plugins/e-acsl/doc/userman/cealistlogo.jpg b/src/plugins/e-acsl/doc/userman/cealistlogo.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..966be5a8ff6d50d9a7f50759633ca144c4c5db1c
Binary files /dev/null and b/src/plugins/e-acsl/doc/userman/cealistlogo.jpg differ
diff --git a/src/plugins/e-acsl/doc/userman/eacslversion.tex b/src/plugins/e-acsl/doc/userman/eacslversion.tex
new file mode 100644
index 0000000000000000000000000000000000000000..c5b0dd941b6d7806f51e4aeba1d928fcf593e0c3
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/eacslversion.tex
@@ -0,0 +1,2 @@
+\newcommand{\eacslversion}{0.1+dev\xspace}
+\newcommand{\fcversion}{Fluorine-20130501\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-book.cls b/src/plugins/e-acsl/doc/userman/frama-c-book.cls
new file mode 100644
index 0000000000000000000000000000000000000000..47463e1cc216eb43d7a224547eac4fef99aed78b
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/frama-c-book.cls
@@ -0,0 +1,332 @@
+% --------------------------------------------------------------------------
+% --- LaTeX Class for Frama-C Books ---
+% --------------------------------------------------------------------------
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
+% --------------------------------------------------------------------------
+% --- Base Class management ---
+% --------------------------------------------------------------------------
+\LoadClass[a4paper,11pt,twoside,openright]{report}
+\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
+\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
+\ProcessOptions
+\RequirePackage{fullpage}
+\RequirePackage{hevea}
+\RequirePackage{ifthen}
+\RequirePackage[T1]{fontenc}
+\RequirePackage[latin1]{inputenc}
+\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref}
+\RequirePackage{amssymb}
+\RequirePackage{xcolor}
+\RequirePackage[pdftex]{graphicx}
+\RequirePackage{xspace}
+\RequirePackage{makeidx}
+\RequirePackage[leftbars]{changebar}
+\RequirePackage[english]{babel}
+\RequirePackage{fancyhdr}
+\RequirePackage{titlesec}
+% --------------------------------------------------------------------------
+% --- Page Layout ---
+% --------------------------------------------------------------------------
+\setlength{\voffset}{-6mm}
+\setlength{\headsep}{8mm}
+\setlength{\footskip}{21mm}
+\setlength{\textheight}{238mm}
+\setlength{\topmargin}{0mm}
+\setlength{\textwidth}{155mm}
+\setlength{\oddsidemargin}{2mm}
+\setlength{\evensidemargin}{-2mm}
+\setlength{\changebarsep}{0.5cm}
+\setlength{\headheight}{13.6pt}
+\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
+ \begin{picture}(0,0)(#1,#2)
+ \put(0,0){\includegraphics[width=#3cm]{#4}}
+ \end{picture}}
+\fancypagestyle{plain}{%
+ \fancyfoot{}
+ \fancyhead{}
+ \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
+ \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
+ \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
+ \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
+ \fancyfoot[C]{\small\textsf{\thepage}}
+ \renewcommand{\headrulewidth}{0pt}
+ \renewcommand{\footrulewidth}{0pt}
+}
+\fancypagestyle{blank}{%
+ \fancyfoot{}
+ \fancyhead{}
+ \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
+ \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
+}
+%% Redefinition of cleardoublepage for empty page being blank
+\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
+\hbox{}
+\thispagestyle{#1}
+\newpage
+\fi\fi}
+\def\cleardoublepage{\cleardoublepagewith{blank}}
+\pagestyle{plain}
+
+% --------------------------------------------------------------------------
+% --- Cover Page ---
+% --------------------------------------------------------------------------
+\newcommand{\coverpage}[1]{%
+\thispagestyle{empty}
+\setlength\unitlength{1cm}
+\begin{picture}(0,0)(3.27,26.75)
+\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
+\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
+\end{picture}
+}
+
+% --------------------------------------------------------------------------
+% --- Title Page ---
+% --------------------------------------------------------------------------
+\renewenvironment{titlepage}%
+{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
+{\end{center}}
+\renewcommand{\title}[2]{
+\vspace{20mm}
+{\Huge\bfseries #1}
+
+\bigskip
+
+{\LARGE #2}
+\vspace{20mm}
+}
+\renewcommand{\author}[1]{
+\vspace{20mm}
+
+{#1}
+
+\medskip
+}
+% --------------------------------------------------------------------------
+% --- Sectionning ---
+% --------------------------------------------------------------------------
+\titleformat{\chapter}[display]{\Huge\raggedleft}%
+{\huge\chaptertitlename\,\thechapter}{0.5em}{}
+\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
+[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
+\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
+[\vspace{-8pt}]
+
+% --------------------------------------------------------------------------
+% --- Main Text Style ---
+% --------------------------------------------------------------------------
+%\raggedright
+\setlength\parindent{0pt}
+\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
+\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
+\def\FramaC{\textsf{Frama-C}\xspace}
+% --------------------------------------------------------------------------
+% --- Listings ---
+% --------------------------------------------------------------------------
+\RequirePackage{listings}
+
+\lstdefinelanguage{ACSL}{%
+ morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
+ boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
+ exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
+ model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
+ union,variant},
+ keywordsprefix={\\},
+ alsoletter={\\},
+ morecomment=[l]{//}
+}
+
+\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
+\definecolor{lstbg}{gray}{0.98}
+\definecolor{lstfg}{gray}{0.10}
+\definecolor{lstrule}{gray}{0.6}
+\definecolor{lstnum}{gray}{0.4}
+\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
+\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
+\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
+\definecolor{lstfile}{gray}{0.85}
+\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
+\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\scriptsize\else\normalfont\ttfamily\mdseries\scriptsize\fi}
+\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
+\def\lp@keyword{}
+\def\lp@special{\color{lstfg}}
+\def\lp@comment{\normalfont\ttfamily\mdseries}
+\def\lp@string{\color{lstfg}} \def\lp@ident{}
+\def\lp@number{\rmfamily\tiny\color{lstnum}}
+\lstdefinestyle{frama-c-style}{%
+ basicstyle=\lp@inline,%
+ identifierstyle=\lp@ident,%
+ commentstyle=\lp@comment,%
+ keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
+ keywordstyle=[2]\lp@special,%
+ stringstyle=\lp@string,%
+ emphstyle=\lp@ident\underbar,%
+ showstringspaces=false,%
+ mathescape=true,%
+ numberstyle=\lp@number,%
+ xleftmargin=6ex,xrightmargin=2ex,%
+ framexleftmargin=1ex,%
+ frame=l,%
+ framerule=1pt,%
+ rulecolor=\color{lstrule},%
+ backgroundcolor=\color{lstbg},%
+ moredelim={*[s]{/*@}{*/}},%
+ moredelim={*[l]{//@}},%
+ morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
+ morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
+ mathescape=true,
+ escapechar=`
+% breaklines is broken when using a inline and background
+% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
+}
+
+\lstdefinestyle{c}%
+{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
+\lstdefinestyle{c-basic}%
+{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
+
+
+% --- C/ACSL Stuff ---------------------------------------------------------
+% Make 'c' the default style
+\lstset{style=c}
+
+\newcommand{\listinginput}[3][1]%
+{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
+
+\newcommand{\listinginputcaption}[4][1]%
+{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}
+
+\lstnewenvironment{listing}[2][1]%
+{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
+
+\lstnewenvironment{listing-nonumber}%
+{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
+
+% --- Verbatim Stuff -------------------------------------------------------
+\lstdefinelanguage{Shell}[]{csh}%
+{identifierstyle=\lp@basic,mathescape=false,backgroundcolor=,literate={\\\$}{\$}1}
+\lstnewenvironment{shell}[1][]{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
+
+% ---- Stdout Stuff --------------------------------------------------------
+\lstdefinelanguage{Logs}[]{csh}%
+{identifierstyle=\lp@basic,backgroundcolor=}
+\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
+\newcommand{\logsinput}[1]%
+{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
+
+% --------------------------------------------------------------------------
+% --- Developer Code Stuff ---
+% --------------------------------------------------------------------------
+
+\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
+
+% --- Style ----------------------------------------------------------------
+\lstdefinestyle{framac-code-style}{%
+basicstyle=\lp@inline,%
+numberstyle=\lp@number,%
+keywordstyle=[1]\sffamily\color{lstmodule},%
+keywordstyle=[2]\sffamily\color{lstspecial},%
+keywordstyle=[3]\sffamily\bfseries,%
+identifierstyle=\rmfamily,%
+stringstyle=\ttfamily\color{lstfg},%
+commentstyle=\rmfamily\bfseries\color{lsttxt},%
+}
+\lstdefinestyle{framac-shell-style}{%
+mathescape=false,%
+basicstyle=\lp@basic,%
+numberstyle=\lp@number,%
+keywordstyle=\sffamily\bfseries,%
+keywordstyle=[1]\sffamily\color{lstmodule},%
+keywordstyle=[2]\sffamily\color{lstspecial},%
+keywordstyle=[3]\sffamily\bfseries,%
+identifierstyle=\ttfamily,%
+stringstyle=\ttfamily\color{lstfg},%
+commentstyle=\rmfamily\bfseries\color{lsttxt},%
+literate={\\\$}{\$}1,%
+}
+% --- Configure ------------------------------------------------------------
+\lstdefinelanguage{Configure}[]{csh}{%
+style=framac-shell-style,%
+morekeywords={fi},%
+}
+\lstnewenvironment{configurecode}[1][]%
+{\lstset{language=Configure,#1}}{}
+\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
+% --- Makefile ------------------------------------------------------------
+\lstdefinelanguage{Makefile}[]{make}{%
+style=framac-shell-style,%
+morekeywords={include},%
+}
+\lstnewenvironment{makefilecode}[1][]%
+{\lstset{language=Makefile,#1}}{}
+\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
+% --- C- for Developer ----------------------------------------------------
+\lstdefinestyle{framac-code}%
+ {language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
+\lstnewenvironment{ccode}[1][]%
+{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
+\newcommand{\cinput}[1]%
+{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
+\newcommand{\cinline}[1]%
+{\lstinline[style=framac-code]{#1}}
+% --- Ocaml ----------------------------------------------------------------
+\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
+style=framac-code-style,%
+deletekeywords={when,module,struct,sig,begin,end},%
+morekeywords=[2]{failwith,raise,when},%
+morekeywords=[3]{module,struct,sig,begin,end},%
+literate=%
+{~}{${\scriptstyle\thicksim}$}1%
+{<}{$<$}1%
+{>}{$>$}1%
+{->}{$\rightarrow$}1%
+{<-}{$\leftarrow$}1%
+{:=}{$\leftarrow$}1%
+{<=}{$\leq$}1%
+{>=}{$\geq$}1%
+{==}{$\equiv$}1%
+{!=}{$\not\equiv$}1%
+{<>}{$\neq$}1%
+{'a}{$\alpha$}1%
+{'b}{$\beta$}1%
+{'c}{$\gamma$}1%
+{µ}{`{}}1%
+}
+
+\lstdefinestyle{ocaml-basic}%
+{language=Ocaml,basicstyle=\lp@basic}
+\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
+\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
+% --------------------------------------------------------------------------
+\lstdefinelanguage{Why}{%
+ morekeywords={
+ type, logic, axiom, predicate, goal,
+ forall, let, in,
+ },
+ morecomment=[s]{(*}{*)},
+ alsoletter={_},
+ literate=%
+ {->}{$\Rightarrow$}1%
+ {forall}{$\forall$}1%
+ {not}{$\neg$}1%
+ {<>}{$\neq$}1%
+ {...}{$\dots$}1%
+ %{_}{\_}1%
+ %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
+ }
+
+\lstdefinestyle{why-style}{%
+language=Why,%
+style=framac-code-style,%
+basicstyle=\lp@inline,%
+}
+
+\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
+\newcommand{\whyinput}[1]%
+{\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
+\newcommand{\whyinline}[1]%
+{\lstinline[style=why-style]{#1}}
+
+% --------------------------------------------------------------------------
+% --- End. ---
+% --------------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-cover.pdf b/src/plugins/e-acsl/doc/userman/frama-c-cover.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..4e14243c8064ca92d696fd354476dcdb31092895
Binary files /dev/null and b/src/plugins/e-acsl/doc/userman/frama-c-cover.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-left.pdf b/src/plugins/e-acsl/doc/userman/frama-c-left.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..ddf8888d292539177ab81c1b33d6411edf51c820
Binary files /dev/null and b/src/plugins/e-acsl/doc/userman/frama-c-left.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/frama-c-right.pdf b/src/plugins/e-acsl/doc/userman/frama-c-right.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..db9b236dfdb19d9a6631ec55eee63f431f8d6f0d
Binary files /dev/null and b/src/plugins/e-acsl/doc/userman/frama-c-right.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
new file mode 100644
index 0000000000000000000000000000000000000000..51719d3d384b090aface34a61becfd4faa963e13
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -0,0 +1,250 @@
+%%% Environnements dont le corps est suprimé, et
+%%% commandes dont la définition est vide,
+%%% lorsque PrintRemarks=false
+
+\usepackage{comment}
+
+\newcommand{\framac}{\textsc{Frama-C}\xspace}
+\newcommand{\acsl}{\textsc{ACSL}\xspace}
+\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
+\newcommand{\C}{\textsc{C}\xspace}
+\newcommand{\jml}{\textsc{JML}\xspace}
+
+\newcommand{\nodiff}{\emph{No difference with \acsl.}}
+\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
+\newcommand{\limited}[1]{\emph{Limited to #1.}}
+\newcommand{\absent}{\emph{No such feature in \eacsl.}}
+\newcommand{\absentwhy}[1]{\emph{No such feature in \eacsl: #1.}}
+\newcommand{\absentexperimental}{\emph{No such feature in \eacsl, since it is
+ still experimental in \acsl.}}
+\newcommand{\absentexcept}[1]{\emph{No such feature in \eacsl, but #1.}}
+\newcommand{\difficultwhy}[2]{\emph{#1 is usually difficult to implement, since
+ it requires #2. Thus you would not wonder if most tools do not support it
+ (or support it partially).}}
+\newcommand{\difficultswhy}[2]{\emph{#1 are usually difficult to implement,
+ since they require #2. Thus you would not wonder if most tools do not
+ support them (or support them partially).}}
+\newcommand{\difficult}[1]{\emph{#1 is usually difficult to implement. Thus
+ you would not wonder if most tools do not support it (or support
+ it partially).}}
+\newcommand{\difficults}[1]{\emph{#1 are usually difficult to implement. Thus
+ you would not wonder if most tools do not support them (or support
+ them partially).}}
+
+\newcommand{\changeinsection}[2]{\textbf{Section \ref{sec:#1}:} #2.}
+
+\newcommand{\todo}[1]{{\large \textbf{TODO: #1.}}}
+
+\newcommand{\markdiff}[1]{{\color{blue}{#1}}}
+\newenvironment{markdiffenv}[1][]{%
+ \begin{changebar}%
+ \markdiff\bgroup%
+}%
+{\egroup\end{changebar}}
+
+% true = prints remarks for the ACSL working group.
+% false = prints no remark for the distributed version of ASCL documents
+\newboolean{PrintRemarks}
+\setboolean{PrintRemarks}{false}
+
+% true = prints marks signaling the state of the implementation
+% false = prints only the ACSL definition, without remarks on implementation.
+\newboolean{PrintImplementationRq}
+\setboolean{PrintImplementationRq}{true}
+
+% true = remarks about the current state of implementation in Frama-C
+% are in color.
+% false = they are rendered with an underline
+\newboolean{ColorImplementationRq}
+\setboolean{ColorImplementationRq}{true}
+
+%% \ifthenelse{\boolean{PrintRemarks}}%
+%% {\newenvironment{todo}{%
+%% \begin{quote}%
+%% \begin{tabular}{||p{0.8\textwidth}}TODO~:\itshape}%
+%% {\end{tabular}\end{quote}}}%
+%% {\excludecomment{todo}}
+
+\ifthenelse{\boolean{PrintRemarks}}%
+ {\newenvironment{remark}[1]{%
+ \begin{quote}\itshape%
+ \begin{tabular}{||p{0.8\textwidth}}Remarque de {#1}~:}%
+ {\end{tabular}\end{quote}}}%
+ {\excludecomment{remark}}
+
+\newcommand{\oldremark}[2]{%
+\ifthenelse{\boolean{PrintRemarks}}{%
+ %\begin{quote}\itshape%
+ %\begin{tabular}{||p{0.8\textwidth}}Vieille remarque de {#1}~: #2%
+ %\end{tabular}\end{quote}%
+}%
+{}}
+
+\newcommand{\highlightnotreviewed}{%
+\color{blue}%
+}%
+
+\newcommand{\notreviewed}[2][]{%
+\ifthenelse{\boolean{PrintRemarks}}{%
+ \begin{changebar}%
+ {\highlightnotreviewed #2}%
+ \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
+ \end{changebar}%
+}%
+{}}
+
+\ifthenelse{\boolean{PrintRemarks}}{%
+\newenvironment{notreviewedenv}[1][]{%
+ \begin{changebar}%
+ \highlightnotreviewed%
+ \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
+ \bgroup}%
+ {\egroup%
+ \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}}%
+{\excludecomment{notreviewedenv}}
+
+%%% Commandes et environnements pour la version relative à l'implementation
+\newcommand{\highlightnotimplemented}{%
+\ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
+ {\ul}%
+}%
+
+\newcommand{\notimplemented}[2][]{%
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{changebar}%
+ {\highlightnotimplemented #2}%
+ \ifthenelse{\equal{#1}{}}{}{\footnote{#1}}%
+ \end{changebar}%
+}%
+{#2}}
+
+\newenvironment{notimplementedenv}[1][]{%
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{changebar}%
+ \highlightnotimplemented%
+ \ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
+ \bgroup
+}{}}%
+{\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \egroup%
+ \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}{}}
+
+%%% Environnements et commandes non conditionnelles
+\newcommand{\experimental}{\textsc{Experimental}}
+
+\newsavebox{\fmbox}
+\newenvironment{cadre}
+ {\begin{lrbox}{\fmbox}\begin{minipage}{0.98\textwidth}}
+ {\end{minipage}\end{lrbox}\fbox{\usebox{\fmbox}}}
+
+
+\newcommand{\keyword}[1]{\lstinline|#1|\xspace}
+\newcommand{\keywordbs}[1]{\lstinline|\\#1|\xspace}
+
+\newcommand{\integer}{\keyword{integer}}
+\newcommand{\real}{\keyword{real}}
+\newcommand{\bool}{\keyword{boolean}}
+
+\newcommand{\assert}{\keyword{assert}}
+\newcommand{\terminates}{\keyword{terminates}}
+\newcommand{\assume}{\keyword{assume}}
+\newcommand{\requires}{\keyword{requires}}
+\newcommand{\ensures}{\keyword{ensures}}
+\newcommand{\exits}{\keyword{exits}}
+\newcommand{\returns}{\keyword{returns}}
+\newcommand{\breaks}{\keyword{breaks}}
+\newcommand{\continues}{\keyword{continues}}
+\newcommand{\assumes}{\keyword{assumes}}
+\newcommand{\assigns}{\keyword{assigns}}
+\newcommand{\reads}{\keyword{reads}}
+\newcommand{\decreases}{\keyword{decreases}}
+
+\newcommand{\boundseparated}{\keywordbs{bound\_separated}}
+\newcommand{\Exists}{\keywordbs{exists}~}
+\newcommand{\Forall}{\keywordbs{forall}~}
+\newcommand{\bslambda}{\keywordbs{lambda}~}
+\newcommand{\freed}{\keywordbs{freed}}
+\newcommand{\fresh}{\keywordbs{fresh}}
+\newcommand{\fullseparated}{\keywordbs{full\_separated}}
+\newcommand{\distinct}{\keywordbs{distinct}}
+\newcommand{\Max}{\keyword{max}}
+\newcommand{\nothing}{\keywordbs{nothing}}
+\newcommand{\numof}{\keyword{num\_of}}
+\newcommand{\offsetmin}{\keywordbs{offset\_min}}
+\newcommand{\offsetmax}{\keywordbs{offset\_max}}
+\newcommand{\old}{\keywordbs{old}}
+\newcommand{\at}{\keywordbs{at}}
+
+\newcommand{\If}{\keyword{if}~}
+\newcommand{\Then}{~\keyword{then}~}
+\newcommand{\Else}{~\keyword{else}~}
+\newcommand{\For}{\keyword{for}~}
+\newcommand{\While}{~\keyword{while}~}
+\newcommand{\Do}{~\keyword{do}~}
+\newcommand{\Let}{\keywordbs{let}~}
+\newcommand{\Break}{\keyword{break}}
+\newcommand{\Return}{\keyword{return}}
+\newcommand{\Continue}{\keyword{continue}}
+
+\newcommand{\exit}{\keyword{exit}}
+\newcommand{\main}{\keyword{main}}
+\newcommand{\void}{\keyword{void}}
+
+\newcommand{\struct}{\keyword{struct}}
+\newcommand{\union}{\keywordbs{union}}
+\newcommand{\inter}{\keywordbs{inter}}
+\newcommand{\typedef}{\keyword{typedef}}
+\newcommand{\result}{\keywordbs{result}}
+\newcommand{\separated}{\keywordbs{separated}}
+\newcommand{\sizeof}{\keyword{sizeof}}
+\newcommand{\strlen}{\keywordbs{strlen}}
+\newcommand{\Sum}{\keyword{sum}}
+\newcommand{\valid}{\keywordbs{valid}}
+\newcommand{\validrange}{\keywordbs{valid\_range}}
+\newcommand{\offset}{\keywordbs{offset}}
+\newcommand{\blocklength}{\keywordbs{block\_length}}
+\newcommand{\baseaddr}{\keywordbs{base\_addr}}
+\newcommand{\comparable}{\keywordbs{comparable}}
+
+\newcommand{\N}{\ensuremath{\mathbb{N}}}
+\newcommand{\ra}{\ensuremath{\rightarrow}}
+\newcommand{\la}{\ensuremath{\leftarrow}}
+
+% BNF grammar
+\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
+\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
+\newif\ifspace
+\newif\ifnewentry
+\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
+\newcommand{\term}[2]{\addspace\hbox{\lstinline|#1|%
+\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
+\newcommand{\nonterm}[2]{%
+ \ifthenelse{\equal{#2}{}}%
+ {\addspace\hbox{\textsl{#1}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}%
+ {\addspace\hbox{\textsl{#1}\footnote{#2}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}}
+\newcommand{\repetstar}{$^*$\spacetrue}
+\newcommand{\repetplus}{$^+$\spacetrue}
+\newcommand{\repetone}{$^?$\spacetrue}
+\newcommand{\lparen}{\addspace(}
+\newcommand{\rparen}{)}
+\newcommand{\orelse}{\addspace$\mid$\spacetrue}
+\newcommand{\sep}{ \\[2mm] \spacefalse\newentrytrue}
+\newcommand{\newl}{ \\ & & \spacefalse}
+\newcommand{\alt}{ \\ & $\mid$ & \spacefalse}
+\newcommand{\is}{ & $::=$ & \newentryfalse}
+\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
+\newcommand{\synt}[1]{$\spacefalse#1$}
+\newcommand{\emptystring}{$\epsilon$}
+\newcommand{\below}{See\; below}
+
+% colors
+
+\definecolor{darkgreen}{rgb}{0, 0.5, 0}
+
+% theorems
+
+\newtheorem{example}{Example}[chapter]
+
+% for texttt
+
+\newcommand{\bs}{\ensuremath{\backslash}}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..7b6164d578bf513e77869157f65826036da056fa
Binary files /dev/null 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
new file mode 100644
index 0000000000000000000000000000000000000000..c65213626b1ae38fd3e529fd2f78ddf46d3debec
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -0,0 +1,99 @@
+\documentclass[web]{frama-c-book}
+
+\usepackage{graphicx}
+\usepackage{calc}
+
+\include{macros}
+\include{eacslversion}
+
+\makeindex
+
+\begin{document}
+
+\coverpage{\eacsl User Manual}
+
+\begin{titlepage}
+\begin{flushleft}
+\includegraphics[height=14mm]{cealistlogo.jpg}
+\end{flushleft}
+\vfill
+\title{\framac's \eacsl Plug-in}{Release \eacslversion compatible
+ with \fcversion}
+\author{Julien Signoles}
+\begin{tabular}{l}
+CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
+\end{tabular}
+\vfill
+\begin{flushleft}
+ \textcopyright 2013 CEA LIST
+
+ This work has been supported by the `Hi-Lite' FUI project (FUI AAP 9).
+\end{flushleft}
+\end{titlepage}
+
+\tableofcontents
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\chapter*{Foreword}
+\markright{}
+\addcontentsline{toc}{chapter}{Foreword}
+
+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
+future.
+
+%% \section*{Acknowledgements}
+
+%% We gratefully thank all the people who contributed to this document: Patrick
+%% Baudin, Mickaël Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\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}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\appendix
+
+%% \include{user-changes}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\bibname}
+\bibliographystyle{plain}
+\bibliography{./biblio}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%% \cleardoublepage
+%% \addcontentsline{toc}{chapter}{\listfigurename}
+%% \listoffigures
+
+%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%% \cleardoublepage
+%% \addcontentsline{toc}{chapter}{\indexname}
+%% \printindex
+
+\end{document}