diff --git a/VERSION b/VERSION
new file mode 100644
index 0000000000000000000000000000000000000000..c042c38017b3ecd2aa36437edad00ba95b4525a3
--- /dev/null
+++ b/VERSION
@@ -0,0 +1 @@
+Chlorine+
diff --git a/doc/userman/Makefile b/doc/userman/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..197a040a9908f8b3672d3d582f7d6e475d9d4170
--- /dev/null
+++ b/doc/userman/Makefile
@@ -0,0 +1,97 @@
+MAIN=main
+
+C_CODE=$(wildcard examples/*.[ci])
+VERSION_FILE=../../../../../VERSION
+ifeq ("$(wildcard $(VERSION_FILE))", "")
+VERSION_FILE=../../VERSION
+FC_VERSION+=Chlorine+
+else
+#internal mode
+FC_VERSION=$(shell cat $(VERSION_FILE))
+endif
+FCLANG_VERSION= $(shell cat $(VERSION_FILE))
+
+DEPS_MODERN=fclangversion.tex biblio.bib macros.tex \
+ introduction.tex \
+ provides.tex \
+ limitations.tex \
+ changes.tex \
+ $(C_CODE) \
+ $(VERSION_FILE)
+
+default: main.pdf
+
+main.pdf: $(DEPS_MODERN)
+
+EACSL_DIR=../..
+DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
+install:
+ mkdir -p $(EACSL_DIR)/doc/manuals/
+ cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
+# cp -f main.pdf \
+ $(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
+
+include $(EACSL_DIR)/doc/support/MakeLaTeXModern
+
+fclangversion.tex: Makefile
+ rm -f $@
+ printf '\\newcommand{\\fclangversion}{$(FCLANG_VERSION)\\xspace}\n' > $@
+ printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
+ 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
+ rm -f fclangversion.tex
diff --git a/doc/userman/biblio.bib b/doc/userman/biblio.bib
new file mode 100644
index 0000000000000000000000000000000000000000..3a444b97790c71379b9e33a1577d3fcb2aadd2d8
--- /dev/null
+++ b/doc/userman/biblio.bib
@@ -0,0 +1,154 @@
+@manual{userman,
+ title = {Frama-C User Manual},
+ author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
+ André Maroneze and Virgile Prevosto and
+ Armand Puccetti and Julien Signoles and
+ Boris Yakobowski},
+ 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}},
+ note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
+}
+
+@manual{eva,
+ author = {David B\"uhler and Pascal Cuoq and Boris Yakobowski and
+ Matthieu Lemerre and André Maroneze and Valentin Perelle and
+ Virgile Prevosto},
+ title = {{EVA} -- The Evolved Value Analysis plug-in},
+ 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},
+ title = {{ACSL: ANSI/ISO C Specification Language.}},
+}
+
+@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},
+ title = {ACSL: ANSI/ISO C Specification Language. ---
+ Frama-C Silicon implementation.},
+}
+
+@manual{eacsl,
+ author = {Julien Signoles},
+ title = {E-ACSL: Executable ANSI/ISO C Specification Language.},
+ note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
+}
+
+@manual{eacsl-implem,
+ author = {Julien Signoles},
+ title = {E-ACSL. Implementation in Frama-C Plug-in E-ACSL},
+ note = {\mbox{\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},
+}
+
+
+@inproceedings{rv13tutorial,
+ author = {Nikolaï Kosmatov and Julien Signoles},
+ title = {A Lesson on Runtime Assertion Checking with {Frama-C}},
+ booktitle = {International Conference on Runtime Verification ({RV 2013})},
+ publisher = {Springer},
+ series= {LNCS},
+ volume= {8174},
+ pages= {386--399},
+ year = 2013,
+ month = sep,
+}
+
+@manual{wp,
+ author = {Patrick Baudin and François Bobot and Loïc Correnson
+ and Zaynah Dargaye},
+ title = {{Frama-C}'s {WP} plug-in},
+ 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},
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-rte-manual.pdf}}},
+}
+
+@article{fac15,
+year={2015},
+month={jan},
+journal={Formal Aspects of Computing},
+title={{Frama-C: A Software Analysis Perspective}},
+publisher={Springer},
+keywords={Formal verification; Static analysis; Dynamic analysis; C},
+author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and
+Signoles, Julien and Yakobowski, Boris},
+pages={1-37},
+}
+
+@article{runtime-assertion-checking,
+ author = {Lori A. Clarke and
+ David S. Rosenblum},
+ title = {A historical perspective on runtime assertion checking in
+ software development},
+ journal = {ACM SIGSOFT Software Engineering Notes},
+ volume = {31},
+ number = {3},
+ year = {2006},
+ pages = {25-37},
+}
+
+@inproceedings{rv13,
+ author = {Nikolaï Kosmatov and Guillaume Petiot and Julien Signoles},
+ title = {An Optimized Memory Monitoring for Runtime Assertion Checking of
+ {C} Programs},
+ booktitle = {International Conference on
+ Runtime Verification ({RV 2013})},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {8174},
+ pages = {167--182},
+ year = 2013,
+ month = sep,
+}
+
+@inproceedings{jfla15,
+ title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
+ editor = {David Baelde and Jade Alglave},
+ year = {2015},
+ month = jan,
+ note = {In French},
+}
+
+@article{scp16,
+ title = {{Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring
+for C}},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ journal = {Science of Computer Programming},
+ publisher = {Elsevier},
+ pages = {226-246},
+ language = {English},
+ year = {2016},
+ month = oct,
+}
+
+@article{pldi16,
+ title = {{Shadow State Encoding for Efficient Monitoring of Block-level
+Properties}},
+ author = {Kostyantyn Vorobyov and Julien Signoles and Nikolai Kosmatov},
+ note = {Submitted for publication},
+}
diff --git a/doc/userman/cealistlogo.jpg b/doc/userman/cealistlogo.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..966be5a8ff6d50d9a7f50759633ca144c4c5db1c
Binary files /dev/null and b/doc/userman/cealistlogo.jpg differ
diff --git a/doc/userman/changes.tex b/doc/userman/changes.tex
new file mode 100644
index 0000000000000000000000000000000000000000..cf26227b1daa1957c4fe927e99e287fe829e834d
--- /dev/null
+++ b/doc/userman/changes.tex
@@ -0,0 +1,16 @@
+\chapter{Changes}\label{chap:changes}
+
+This chapter summarizes the changes in this documentation between each \fclang
+release, with the most recent releases first.
+
+\begin{itemize}
+\item New section \textbf{Additional Verifications}.
+\item Update each section with respect to the changes introduced since \eacsl
+ Sulfur-20180101.
+\end{itemize}
+
+\section*{Frama-C Chlorine-20180101}
+
+\begin{itemize}
+\item First release of this manual.
+\end{itemize}
diff --git a/doc/userman/description.tex b/doc/userman/description.tex
new file mode 100644
index 0000000000000000000000000000000000000000..57288d327c79f7a4c21e03892abea0f9ddff12f1
--- /dev/null
+++ b/doc/userman/description.tex
@@ -0,0 +1,1146 @@
+The \fclang plug-in intends to provide a full translation of C++ and ACSL++ into the \framac internal representation, and from there be able to be analyzed by other \framac plug-ins. This is a work in progress. The following sections describe the limitations of the current implementation.
+\begin{itemize}
+ \item The plug-in aims for the TBD version of C++
+ \item \acslpp is described in the companion \acslpp reference manual, also a part of the \framac release.
+\end{itemize}
+
+
+Notes
+\begin{itemize}
+ \item Which version of Clang?
+ \item Clang (8) support C++98 (except exported templates, later removed) and C++11 and current draft standard for C++1y
+ \item see https://clang.llvm.org/docs/UsersManual.html\#cxx for supported features in clang C++
+\end{itemize}
+
+\chapter{Installation}
+
+TBD - installation instructions
+
+\chapter{Running the plug-in}
+
+TBD - including command-line options
+
+\chapter{Current implementation details and limitations}
+
+\section{Preprocessing}
+
+As a refresher, the C/C++ preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onlinedocs/cpp/}) conceptually implements the following operations on a C++ source file:
+\begin{itemize}
+ \item The input is read and broken it into a sequence of physical lines according to the line terminators (ASCII character sequences \\r, \\n, or \\r\\n).
+ \item Each C trigraph is replaced by its corresponding character.
+ \item Any backslash-whitespace-line-terminator sequence is removed and the line that it ends is combined with the following line.
+ \item Comments are replaced by single spaces. This requires tokenizing the input to avoid recognizing comment markers within strings as indicating a comment. Note that this allows block comments to hide line terminations.
+ \item The input text is divided into preprocessing tokens grouped in logical lines. Each preprocessor token becomes a compiler token (except where \#\# concatenation occurs). However, \acslb tokens are slightly different, as described below.
+ \item The source text is transformed according to any preprocessing directives contained within it. Each preprocessing directive must be contained within one logical line
+
+\end{itemize}
+The result is a sequence of preprocessing tokens that is passed on to the
+remaining compiler phases.
+
+\subsection{Trigraphs}
+
+TBD - are these supported by clang?
+
+\subsection{Preprocessor tokens}
+Preprocessor tokens (per CPP) belong to one of five categories. White space (space, tab, TBD) serves only to separate tokens; it is not needed between tokens whose concatenation is not a single token. Line terminators also separate tokens and also delineate certain features: preprocessing directives and string literals do not extend over more than one (logical) line.
+\begin{itemize}
+ \item identifiers: character sequences that match the regular expression \texttt{[a-zA-Z\_][a-zA-Z\_0-9]*} . Dollar signs are allowed as non-digit identifier characters if the clang option \texttt{-fdollars-in-identifiers} is used. (TBD - on by default?)
+ \item number: character sequences that match the regular expression \texttt{[.]?[0-9]([0-9a-zA-Z.]|[eEpP][+-]))*} . (TBD - dollar signs also allowed?)
+ \item string literals: character sequence enclosed in " " or ' ' or < >, with \textbackslash " for " in a double-quoted literal (that is not a header file name) and \' for ' in a single-quoted literal.
+ \item punctuator: all single non-alphanumeric printable characters except \@, \# and `, and all multi-punctuation sequences that meaningful to C/C++ (e.g. >>>= ), but not an arbitrary multi-punctuation character sequence.
+ \\item other tokens: \@, \#, ` and all non-ASCII single characters.
+\end{itemize}
+TBD - unicode characters
+Note that not all preprocessor tokens are valid C/C++ parser tokens. Tokens in the other category have no meaning to C/C++ and the \texttt{number} category allows many sequences that are not legal C/C++ numeric tokens. These tokens will generally provoke compiler errors. For example in C/C++, 0..2 is one token and is not interpreted as two consecutive numeric tokens.
+
+\acsl and \acslpp have slightly different tokens than the above, so the preprocessor tokens need to be re-tokenized in some cases:
+\begin{itemize}
+ \item The \@ token is a whitespace character in \acslb.
+ \item There are some \acslb multi-character punctuator tokens that are not
+ preprocessor tokens:
+ \begin{itemize}
+ \item[] $==>$ (logical implies)
+ \item[] $-->$ (bit-wise implies)
+ \item[] $<==>$ (logical equality)
+ \item[] $<-->$ (bit-wise equality)
+ \item[] TBD any more?
+ \end{itemize}
+ These ACSL/ACSL++ tokens need to be assembled from multiple CPP tokens (and those CPP tokens must not be separated by white space)
+ \item A CPP numeric token that contains .. will not be a legal C/C++ number, but may be multiple legal \acslb tokens with the .. representing the range operator. For example, the single CPP token \texttt{0..last} is retokenized for \acslb as if it were written \texttt{0 .. last} .
+ \item \acslb allows certain built-in non-ASCII symbols, namely
+ \begin{itemize}
+ \item[] $\forall$ (unicode 0x2200) - universal quantifier
+ \item[] $\exists$ (unicode 0x2203) - existential quantifier
+% \item[] $\equal$ (unicode 0x2261) - equality
+% \item[] $\notequal$ (unicode 0x2262) - inequality
+ \item[] $\leq$ (unicode 0x2264) - less than or equal
+ \item[] $\geq$ (unicode 0x2265) - greater than or equal
+% \item[] $\minus$ (unicode 0x2212) - minus
+% \item[] $\implies$ (unicode 0x21D2) - implies
+% \item[] $\equiv$ (unicode 0x21D4) - equivalence
+ \item[] $\bigwedge$ (unicode 0x2227) - logical and
+ \item[] $\bigvee$ (unicode 0x2228) - logical or
+ \item[] $\neg$ (unicode 0x00AC) - logical negation
+% \item[] $\logicalxor$ (unicode 0x22BB) - logical inequivalence
+ \item[] $\subset$ (unicode 0x2208) - subset
+% \item[] $\Boolean$ (unicode 0x1D539) - set of booleans
+% \item[] $\Integer$ (unicode 0x2124) - set of integers
+% \item[] $\Real$ (unicode 0x211D) - set of reals
+ \item TBD - more - ensure unicode equivalent
+ \end{itemize}
+\end{itemize}
+
+\subsection{Preprocessor directives}
+A preprocessing directive consists of a line (after the previous preprocessing phaseshave been completed) that begins with optional white space, the '\#' character, additional optional white space, and a preprocessor directive identifier.
+The preprocessing language contains a fixed set of preprocessing directive identifiers:
+\begin{itemize}
+ \item \texttt{define}, \texttt{undef}
+ \item \texttt{if}, \texttt{ifdef}, \texttt{ifndef}, \texttt{elif}, \texttt{else}, \texttt{endif}
+ \item \texttt{warning}, \texttt{error}
+ \item \texttt{include}
+ \item \texttt{line}
+ \item \texttt{pragma}
+\end{itemize}
+In addition, identifiers that have been defined (by a \#define directive) as macros are expanded according to the macro expansion rules (not described here).
+
+Now ACSL/ACSL++ annotations are contained in C/C++ comments.
+Consequently, any directives contained in the annotation are not seen when the source file is processed simply as a C/C++ source file. However, the effect of some directives lasts until the end of the source file.
+Accordingly, ACSL++ imposes constrains on the directives that may be present within annotations:
+\begin{itemize}
+ \item \texttt{define} and \texttt{undef} are not permitted in an annotation
+ \item \texttt{if}, \texttt{ifdef}, \texttt{ifndef}, \texttt{elif}, \texttt{else}, \texttt{endif} are permitted but must be completely nested within the annotation in which they appear (an \#endif and its corresponding \#if/\#ifdef/\#ifndef must be in the same annotation comment.)
+ \item \texttt{warning} and \texttt{error} are permitted
+ \item \texttt{include} is permitted, but will cause errors if it contains, as is almost always the case, either \texttt{define} or \texttt{pragma} directives
+ \item \texttt{line} - TBD
+ \item \texttt{pragma} is not permitted
+\end{itemize}
+
+
+
+\section{ACSL++ constructs}
+
+%This chapter is the core of this manual and describes how to use the \fclang
+%plug-in.
+
+
+%% You can still call the option \shortopt{e-acsl-help} to get the list of
+%% available options with few lines of documentation.
+%First, Section~\ref{sec:simple} shows how to run the plug-in on a toy example,
+%compile the generated code with the \gcc compiler and detect invalid
+%annotations at runtime. Further, Section~\ref{sec:wrapper} describes \eacslgcc\
+%-- a convenience wrapper script around \framac and \gcc. The aim of this script
+%is to simplify instrumentation and compilation of the instrumented code.
+%Section~\ref{sec:exec-env} gives additional details on the execution of the
+%generated code. Next, Section~\ref{sec:incomplete} focuses on how to deal with
+%incomplete programs, \emph{i.e.} in which some functions are not defined or in
+%which there are no main function. Section~\ref{sec:combine} explains how to
+%combine the \eacsl plug-in with other \framac plug-ins. Finally,
+%Section~\ref{sec:custom} introduces how to customize the plug-in, and
+%Section~\ref{sec:verbose} details the verbosing policy of the plug-in.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%\section{Simple Example} % <<<
+%\label{sec:simple}
+%
+%This section is a mini-tutorial which explains from scratch how to use the
+%\eacsl plug-in to detect whether an \eacsl annotation is violated at runtime.
+%
+%% All tool invocations and code listings shown in this section assume a Linux
+%% distribution with system-wide \framac installation.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Running \eacsl}
+%\label{sec:run}
+%
+%Consider the following program containing two \eacsl assertions such that
+%the first assertion is valid, whereas the second one is not.
+%
+%\listingname{first.i}
+%\cinput{examples/first.i}
+%
+%Running \eacsl on \texttt{first.i} consists of adding \shortopt{e-acsl} option
+%to the \framac command line:
+%\begin{shell}
+%\$ frama-c -e-acsl first.i
+%[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
+%[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+%[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+%[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+%[kernel] Parsing first.i (no preprocessing)
+%[e-acsl] beginning translation.
+%<skip a warning when translating the Frama-C libc>
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%Even though \texttt{first.i} has already been pre-processed, \eacsl first asks
+%the \framac kernel to process and combine it against several header files
+%provided by the \eacsl plug-in. Further \eacsl translates the annotated code
+%into a new \framac project named \texttt{e-acsl}\footnote{The notion of
+%\emph{project} is explained in Section 8.1 of the \framac user
+%manual~\cite{userman}.}. By default, the option \shortopt{e-acsl} does nothing
+%more. It is however possible to have a look at the generated code in the
+%\framac GUI. This is also possible through the command line thanks to the
+%kernel options \shortopt{then-last} and \shortopt{print}. The former
+%switches to the last generated project, while the latter pretty prints the \C
+%code~\cite{userman}:
+%
+%\input{examples/instrumented_first.c}
+%
+%As you can see, the generated code contains additional type declarations,
+%constant declarations and global \acsl annotations not present in the initial
+%file \texttt{first.i}. They are part of the \eacsl monitoring library. You can
+%safely ignore them for now. The translated \texttt{main} function of
+%\texttt{first.i} is displayed at the end. After each \eacsl annotation,
+%a call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert} has been added.
+%
+%\begin{minipage}{\linewidth}
+%\begin{ccode}
+% /*@ assert x == 0; */
+% __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
+% /*@ assert x == 1; */
+% __e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
+%\end{ccode}
+%\end{minipage}
+%
+%Each call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert}, function
+%defined by the \eacsl monitoring library, dynamically verifies the validity of
+%the corresponding assertion. In other words, it checks that its first argument
+%(here \texttt{x == 0} or \texttt{x == 1}) is not equal to 0 and fails
+%otherwise. The extra arguments are used to display error reports as shown in
+%Section~\ref{sec:exec}.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Executing the generated code}
+%\label{sec:exec}
+%
+%Using \shortopt{ocode} \framac~\cite{userman} option, the code generated by the
+%\eacsl plug-in can be redirected into a file as follows:
+%\begin{shell}
+%\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c
+%\end{shell}
+%
+%\framac uses architecture-dependent configuration which
+%affects sizes of integer types, endianness and potentially other features. It
+%can be seen that the code generated from \texttt{first.i} (shown in the
+%previous section) defines \C type \texttt{size\_t} as \texttt{unsigned int}, whereas
+%in 64-bit architectures \texttt{size\_t} is typically defined as
+%\texttt{unsigned long}. Architecture used during \framac translation is
+%controlled through \framac \shortopt{machdep} option that specifies the
+%architecture type to use during translation. The default value of
+%\shortopt{machdep} is \texttt{x86\_32} (a generic 32-bit x86 architecture).
+%Note that since code generated by \eacsl is aimed at being compiled it is
+%important that the architecture used by \framac matches the architecture
+%corresponding to your compiler and your system. For instance, in a 64-bit
+%machine you should also pass
+%\shortopt{machdep} \texttt{x86\_64} option as follows:
+%\begin{shell}
+% \$ frama-c -machdep x86_64 -e-acsl first.i -then-last \
+% -print -ocode monitored_first.c
+%\end{shell}
+%
+%This file can be compile with a \C compiler (for instance \gcc), as follows:
+%
+%\lstset{escapechar=£}
+%\begin{shell}
+%\$ gcc -c -Wno-attributes monitored_first.c
+%\end{shell}
+%
+%However, creating an executable through a proper invokation to \gcc is painful
+%and is not documented. Instead, \eacsl comes with a companion wrapper script for
+%this purpose.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{\eacsl Wrapper Script} % <<<
+%\label{sec:wrapper}
+%
+%\begin{important}\index{Gcc}
+% Presently, \eacslgcc is a recommended way of running the \eacsl plug-in.
+% This manual further describes features of the \eacsl plug-in using \eacslgcc
+% as its main driver for source code instrumentation and compilation of the
+% instrumented programs.
+%\end{important}
+%
+%In this section we describe \eacslgcc and provide several examples of its use.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Standard Usage}
+%
+%The default behaviour of \eacslgcc is to instrument an annotated C program
+%with runtime assertions via a run of \framac.
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -omonitored_first.i first.i
+%\end{shell}
+%
+%The above command instruments \texttt{first.i} with runtime assertions and
+%outputs the generated code to \texttt{monitored\_first.i}. Unless the name of
+%the output file is specified via the \shortopt{o} option (i.e.,
+%\shortopt{-omonitored\_first.i} in the above example), the generated
+%code is placed to a file named \texttt{a.out.frama.c}.
+%
+%Compilation and Linking of the original and the instrumented sources
+%is enabled using the \shortopt{c} option. For instance, command
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -omonitored_first.i first.i
+%\end{shell}
+%
+%instruments the code in \texttt{first.i}, outputs it to
+%\texttt{monitored\_first.i} and produces 2 executables: \texttt{a.out} and
+%\texttt{a.out.e-acsl}, such that \texttt{a.out} is an executable compiled from
+%\texttt{first.i}, while \texttt{a.out.e-acsl} is an executable compiled from
+%\texttt{monitored\_first.i} generated by \eacsl.
+%
+%You can execute the generate binaries, in particular \texttt{a.out.e-acsl} which
+%detects at runtime the incorrect annotation.
+%\begin{shell}
+%\$ ./a.out.e-acsl
+%Assertion failed at line 4 in function main.
+%The failing predicate is:
+%x == 1.
+%Aborted
+%\$ echo \$?
+%134
+%\end{shell}
+%The execution aborts with a non-zero exit code (134) and an error message
+%indicating \eacsl annotation that has been violated. There is no output for the
+%valid \eacsl annotation. That is, the run of an executable generated from the
+%instrumented source file (i.e., \texttt{monitored\_first.i}) detects that the
+%second annotation in the initial program is invalid, whereas the first
+%annotation holds for this execution.
+%
+%Named executables can be created using the \shortopt{O} option. This is such
+%that a value supplied to the \shortopt{O} option is used to name the executable
+%generated from the original program and the executable generated from the
+%\eacsl-instrumented code is suffixed \texttt{.e-acsl}.
+%
+%For example, command
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
+%\end{shell}
+%names the executables generated from \texttt{first.i} and
+%\texttt{monitored\_first.i}: \texttt{monitored\_first} and
+%\texttt{monitored\_first.e-acsl} respectively.
+%
+%The \eacslgcc \shortopt{C} option allows to skip the instrumentation step and
+%compile a given program as if it was already instrumented by the \eacsl
+%plug-in. This option is useful if one makes changes to an already
+%instrumented source file by hand and only wants to recompile it.
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
+%\end{shell}
+%
+%The above command generates a single executable named
+%\texttt{monitored\_first.e-acsl}. This is because \texttt{monitored\_first.i} is
+%considered to be instrumented code and thus no original program is provided.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Customising \framac and \gcc Invocations}
+%
+%By default \eacslgcc uses \T{frama-c} and \T{gcc} executables by looking them
+%up in a system's path. If either of the tools are not found the script fails
+%with an appropriate error message. Paths to \framac and \gcc executables can
+%also be passed using \shortopt{I} and \shortopt{G} options
+%respectively, for instance as follows:
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
+%\end{shell}
+%
+%Runs of \framac and \gcc issued by \eacslgcc can further be customized by using
+%additional flags. \framac flags can be passed using the \shortopt{F} option,
+%while \shortopt{l} and \shortopt{e} options allow for passing additional
+%pre-processor and linker flags during \gcc invocations. For example, command
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
+%\end{shell}
+%
+%yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
+%are output using the UTF-8 character set. Further, during the compilation of
+%\texttt{a.out.frama.c} \gcc adds directories \texttt{/bar} and
+%\texttt{/baz} to the list of directories to be searched for header files.
+%
+%It is worth mentioning that \eacslgcc implements several convenience flags for
+%setting some of the \framac options. For instance, \shortopt{E} can be used to
+%pass additional arguments to the \framac pre-processor (see
+%Section~\ref{sec:eacsl-gcc:doc}).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Verbosity Levels and Output Redirection}
+%
+%By default \eacslgcc prints the executed \framac and \gcc commands and pipes
+%their output to the terminal. The verbosity of \framac output can be changed
+%using \shortopt{v} and \shortopt{d} options used to pass values to
+%\shortopt{verbose} and \shortopt{debug} flags of \framac respectively. For
+%instance, to increase the verbosity of plug-ins but suppress the verbosity of
+%the \framac kernel while instrumenting \texttt{foo.c} one can use the following
+%command:
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
+%\end{shell}
+%
+%Verbosity of the \eacslgcc output can also be reduced using the \shortopt{q}
+%option that suppresses any output except errors or warnings issued by \gcc,
+%\framac, and \eacslgcc itself.
+%
+%The output of \eacslgcc can also be redirected to a specified file using the
+%\shortopt{s} option. For example, the following command redirects all
+%output during instrumentation and compilation of \texttt{foo.c} to the
+%file named \texttt{/tmp/log}.
+%
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Architecture Dependency}
+%
+%As pointed out in Section~\ref{sec:exec} the execution of a \C program depends
+%on the underlying machine architecture it is executed on. The program must be
+%compiled on the very same architecture (or cross-compiled for it) for the
+%compiler being able to generate a correct binary.
+%
+%\framac makes assumptions about the machine architecture when analyzing source
+%code. By default, it assumes an X86 32-bit platform, but it can be customized
+%through \shortopt{machdep} switch~\cite{userman}. This option is of primary
+%importance when using the \eacsl plug-in: it must be set to the value
+%corresponding to the machine architecture which the generated code will be
+%executed on, otherwise the generated program is likely to fail to link against
+%the \eacsl library. Note that the library is built using the default
+%machine architecture.
+%
+%One of the benefits of using the wrapper script is that it makes sure that
+%\framac is invoked with the correct \shortopt{machdep} option. By default
+%\eacslgcc uses \shortopt{machdep gcc\_x86\_64} for 64-bit architectures and
+%\shortopt{machdep gcc\_x86\_32} for 32-bit ones. Compiler invocations are
+%further passed \shortopt{m64} or \shortopt{m32} options to generate code using
+%64-bit or 32-bit ABI respectively.
+%
+%At the present stage of implementation \eacsl does not support generating
+%executables with ABI different to the default one.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\subsection{Documentation}\label{sec:eacsl-gcc:doc}
+%
+%For full up-to-date documentation of \eacslgcc see its man page:
+%
+%\begin{shell}
+% \$ man e-acsl-gcc.sh
+%\end{shell}
+%
+%Alternatively, you can also use the \shortopt{h} option of \eacslgcc:
+%
+%\begin{shell}
+% \$ man e-acsl-gcc.sh -h
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Execution Environment of the Generated Code} %<<<
+%\label{sec:exec-env}
+%
+%The environment in which the code is executed is not necessarily the same as
+%the one assumed by \framac. You should take care of that when running the \eacsl
+%plug-in and when compiling the generated code with \gcc. In this aspect, the
+%plug-in offers a few possibilities of customization.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Runtime Errors in Annotations}
+%\label{sec:runtime-error}
+%\index{Runtime Error}
+%
+%The major difference between \acsl~\cite{acsl} and \eacsl~\cite{eacsl}
+%specification languages is that the logic is total in the former while it is
+%partial in the latter one: the semantics of a logic construct $c$ denoting a \C
+%expression $e$
+%is undefined if $e$ leads to a runtime error and, consequently, the semantics of
+%any term $t$ (resp. predicate $p$) containing such a construct $c$ is
+%undefined as soon as $e$ has to be evaluated in order to evaluate $t$
+%(resp. $p$). The \eacsl Reference Manual also states that \emph{``it is the
+%responsibility of each tool which interprets \eacsl to ensure that an
+%undefined term is never evaluated''}~\cite{eacsl}.
+%
+%Accordingly, the \eacsl plug-in prevents an undefined term from being
+%evaluated. If an annotation contains such a term, \eacsl will report a proper
+%error at runtime instead of evaluating it.
+%
+%Consider for instance the following annotated program.
+%
+%\listingname{rte.i}
+%\cinput{examples/rte.i}
+%
+%The terms and predicates containing the modulo `\%' in the \T{assumes} clause
+%are undefined in the context of the \T{main} function call since the second
+%argument is equal to 0. However, we can generate an instrumented code and
+%compile it using the following command:
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c -omonitored_rte.i -Orte rte.i
+%\end{shell}
+%
+%Now, when \T{rte.e-acsl} is executed, you get the following output indicating
+%that your function contract is invalid because it contains a division by zero.
+%
+%\begin{shell}
+%\$ ./rte.e-acsl
+%RTE failed at line 5 in function is_dividable.
+%The failing predicate is:
+%division_by_zero: y != 0.
+%Aborted
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Libc}\index{Libc}
+%
+%By default, \framac uses its own standard library (\emph{aka} libc) instead of
+%the one of your system. If you do not want to use it, you have to add the option
+%\shortopt{no-framac-stdlib}\optionidx{-}{framac-stdlib} to the \framac command
+%line.
+%
+%It might be particularly useful in one of the following contexts:
+%\begin{itemize}
+%\item several libc functions used by the analyzed program are still not defined
+% in the \framac libc; or
+%\item your system libc and the \framac libc mismatch about several function
+% types (for instance, your system libc is not 100\% POSIX compliant); or
+%\item several \framac lib functions get a contract and you are not interested in
+% verifying them (for instance, only checking undefine behaviors matters).
+%\end{itemize}
+%
+%\begin{important} \index{eacslgcc}
+%Notably, \eacslgcc disables \framac libc by default. This is because most of
+%its functions are annotated with \eacsl contracts and generating code for
+%these contracts results in additional runtime overheads. To enforce default
+%\framac contracts with \eacslgcc you can pass \shortopt{L} option to the wrapper
+%script.
+%\end{important}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Integers}
+%\label{sec:integers}
+%\index{GMP}
+%
+%\eacsl uses an \texttt{integer}\codeidx{integer} type corresponding to
+%mathematical integers which does not fit in any integral \C type. To circumvent
+%this issue, \eacsl uses the \gmp library\footnote{\url{http://gmplib.org}}.
+%Thus, even if \eacsl does its best to use standard integral types instead of
+%\gmp~\cite{sac13,jfla15}, it may generate such integers from time to time. It is
+%notably the case if your program contains \lstinline|long long|, either signed
+%or unsigned.
+%
+%Consider for instance the following program.
+%
+%\listingname{gmp.i}
+%\cinput{examples/gmp.i}
+%
+%Even on a 64-bit machine, it is not possible to compute the assertion with a
+%standard \C type. In this case, the \eacsl plug-in generates \gmp code. Note
+%that E-ACSL library already includes \gmp, thus no additional arguments need to
+%be provided. We can generate and execute the instrumented code as usual via
+%the following command:
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -omonitored_gmp.i -Ogmp gmp.i
+%\$ ./gmp.e-acsl
+%\end{shell}
+%
+%Since the assertion is valid, there is no output in this case.
+%
+%Note that it is possible to use \gmp arithmetic in all cases (even if not
+%required). This option is controlled through \shortopt{g} switch of \eacslgcc
+%which passes the \shortopt{e-acsl-gmp-only} option to the \eacsl
+%plug-in. However it could slow down the execution of the instrumented program
+%significantly.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Memory-related Annotations}
+%\label{sec:memory}
+%
+%The \eacsl plug-in handles memory-related annotations such as
+%\lstinline|\valid|. Consider for instance the following program.
+%
+%\listingname{valid.c}
+%\cinput{examples/valid.c}
+%
+%Even though the first annotation holds, the second annotation (labelled
+%\I{freed}) is invalid. This is because at the point of its execution memory
+%allocated via \texttt{malloc} has been deallocated and \T{x} is a stale pointer
+%referencing unallocated memory. The execution of the instrumented program thus
+%reports the violation of the second annotation:
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c -Ovalid valid.c
+%\$ ./valid.e-acsl
+%Assertion failed at line 11 in function main.
+%The failing predicate is:
+%freed: \valid(x).
+%Aborted
+%\end{shell}
+%
+%To check memory-related predicates (such as \lstinline|\valid|) \eacsl tracks
+%memory allocated by a program at runtime. \eacsl records memory blocks in a
+%meta-storage tracking each block's boundaries (i.e., its base address and
+%length), per-byte initialization and the notion of an address being freeable
+%(i.e., whether it can be safely passed to the \texttt{free} function). During
+%an execution of the instrumented program code injected by \eacsl
+%transformations queries the meta-storage to identify properties of an address
+%in question. For instance, during the execution of the above program the
+%monitor injected by \eacsl first records information about the memory block
+%allocated via a call to \texttt{malloc}. Further, during the execution of the
+%first assertion the monitor queries the meta-storage about the address of the
+%memory location pointed to by \texttt{x}. Since the location belongs to an
+%allocated memory block, the meta-storage identifies it as belonging to the
+%tracked allocation. Consequently, the assertion evaluates to true and the
+%monitors allows the execution to continue. The second assertion, however,
+%fails. This is because the block pointed to by \T{x} has been removed from the
+%meta-storage by a call to \T{free}, and thus a meta-storage query identifies
+%location \T{x} as belonging unallocated memory space.
+%
+%\subsubsection{\eacsl Memory Models}
+%
+%Memory tracking implemented by the \eacsl library comes in two flavours dubbed
+%\I{bittree-based} and \I{segment-based} memory models. With the bittree-based
+%model meta-storage is implemented as a compact prefix trie called Patricia
+%trie~\cite{rv13}, whereas segment-based memory model
+%\footnote{Segment-based model of \eacsl has not yet appeared in the literature.}
+%is based on shadow memory~\cite{pldi16}. The functionality of the provided
+%memory models is equivalent, however they differ in performance. We further
+%discuss performance considerations.
+%
+%The \eacsl models allocate heap memory using a customized version of the
+%\dlmalloc\footnote{\url{http://dlmalloc.net/}} memory allocator replacing
+%system-wide \T{malloc} and similar functions (e.g., \T{calloc} or \T{free}).
+%
+%At the level of \eacslgcc you can choose between different memory models using
+%the \shortopt{m} switch followed by the name of the memory model to link
+%against. For instance, command
+%\begin{shell}
+%\$ e-acsl-gcc.sh -mbittree -c -Ovalid valid.c
+%\end{shell}
+%links a program generated from \T{valid.c} against the library implementing the
+%bittree-based memory model, whereas the following invocation uses shadow-based
+%tracking:
+%\begin{shell}
+%\$ e-acsl-gcc.sh -msegment -c -Ovalid valid.c
+%\end{shell}
+%It is also possible to generate executables using both models as follows:
+%\begin{shell}
+%\$ e-acsl-gcc.sh -msegment,bittree -c -Ovalid valid.c
+%\end{shell}
+%In this case, \eacslgcc produces 3 executables: \T{valid},
+%\T{valid.e-acsl-segment} and \T{valid.e-acsl-bittree} corresponding to an
+%executable generated from the original source code, and the executables
+%generated from the \eacsl-instrumented sources linked against
+%segment-based and bittree-based memory models.
+%
+%Unless specified, \eacsl defaults to the segment-based memory model.
+%
+%\subsubsection{Performance Considerations}
+%\label{sec:perf}
+%
+%As pointed out in the previous section the functionalities provided by both
+%segment-based and bittree-based memory models are equivalent but differ in
+%performance. The bittree-based model uses compact memory representation of
+%metadata. The segment-based model on the other hand uses significantly more
+%memory. You can expect over 2x times memory overheads when using it. However It
+%is often an order of magnitude faster than the bittree-based
+%model~\cite{pldi16}.
+%
+%%[Need ref here with comparison of the performance. Ideally a reference to the PLDI paper].
+%
+%\subsubsection{Maximized Memory Tracking}
+%
+%By default \eacsl uses static analysis to reduce instrumentation and therefore
+%runtime and memory overheads~\cite{scp16}. With respect to memory tracking this
+%means that
+%\eacsl may omit recording memory blocks irrelevant for runtime analysis. It
+%is, however, still possible to systematically instrument the code for handling
+%potential memory-related annotations even when it is not required. This
+%feature can be enabled using the \shortopt{M} switch of \eacslgcc or
+%\shortopt{e-acsl-full-mmodel} option of the \eacsl plug-in.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% \subsection{Debug Libraries}
+%%% \label{sec:runtime-debug}
+%
+%%% \eacsl memory models mentioned in Section~\ref{sec:memory} are optimized for
+%%% performance (via \shortopt{-O2} compiler flag). An \eacsl installation also
+%%% provides unoptimized versions of these libraries (suffixed \T{-dbg.a}) aimed at
+%%% being used during debugging.
+%
+%%% The main difference between unoptimized (debug) and optimized (production)
+%%% libraries is that debug libraries include assertions validating the correctness
+%%% of the RTL itself. For instance, during memory tracking such assertions ensure
+%%% that during a run of a program all tracked memory blocks are disjoint.
+%
+%%% Consider the following program that violates an annotation
+%%% in function \T{foo} via a call \T{bar(p+1)} in the main function:
+%
+%%% \listingname{rte\_debug.i}
+%%% \cinput{examples/rte_debug.i}
+%
+%%% A monitored executable linked against a debug version of \eacsl RTL
+%%% can ge generated using
+%%% \longopt{rt-debug} flag of \eacslgcc as follows:
+%
+%%% \begin{shell}
+%%% \$ e-acsl-gcc.sh --rt-debug -c -omonitored_rte_debug.c -Orte_debug rte_debug.i
+%%% \end{shell}
+%
+%%% A run of the monitored executable shows violation of the \eacsl annotation.
+%%% \begin{shell}
+%%% \$ rte_debug.e-acsl
+%%% Assertion failed at line 2 in function foo.
+%%% The failing predicate is:
+%%% \valid(p).
+%%% /** Backtrace **************************/
+%%% trace at e_acsl_trace.h:45
+%%% - exec_abort at e_acsl_assert.h:58
+%%% - runtime_assert at e_acsl_assert.h:93
+%%% - foo at monitored_rte_debug.c:92
+%%% - bar at monitored_rte_debug.c:102
+%%% - main at monitored_rte_debug.c:119
+%%% /***************************************/
+%%% Aborted
+%%% \end{shell}
+%
+%%% A run of an executable linked against an unoptimized RTL shows a stack trace on
+%%% the instrumented program saved to \T{monitored\_rte\_debug.c}. In the example
+%%% above calls to \T{exec\_abort} and \T{runtime\_assert} belong to the \eacsl
+%%% RTL, whereas calls to \T{foo}, \T{bar} and \T{main} belong to the input
+%%% program.
+%
+%%% It should be noted that because debug versions of \eacsl RTL are compiled
+%%% without compile-time optimizations and execute additional assertions the
+%%% runtime overheads of the instrumented programs linked against the debug
+%%% versions of \eacsl RTL can be up to 10 times greater than those linked against
+%%% the production versions.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Runtime Monitor Behavior}
+%
+%When a predicate is checked at runtime function
+%\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} is called. By
+%default this function does nothing if the predicate is valid, and prints
+%an error message and aborts the execution (by raising an \texttt{ABORT}
+%signal via a call to the \C function \texttt{abort}) if the predicate is invalid.
+%
+%The default behavior of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
+%can be altered using \longopt{fail-with-code=CODE} option of \eacslgcc
+%that uses \texttt{exit(CODE)} instead of \texttt{abort}.
+%
+%For instance, the program generated using the following command
+%exits with code \texttt{5} on a predicate violation.
+%\begin{shell}
+% \$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
+%\end{shell}
+%
+%Forceful termination of a monitored program can be disabled using
+%\longopt{keep-going} option. If specified, \eacslgcc generates code that
+%reports each property violated at runtime but allows the monitored program to
+%continue execution. \longopt{keep-going} should be used with caution:
+%such unterminated executions may lead to incorrect verification results.
+%
+%\eacslgcc also provides a way to use an alternative definition of
+%\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}.
+%
+%Custom implementation of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
+%should be provided in a separate \C (or object file) and respect the
+%following signature:
+%
+%\cinput{examples/assert_sign.c}
+%
+%Below is an example which prints the validity status of each property but never
+%exits.
+%
+%\listingname{my\_assert.c}
+%\cinput{examples/my_assert.c}
+%
+%A monitored program that uses custom definition of
+%\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} can then be generated
+%as follows using \longopt{external-assert} option of \eacslgcc to replace the
+%default implementation of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
+%with the customized one specified in \texttt{my\_assert.c}
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c first.i my_assert.c -Ofirst --external-assert=my\_assert.c
+%\$ ./first.e-acsl
+%Assertion at line 3 in function main is valid.
+%The verified predicate was: `x == 0'.
+%Assertion at line 4 in function main is invalid.
+%The verified predicate was: `x == 1'.
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Additional Verifications} % <<<
+%
+%In addition to checking annotations at runtime, \eacsl is able to detect a few
+%errors at runtime.
+%
+%\subsection{Format String Vulnerabilities}
+%\index{Format String Vulnerabilities}
+%
+%Whenever option \longopt{validate-format-strings} of \eacslgcc is set, \eacsl
+%detects format-string vulnerabilities in \texttt{printf}-like function. Below is
+%an example which incorrectly tries to print a string through a \texttt{\%d}
+%format.
+%
+%\listingname{printf.c}
+%\cinput{examples/printf.c}
+%
+%This error can be detected by \eacsl as follows.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings printf.c
+%\$ ./printf.e-acsl
+%printf: directive 1 ('%d') expects argument of type 'int' but the corresponding
+%argument has type 'char*'
+%Abort
+%\end{shell}
+%
+%\subsection{Incorrect Usage of Libc Functions}
+%\index{Libc}
+%
+%Whenever option \longopt{libc-replacements} of \eacslgcc is set, \eacsl is
+%able to detect incorrect usage of the following libc functions:
+%\begin{itemize}
+%\item \texttt{memcmp}
+%\item \texttt{memcpy}
+%\item \texttt{memmove}
+%\item \texttt{memset}
+%\item \texttt{strcat}
+%\item \texttt{strncat}
+%\item \texttt{strcmp}
+%\item \texttt{strcpy}
+%\item \texttt{strncpy}
+%\item \texttt{strlen}
+%\end{itemize}
+%
+%For instance, the program below incorrectly uses \texttt{strcpy} because the
+%destination string should contain at least 7 \texttt{char} (and not only 6).
+%
+%\listingname{strcpy.c}
+%\cinput{examples/strcpy.c}
+%
+%This error can be reported by \eacsl as follows.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -Ostrcpy -c --libc-replacements strcpy.c
+%\$ ./strcpy.e-acsl
+%strlen: insufficient space in destination string, at least 7 bytes required
+%Abort
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Incomplete Programs} % <<<
+%\label{sec:incomplete}
+%
+%Executing a \C program requires to have a complete application. However, the
+%\eacsl plug-in does not necessarily require to have it to generate the
+%instrumented code. It is still possible to instrument a partial program with no
+%entry point or in which some functions remain undefined.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Programs without Main}
+%\label{sec:no-main}
+%\index{Program!Without main}
+%
+%The \eacsl plug-in can instrument a program without the \T{main} function.
+%Consider for instance the following annotated program without \texttt{main}.
+%
+%\listingname{no\_main.i}
+%\cinput{examples/no_main.i}
+%
+%The instrumented code is generated as usual, even though you get an additional
+%warning.
+%\begin{shell}
+%\$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
+%<skip preprocessing command line>
+%[e-acsl] beginning translation.
+%[e-acsl] warning: cannot find entry point `main'.
+% Please use option `-main' for specifying a valid entry point.
+% The generated program may miss memory instrumentation.
+% if there are memory-related annotations.
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%This warning indicates that the instrumentation could be incorrect if the
+%program contains memory-related annotations (see
+%Section~\ref{sec:limits:no-main}). That is not the case here, so you can
+%safely ignore it. Now, it is possible to compile the generated code with a \C
+%compiler in a standard way, and even link it against additional files such as
+%the following:
+%
+%\listingname{main.c}
+%\cinput{examples/main.c}
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -C monitored_no_main.i main.c -Owith_main
+%\$ ./with_main.e-acsl
+%x = 65536
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\
+%\subsection{Undefined Functions}
+%\label{sec:no-code}
+%\index{Function!Undefined}
+%
+%Similar to the above section \eacsl is capable of instrumenting a program which
+%has definitions of arbitrary functions missing. Consider for instance the
+%following annotated program for which the implementation of the function
+%\texttt{my\_pow} is not provided.
+%
+%\listingname{no\_code.c}
+%\cinput{examples/no_code.c}
+%
+%The instrumented code is generated as usual, even though you get an additional
+%warning.
+%\begin{shell}
+%\$ e-acsl-gcc.sh -omonitored_no_code.i no_code.c
+%[e-acsl] beginning translation.
+%[e-acsl] warning: annotating undefined function `my_pow':
+% the generated program may miss memory instrumentation
+% if there are memory-related annotations.
+%no_code.c:9:[kernel] warning: No code nor implicit assigns clause for function my_pow,
+%generating default assigns from the prototype
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%Similar to the previous Section the warning indicates that the instrumentation
+%could be incorrect if the program contains memory-related annotations (see
+%Section~\ref{sec:limits:no-code}). That is still not the case here, so you can
+%safely ignore it.
+%
+%\listingname{pow.i}
+%\cinput{examples/pow.i}
+%
+%Similar to the example shown in the previous section you can generate the
+%executable by providing definition of \T{my\_pow}.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i
+%\$ ./no_code.e-acsl
+%Postcondition failed at line 5 in function my_pow.
+%The failing predicate is:
+%\old(n % 2 == 0) ==> \result >= 1.
+%Aborted
+%\end{shell}
+%
+%The execution of the corresponding binary fails at runtime: actually, our
+%implementation of the function \texttt{my\_pow} overflows in case of large
+%exponentiations.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Combining E-ACSL with Other Plug-ins} % <<<
+%\label{sec:combine}
+%
+%As the \eacsl plug-in generates a new \framac project, it is easy to run any
+%plug-in on the generated program, either in the same \framac session (thanks to
+%the option \shortopt{then} or through the GUI), or in another one. The only
+%issue might be that, depending on the plug-in, the analysis may be imperfect if
+%the generated program uses \gmp or the dedicated memory library: both make
+%intensive use of dynamic structures which are usually difficult to handle by
+%analysis tools.
+%
+%Another way to combine \eacsl with other plug-ins is to run \eacsl last. For
+%instance, the \rte plug-in~\cite{rte} may be used to generate annotations
+%corresponding to runtime errors. Then the \eacsl plug-in may generate an
+%instrumented program to verify that there are no such runtime errors during the
+%execution of the program.
+%
+%Consider the following program.
+%
+%\listingname{combine.i}
+%\cinput{examples/combine.i}
+%To check at runtime that this program does not perform any runtime error (which
+%are potential overflows in this case), just do:
+%
+%\begin{shell}
+%\$ frama-c -rte combine.i -then -e-acsl -then-last -print
+% -ocode monitored_combine.i
+%\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.i
+%\$ ./combine.
+%\end{shell}
+%
+%Automatic assertion generation can also be enabled via \eacslgcc directly via
+%the following command:
+%\begin{shell}
+%\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all
+%\end{shell}
+%
+%Note the use of \eacslgcc \longopt{rte} option which asks \framac to combine
+%\eacsl with \rte plug-in. This plug-in automatically instruments the input
+%program with runtime
+%assertions before running the \eacsl plug-in on it. \longopt{rte} option of
+%\eacslgcc also accepts a comma-separated list of arguments indicating the types
+%of assertions to generate. Consult the \eacslgcc man page for a detailed
+%list of arguments accepted by \longopt{rte}.
+%
+%The present implementation of \eacslgcc does not fully support combining \eacsl
+%with other \framac plug-ins. However it is still possible to instrument programs
+%with \eacsl directly and use \eacslgcc to compile the generated code.
+%
+%If you run the \eacsl plug-in after another one, it first generates
+%a new temporary project in which it links the analyzed program against its own
+%library in order to generate the \framac internal representation of the \C
+%program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
+%even if the \eacsl plug-in keeps the maximum amount of information, the results
+%of already executed analyzers (such as validity status of annotations) are not
+%known in this new project. If you want to keep them, you have to set the option
+%\shortopt{e-acsl-prepare} when the first analysis is asked for.
+%
+%In this context, the \eacsl plug-in does not generate code for annotations
+%proven valid by another plug-in, except if you explicitly set the option
+%\shortopt{e-acsl-valid}. For instance, \Eva~\cite{eva} is able to
+%prove that there is no potential overflow in the previous program, so the \eacsl
+%plug-in does not generate additional code for checking them if you run the
+%following command.
+%\begin{shell}
+%\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+% -then-last -print -ocode monitored_combine.i
+%\end{shell}
+%The additional code will be generated with one of the two following commands.
+%\begin{shell}
+%\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+% -e-acsl-valid -then-last -print -ocode monitored_combine.i
+%\$ frama-c -rte combine.i -then -val -then -e-acsl \
+% -then-last -print -ocode monitored_combine.i
+%\end{shell}
+%In the first case, that is because it is explicitly required by the option
+%\shortopt{e-acsl-valid} while, in the second case, that is because the option
+%\shortopt{e-acsl-prepare} is not provided on the command line which results in
+%the fact that the result of the value analysis are unknown when the \eacsl
+%plug-in is running.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Customization} % <<<
+%\label{sec:custom}
+%
+%There are several ways to customize the \eacsl plug-in.
+%
+%First, the name of the generated project -- which is \texttt{e-acsl} by default
+%-- may be changed by setting the option \shortopt{e-acsl-project} option of the
+%\eacsl plug-in. While there is not direct support for this option in \eacslgcc
+%you can pass it using \shortopt{F} switch:
+%
+%\listingname{check.i}
+%\cinput{examples/check.i}
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i
+%<skip preprocessing commands>
+%[e-acsl] beginning translation.
+%check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
+% Ignoring annotation.
+%[e-acsl] translation done in project "foobar".
+%\end{shell}
+%
+%Further, the \eacsl plug-in option \shortopt{e-acsl-check} does not generate a
+%new project but verifies that each annotation is translatable. Then it produces
+%a summary as shown in the following example (left or right shifts in annotations
+%are not yet supported by the \eacsl plug-in~\cite{eacsl-implem}).
+%
+%\begin{shell}
+%\$ frama-c -e-acsl-check check.i
+%<skip preprocessing commands>
+%check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
+% Ignoring annotation.
+%[e-acsl] 0 annotation was ignored, being untypable.
+%[e-acsl] 1 annotation was ignored, being unsupported.
+%\end{shell}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+%\section{Verbosity Policy} % <<<
+%\label{sec:verbose}
+%
+%By default, \eacsl does not provide much information when it is running. Mainly,
+%it prints a message when it begins the translation, and another one when the
+%translation is done. It may also display warnings when something requires the
+%attention of the user, for instance if it is not able to translate an
+%annotation. Such information is usually enough but, in some cases, you might
+%want to get additional control on what is displayed. As quite usual with
+%\framac plug-ins, \eacsl offers two different ways to do this: the verbosity
+%level which indicates the \emph{amount} of information to display, and the
+%message categories which indicate the \emph{kind} of information to display.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Verbosity Level}
+%
+%The amount of information displayed by the \eacsl plug-in is settable by the
+%option \shortopt{e-acsl-verbose}. It is 1 by default. Below is indicated
+%which information is displayed according to the verbosing level. The level $n$
+%also displays the information of all the lower levels.
+%
+%\begin{center}
+%\begin{tabular}{|l|l|}
+%\hline
+%\shortopt{e-acsl-verbose 0}& only warnings and errors\\
+%\hline
+%\shortopt{e-acsl-verbose 1}& beginning and ending of the translation\\
+%\hline
+%\shortopt{e-acsl-verbose 2}& different parts of the translation and
+% functions-related information\\
+%\hline
+%\shortopt{e-acsl-verbose 3}& predicates- and statements-related information\\
+%\hline
+%\shortopt{e-acsl-verbose 4}& terms- and expressions-related information
+%\\
+%\hline
+%\end{tabular}
+%\end{center}
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+%\subsection{Message Categories}
+%
+%The kind of information to display is settable by the option
+%\shortopt{e-acsl-msg-key} (and unsettable by the option
+%\shortopt{e-acsl-msg-key-unset}). The different keys refer to different
+%parts of the translation, as detailed below.
+%
+%\begin{center}
+%\begin{tabular}{|l|l|}
+%\hline
+%analysis & minimization of the instrumentation for memory-related annotation
+%(section~\ref{sec:memory}) \\
+%\hline
+%duplication & duplication of functions with contracts
+%(section~\ref{sec:no-code}) \\
+%\hline
+%translation & translation of an annotation into \C code\\
+%\hline
+%typing & minimization of the instrumentation for integers
+%(section~\ref{sec:integers}) \\
+%\hline
+%\end{tabular}
+%\end{center}
+% >>>
diff --git a/doc/userman/eacslversion.tex b/doc/userman/eacslversion.tex
new file mode 100644
index 0000000000000000000000000000000000000000..921e0d99cef3b2c72913f553471f5ec89617206e
--- /dev/null
+++ b/doc/userman/eacslversion.tex
@@ -0,0 +1,2 @@
+\newcommand{\eacslversion}{Chlorine-20180501+dev\xspace}
+\newcommand{\fcversion}{Chlorine\xspace}
diff --git a/doc/userman/fclangversion.tex b/doc/userman/fclangversion.tex
new file mode 100644
index 0000000000000000000000000000000000000000..b542d4126cab709a71bfa1934a8ecb8c0c3fa335
--- /dev/null
+++ b/doc/userman/fclangversion.tex
@@ -0,0 +1,2 @@
+\newcommand{\fclangversion}{Chlorine+\xspace}
+\newcommand{\fcversion}{Chlorine+\xspace}
diff --git a/doc/userman/introduction.tex b/doc/userman/introduction.tex
new file mode 100644
index 0000000000000000000000000000000000000000..809a738bcb14a39382a74bf00cb90a1166a51777
--- /dev/null
+++ b/doc/userman/introduction.tex
@@ -0,0 +1,26 @@
+\chapter{Introduction}
+
+\framac~\cite{userman,fac15} is a modular analysis framework for the C
+programming language which supports the \acsl specification
+language~\cite{acsl}. This manual documents the \fclang plug-in of \framac,
+version \fclangversion.
+The \fclang plug-in supports the \acslpp extension of \acsl for C++ programs and specifications;
+it is built on the Clang\footnote{https://clang.llvm.org/} compiler infrastructure and uses Clang for
+parsing C++.
+
+%The \fclang version you are using is indicated by the
+%command \texttt{frama-c -e-acsl-version}\optionidx{-}{e-acsl-version}. \fclang
+%automatically translates an annotated C program into another program that fails
+%at runtime if an annotation is violated. If no annotation is violated, the
+%behavior of the new program is exactly the same as the one of the original
+%program.
+
+
+%This manual does \emph{not} explain how to install the \eacsl plug-in. For
+%installation instructions please refer to the \texttt{INSTALL} file in the
+%\eacsl distribution. \index{Installation} Furthermore, even though this manual
+%provides examples, it is \emph{not} a full comprehensive tutorial on
+%\framac or \eacsl.
+
+% You can still refer to any external
+% tutorial~\cite{rv13tutorial} for additional examples.
diff --git a/doc/userman/limitations.tex b/doc/userman/limitations.tex
new file mode 100644
index 0000000000000000000000000000000000000000..29097433073d54da1faec70044a77d65c5f2aea8
--- /dev/null
+++ b/doc/userman/limitations.tex
@@ -0,0 +1,188 @@
+\chapter{Known Limitations}
+
+The development of the \fclang plug-in is still ongoing.
+%First, the \eacsl
+%reference manual~\cite{eacsl} is not yet fully supported. Which annotations can
+%already be translated into \C code and which cannot is defined in a separate
+%document~\cite{eacsl-implem}. Second, even though we do our best to avoid them,
+%bugs may exist. If you find a new one, please report it on the bug tracking
+%system\footnote{\url{http://bts.frama-c.com}} (see Chapter 10 of the \framac
+%User Manual~\cite{userman}). Third, there
+%are some additional known limitations, which could be annoying for the user in
+%some cases, but are tedious to lift. Please contact us if you are interested in
+%lifting these limitations\footnote{Read \url{http://frama-c.com/support.html}
+% for additional details.}.
+
+%\section{Uninitialized Values}
+%\index{Uninitialized value}
+%
+%As explained in Section~\ref{sec:runtime-error}, the \eacsl plug-in should never
+%translate an annotation into \C code which can lead to a runtime error. This is
+%enforced, except for uninitialized values which are values read before having
+%been written.
+%
+%\listingname{uninitialized.i}
+%\cinput{examples/uninitialized.i}
+%
+%If you generate the instrumented code, compile it, and finally execute it, you
+%may get no runtime error depending on your \C compiler, but the behavior is
+%actually undefined because the assertion reads the uninitialized variable
+%\lstinline|x|. You should be caught by the \eacsl plug-in, but that is not
+%the case yet.
+%\begin{shell}
+%
+%\$ e-acsl-gcc.sh uninitialized.i -c -Omonitored_uninitialized
+%monitored_uninitialized.i: In function 'main':
+%monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function
+%[-Wuninitialized]
+%\$ ./monitored_uninitialized.e-acsl
+%\end{shell}
+%
+%This is more a design choice than a limitation: should the \eacsl plug-in
+%generate additional instrumentation to prevent such values from being evaluated,
+%the generated code would be much more verbose and slower.
+%
+%If you really want to track such uninitializations in your annotation, you have
+%to manually add calls to the \eacsl predicate
+%\lstinline|\initialized|~\cite{eacsl}.
+%
+%\section{Incomplete Programs}
+%
+%Section~\ref{sec:incomplete} explains how the \eacsl plug-in is able to handle
+%incomplete programs, which are either programs without main, or programs
+%containing undefined functions (\emph{i.e.} functions without body).
+%
+%However, if such programs contain memory-related annotations, the generated code
+%may be incorrect. That is made explicit by a warning displayed when the \eacsl
+%plug-in is running (see examples of Sections~\ref{sec:no-main} and
+%\ref{sec:no-code}).
+%
+%\subsection{Programs without Main}
+%\index{Program!Without main}
+%\label{sec:limits:no-main}
+%
+%The instrumentation in the generated program is partial for every program
+%without main containing memory-related annotations, except if the option
+%\optionuse{-}{e-acsl-full-mmodel} or the \eacsl plug-in (of \shortopt{M} option
+%of \eacslgcc) is provided. In that case, violations of such annotations are
+%undetected.
+%
+%Consider the following example.
+%
+%\listingname{valid\_no\_main.c}
+%\cinput{examples/valid_no_main.c}
+%
+%You can generate the instrumented program as follows.
+%\begin{shell}
+%\$ e-acsl-gcc.sh -ML -omonitored_valid_no_main.i valid_no_main.c
+%<skip preprocessing commands>
+%[e-acsl] beginning translation.
+%<skip warnings about annotations from the Frama-C libc
+% which cannot be translated>
+%[kernel] warning: no entry point specified:
+% you must call function `__e_acsl_memory_init' by yourself.
+%[e-acsl] translation done in project "e-acsl".
+%\end{shell}
+%
+%The last warning states an important point: if this program is linked against
+%another file containing \texttt{main} function, then this main function must
+%be modified to insert a call to the function \texttt{\_\_e\_acsl\_memory\_init}
+%\index{e\_acsl\_memory\_init@\texttt{\_\_e\_acsl\_memory\_init}} at the very
+%beginning. This function plays a very important role: it initializes metadata
+%storage used for tracking of memory blocks. Unless this call is inserted the
+%run of a modified program is likely to fail.
+%
+%While it is possible to add such intrumentation manually we recommend using
+%\eacslgcc. Consider the following incomplete program containing \T{main}:
+%
+%\listingname{modified\_main.c}
+%\cinput{examples/modified_main.c}
+%
+%Then just compile and run it as explained in Section~\ref{sec:memory}.
+%
+%\begin{shell}
+%\$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
+%\$ e-acsl-gcc.sh -C -Ovalid_no_main monitored_modified_main.i monitored_valid_no_main.i
+%\$ ./valid_no_main.e-acsl
+%Assertion failed at line 11 in function f.
+%The failing predicate is:
+%freed: \valid(x).
+%Aborted
+%\end{shell}
+%
+%Also, if the unprovided main initializes some variables, running the
+%instrumented code (linked against this main) could print some warnings from the
+%\eacsl memory library\footnote{see
+% \url{https://bts.frama-c.com/view.php?id=1696} for an example}.
+%
+%\subsection{Undefined Functions}
+%\label{sec:limits:no-code}
+%\index{Function!Undefined}
+%
+%The instrumentation in the generated program is partial for a program $p$ if and
+%only if $p$ contains a memory-related annotation $a$ and an undefined function
+%$f$ such that:
+%\begin{itemize}
+%\item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
+%\item or $a$ is one of the post-conditions of $f$.
+%\end{itemize}
+%A violation of such an annotation $a$ is undetected. There is no workaround yet.
+%
+%Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
+%undefined functions. There is also no workaround yet.
+%
+%\section{Recursive Function}
+%\index{Function!Recursive}
+%
+%Programs containing recursive functions have the same limitations as the ones
+%containing undefined functions (Section~\ref{sec:limits:no-code}) and
+%memory-related annotations.
+%
+%%% JS: this issue should have been fixed:
+%%% Also, even though there is no such annotations, the generated code may call a
+%%% function before it is declared. When this behavior appears remains
+%%% unspecifed. The generated code is however easy to fix by hand.
+%
+%\section{Variadic Functions}
+%\index{Function!Variadic}
+%
+%Programs containing undefined variadic functions with contracts
+%are not yet supported. Using the \variadic plug-in of \framac could be a
+%solution in some cases, but its generated code cannot always be compiled.
+%
+%\section{Function Pointers}
+%\index{Function!Pointer}
+%
+%Programs containing function pointers have the same limitations on
+%memory-related annotations as the ones containing undefined or recursive
+%functions.
+%
+%\section{Requirements to Input Programs}
+%\index{Function!Input}
+%
+%\subsection{\eacsl Namespace}
+%While \eacsl uses source-to-source transformations and not binary
+%instrumentations it is important that the source code provided at input does
+%not contain any variables or functions prefixed \T{\_\_e\_acsl\_}. \eacsl
+%reserves this namespace for its transformations, and therefore an input program
+%containing such symbols beforehand may fail to be instrumented or compiled.
+%
+%\subsection{Memory Management Functions}
+%Programs providing custom definitions of \T{syscall}, \T{mmap} or
+%\T{sbrk} should be rejected. Also, an input programs should not modify
+%memory-management functions namely \T{malloc}, \T{calloc}, \T{realloc},
+%\T{free}, \T{cfree}, \T{posix\_memalign} and \T{aligned\_alloc}. \eacsl relies
+%on these functions in order to track heap memory. Further, correct heap memory
+%monitoring requires to limit allocation and deallocation of heap memory to
+%POSIX-compliant memory management functions
+%listed above. Monitoring of programs that allocate memory using non-standard or
+%obsolete functions (e.g., \T{valloc}, \T{memalign}, \T{pvalloc}) may not work
+%correctly.
+%
+%\section{Limitations of E-ACSL Monitoring Libraries}
+%\index{Function!Libraries}
+%
+%\eacsl monitoring library implementing segment-based memory model is fairly
+%recent and presently has very limited support for 32-bit architectures. When
+%using a 32-bit machine we recommend using the bittree-based memory model
+%instead.
diff --git a/doc/userman/macros.tex b/doc/userman/macros.tex
new file mode 100644
index 0000000000000000000000000000000000000000..e92cba83f6bc8f418a26e41906c122a482de4a20
--- /dev/null
+++ b/doc/userman/macros.tex
@@ -0,0 +1,295 @@
+%%% 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{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
+\newcommand{\rte}{\textsc{RTE}\xspace}
+\newcommand{\C}{\textsc{C}\xspace}
+\newcommand{\jml}{\textsc{JML}\xspace}
+\newcommand{\Eva}{\textsc{Eva}\xspace}
+\newcommand{\variadic}{\textsc{Variadic}\xspace}
+\newcommand{\wpplugin}{\textsc{Wp}\xspace}
+\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
+\newcommand{\gcc}{\textsc{Gcc}\xspace}
+\newcommand{\gmp}{\textsc{GMP}\xspace}
+\newcommand{\dlmalloc}{\textsc{dlmalloc}\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}}
+
+% Index
+
+\newcommand{\optionidx}[2]{\index{#2@\texttt{#1#2}}}
+\newcommand{\codeidx}[1]{\index{#1@\texttt{#1}}}
+\newcommand{\scodeidx}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}}}
+\newcommand{\sscodeidx}[3]{%
+ \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}}}
+\newcommand{\bfit}[1]{\textbf{\textit{\hyperpage{#1}}}}
+\newcommand{\optionidxdef}[2]{\index{#2@\texttt{#1#2}|bfit}}
+\newcommand{\codeidxdef}[1]{\index{#1@\texttt{#1}|bfit}}
+\newcommand{\scodeidxdef}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}|bfit}}
+\newcommand{\sscodeidxdef}[3]{%
+ \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}|bfit}}
+
+\newcommand{\pragmadef}[1]{\texttt{#1}\index{Pragma!#1@\texttt{#1}}}
+\newcommand{\optiondef}[2]{\texttt{#1#2}\optionidxdef{#1}{#2}}
+\newcommand{\textttdef}[1]{\texttt{#1}\codeidxdef{#1}}
+
+\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
+\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
+\newcommand{\shortopt}[1]{\optionuse{-}{#1}}
+\newcommand{\longopt}[1]{\optionuse{{-}{-}}{#1}}
+% Shortcuts for truetype, italic and bold
+\newcommand{\T}[1]{\texttt{#1}}
+\newcommand{\I}[1]{\textit{#1}}
+\newcommand{\B}[1]{\textbf{#1}}
+
+\definecolor{gris}{gray}{0.85}
+\makeatletter
+\newenvironment{important}%
+{\hspace{5pt plus \linewidth minus \marginparsep}%
+ \begin{lrbox}{\@tempboxa}%
+ \begin{minipage}{\linewidth - 2\fboxsep}}
+{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
diff --git a/doc/userman/main.tex b/doc/userman/main.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5fe5621a0e5af9ff328f0415e208ece9a1a39454
--- /dev/null
+++ b/doc/userman/main.tex
@@ -0,0 +1,99 @@
+\documentclass[web]{frama-c-book}
+
+\usepackage{graphicx}
+\usepackage{calc}
+\usepackage{datetime}
+\newdateformat{ddMyyyydate}{\THEDAY~\monthname[\THEMONTH]~\THEYEAR}
+
+
+
+\include{macros}
+\newcommand{\fclang}{\textsc{Frama-Clang}\xspace}
+\newcommand{\acslpp}{\textsc{ACSL++}\xspace}
+\newcommand{\acslb}{\acsl/acslpp\xspace}
+\include{fclangversion}
+
+
+\makeindex
+
+\begin{document}
+
+\coverpage{\fclang User Manual}
+
+\begin{titlepage}
+\begin{flushleft}
+\includegraphics[height=14mm]{cealistlogo.jpg}
+\end{flushleft}
+\vfill
+\title{\fclang Plug-in}{Release \fclangversion
+%% \ifthenelse{\equal{\eacslversion}{\fcversion}}{}{%
+%% \\[1em] compatible with \framac \fcversion}
+}
+\author{David R. Cok}
+\begin{center}
+CEA LIST\\ Software Reliability \& Security Laboratory
+\end{center}
+\begin{center}
+ Last modified \ddMyyyydate\today
+\end{center}
+\vfill
+\begin{flushleft}
+ \textcopyright 2013-2018 CEA LIST
+%%
+ %% This work has been supported by the VESSEDIA project).
+\end{flushleft}
+\end{titlepage}
+
+\tableofcontents
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\chapter*{Foreword}
+\markright{}
+\addcontentsline{toc}{chapter}{Foreword}
+
+This is the user manual of the \framac plug-in
+\fclang\footnote{\url{https://frama-c.com/frama-clang.html}}. The contents of this
+document correspond to its version \fclangversion compatible with
+\fcversion version of \framac~\cite{userman,fac15}. The development of
+the \fclang plug-in is still ongoing. Features described by this document may
+evolve in the future.
+
+\section*{Acknowledgements}
+
+We gratefully thank the people who contributed to this document:
+David R. Cok, Virgile Prevosto, Armand Pucetti, Franck Verdrine.
+
+TBD-VESSEDIA
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\include{introduction}
+\include{description}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\appendix
+
+\include{changes}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\bibname}
+\bibliographystyle{plain}
+\bibliography{./biblio}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%% \cleardoublepage
+%% \addcontentsline{toc}{chapter}{\listfigurename}
+%% \listoffigures
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\indexname}
+\printindex
+
+\end{document}