diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..445b8df769694e9290747315b8942193a6528b7e
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -0,0 +1,113 @@
+MAIN=main
+DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
+ intro_modern.tex speclang_modern.tex \
+ libraries_modern.tex concl_modern.tex changes_modern.tex \
+ term_modern.bnf binders_modern.bnf predicate_modern.bnf \
+ fn_behavior_modern.bnf oldandresult_modern.bnf \
+ loc_modern.bnf \
+ assertions_modern.bnf loops_modern.bnf st_contracts_modern.bnf \
+ logic_modern.bnf data_invariants_modern.bnf model_modern.bnf \
+ ghost_modern.bnf generalinvariants_modern.bnf iterator_modern.bnf \
+ bsearch.c bsearch2.c link.c
+
+.PHONY: all e-acsl default
+
+default: e-acsl.pdf
+
+e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
+
+all: e-acsl
+
+LANGUAGE_VERSION=1.5-4+dev
+EACSL_VERSION= 0.1+dev
+
+EACSL_DIR=$(HOME)/plugins/e-acsl
+DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
+install: e-acsl-implementation.pdf e-acsl.pdf
+ cp -f $^ $(EACSL_DIR)/doc/manuals
+ cp -f e-acsl.pdf \
+ $(DISTRIB_DIR)/download/e-acsl/e-acsl-$(LANGUAGE_VERSION).pdf
+ cp -f e-acsl-implementation.pdf \
+ $(DISTRIB_DIR)/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
+
+include support/MakeLaTeXModern
+
+eacslversion.tex: Makefile
+ rm -f $@
+ echo '\\newcommand{\\eacslversion}{$(EACSL_VERSION)}' > $@
+ 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
+
+# version WEB liée à ce qui est implementé
+e-acsl-implementation.pdf: $(DEPS_MODERN)
+
+e-acsl-implementation.tex: $(MAIN).tex Makefile
+ rm -f $@
+ sed -e '/PrintRemarks/s/%--//' $^ > $@
+ chmod a-w $@
+
+# version WEB du langage E-ACSL
+e-acsl.pdf: $(DEPS_MODERN)
+
+e-acsl.tex: e-acsl-implementation.tex Makefile
+ rm -f $@
+ sed -e '/PrintImplementationRq/s/%--//' $^ > $@
+ chmod a-w $@
+
+# version pour le goupe de travail E-ACSL
+$(MAIN).pdf: $(DEPS_MODERN)
diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
new file mode 100644
index 0000000000000000000000000000000000000000..bc5d0d0334b30304235f5b0800ddc29a08358e43
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -0,0 +1,7 @@
+\begin{syntax}
+ compound-statement ::= "{" declaration* statement* assertion+ "}"
+ \
+ statement ::= assertion statement \
+ assertion ::= "/*@" "assert" pred ";" "*/" ;
+ | { "/*@" "for" id ("," id)* ":" "assert" pred ";" "*/" } ;
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/at.c b/src/plugins/e-acsl/doc/refman/at.c
new file mode 100644
index 0000000000000000000000000000000000000000..dad0a3819895eccf8c3eaf5cfad9a375aaf449dd
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at.c
@@ -0,0 +1,15 @@
+/*@ requires \valid(p+(0..1));
+ @ requires \valid(q);
+ @*/
+void f(int *p, int *q) {
+ *p = 0;
+ *(p+1) = 1;
+ *q = 0;
+ L1: *p = 2;
+ *(p+1) = 3;
+ *q = 1;
+ L2:
+ /*@ assert (\at(*(p+\at(*q,L1)),Here) == 2); */
+ /*@ assert (\at(*(p+\at(*q,Here)),L1) == 1); */
+ return ;
+}
diff --git a/src/plugins/e-acsl/doc/refman/biblio.bib b/src/plugins/e-acsl/doc/refman/biblio.bib
new file mode 100644
index 0000000000000000000000000000000000000000..7f3a415da0bc157cfd6bcdb53c3366a2c2d425e9
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/biblio.bib
@@ -0,0 +1,91 @@
+@STRING{SV = {Springer}}
+
+@STRING{LNCS = {Lecture Notes in Computer Science}}
+
+@INPROCEEDINGS{jml,
+ author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
+ and Clyde Ruby and Bart Jacobs},
+ title = {{JML}: notations and tools supporting detailed design in {Java}},
+ booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota},
+ pages = {105--106},
+ year = 2000
+}
+
+@INPROCEEDINGS{chalin07,
+ author = {Patrice Chalin},
+ title = {A Sound Assertion Semantics for the Dependable Systems Evolution
+ Verifying Compiler},
+ booktitle = {Proceedings of the International Conference on Software
+ Engineering (ICSE'07)},
+ pages = {23-33},
+ year = 2007,
+ address = {Los Alamitos, CA, USA},
+ publisher = {IEEE Computer Society}
+}
+
+@INPROCEEDINGS{chalin05,
+ author = {Patrice Chalin},
+ title = {Reassessing {JML}'s Logical Foundation},
+ booktitle = {Proceedings of the 7th Workshop on Formal Techniques for
+ Java-like Programs (FTfJP'05)},
+ year = 2005,
+ address = {Glasgow, Scotland},
+ month = JUL
+}
+
+@manual{acsl,
+ title = {{ACSL, ANSI/ISO C Specification Language}},
+ author = {Patrick Baudin and Jean-Christophe Filliâtre and Claude Marché
+ and Benjamin Monate and Yannick Moy and Virgile Prevosto},
+ year = {2011},
+ month = feb,
+ note = {Vesion 1.5. \url{http://frama-c.com/acsl.html}},
+}
+
+@manual{acslimplem,
+ title = {{ACSL version 1.5, Implementation in Carbon-20110201}},
+ author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
+ Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
+ year = {2011},
+ month = feb,
+ note = {\url{http://frama-c.com/acsl.html}},
+}
+
+@manual{framac,
+ title = {Frama-C User Manual},
+ author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
+Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
+ year = {2011},
+ month = oct,
+ note = {\url{http://frama-c.com}},
+}
+
+@manual{eacsl-plugin,
+ title = {Frama-C's E-ACSL Plug-in},
+ author = {Julien Signoles},
+ year = {2012},
+ month = jan,
+ note = {\url{http://frama-c.com}},
+}
+
+@manual{value,
+ title = {Frama-C's value analysis plug-in},
+ author = {Pascal Cuoq and Virgile Prevosto},
+ year = {2011},
+ month = oct,
+ note = {\url{http://frama-c.com/value.html}},
+}
+
+@BOOK{KR88,
+ author = {Brian Kernighan and Dennis Ritchie},
+ title = {The C Programming Language (2nd Ed.)},
+ publisher = {Prentice-Hall},
+ year = 1988
+}
+
+@MANUAL{standardc99,
+ title = {The {ANSI C} standard ({C99})},
+ organization = {International Organization for Standardization ({ISO})},
+ key = {C99},
+ note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}}
+}
diff --git a/src/plugins/e-acsl/doc/refman/binders.tex b/src/plugins/e-acsl/doc/refman/binders.tex
new file mode 100644
index 0000000000000000000000000000000000000000..8b62fd8f3903d9968695a825e5b51f68c2510a0d
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/binders.tex
@@ -0,0 +1,18 @@
+\begin{syntax}
+ binders ::= binder (, binder)* ;
+ \
+ binder ::= type-expr variable-ident;
+ (,variable-ident)*
+ \
+ type-expr ::= logic-type-expr | C-type-expr
+ \
+ logic-type-expr ::= built-in-logic-type ;
+ | id ; type id
+ \
+ built-in-logic-type ::= "boolean" | "integer" | { "real" }
+ \
+ variable-ident ::= id
+ | "*" variable-ident ;
+ | variable-ident "[]";
+ | "(" variable-ident ")"
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/bsearch.c b/src/plugins/e-acsl/doc/refman/bsearch.c
new file mode 100644
index 0000000000000000000000000000000000000000..6025c21a6b8b9cdb58f29f2a2653e4c876db2cca
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/bsearch.c
@@ -0,0 +1,25 @@
+/*@ requires n >= 0 && \valid(t+(0..n-1));
+ @ assigns \nothing;
+ @ ensures -1 <= \result <= n-1;
+ @ behavior success:
+ @ ensures \result >= 0 ==> t[\result] == v;
+ @ behavior failure:
+ @ assumes t_is_sorted : \forall integer k1, int k2;
+ @ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
+ @ ensures \result == -1 ==>
+ @ \forall integer k; 0 <= k < n ==> t[k] != v;
+ @*/
+int bsearch(double t[], int n, double v) {
+ int l = 0, u = n-1;
+ /*@ loop invariant 0 <= l && u <= n-1;
+ @ for failure: loop invariant
+ @ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
+ @*/
+ while (l <= u ) {
+ int m = l + (u-l)/2; // better than (l+u)/2
+ if (t[m] < v) l = m + 1;
+ else if (t[m] > v) u = m - 1;
+ else return m;
+ }
+ return -1;
+}
diff --git a/src/plugins/e-acsl/doc/refman/bsearch2.c b/src/plugins/e-acsl/doc/refman/bsearch2.c
new file mode 100644
index 0000000000000000000000000000000000000000..0588ad16723c164bc050736900cd8b001d0e940b
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/bsearch2.c
@@ -0,0 +1,29 @@
+/*@ requires n >= 0 && \valid(t+(0..n-1));
+ @ assigns \nothing;
+ @ ensures -1 <= \result <= n-1;
+ @ behavior success:
+ @ ensures \result >= 0 ==> t[\result] == v;
+ @ behavior failure:
+ @ assumes t_is_sorted : \forall integer k1, int k2;
+ @ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
+ @ ensures \result == -1 ==>
+ @ \forall integer k; 0 <= k < n ==> t[k] != v;
+ @*/
+int bsearch(double t[], int n, double v) {
+ int l = 0, u = n-1;
+ /*@ assert 0 <= l && u <= n-1;
+ @ for failure: assert
+ @ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
+ @*/
+ while (l <= u ) {
+ int m = l + (u-l)/2; // better than (l+u)/2
+ if (t[m] < v) l = m + 1;
+ else if (t[m] > v) u = m - 1;
+ else return m;
+ /*@ assert 0 <= l && u <= n-1;
+ @ for failure: assert
+ @ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
+ @*/ ;
+ }
+ return -1;
+}
diff --git a/src/plugins/e-acsl/doc/refman/cealistlogo.jpg b/src/plugins/e-acsl/doc/refman/cealistlogo.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..966be5a8ff6d50d9a7f50759633ca144c4c5db1c
Binary files /dev/null and b/src/plugins/e-acsl/doc/refman/cealistlogo.jpg differ
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..04ded99c7eb15b6c63b08ca0a84ecfc4f6711bbb
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -0,0 +1,91 @@
+\section{Changes}
+
+\subsection{Version \version}
+
+\subsection{Version 1.5-4}
+
+\begin{itemize}
+\item Fix typos.
+\item \changeinsection{expressions}{fix syntax of guards in iterators}
+\item \changeinsection{semantics}{fix definition of undefined terms and
+ predicates}
+\item \changeinsection{typing}{no user-defined types}
+\item \changeinsection{builtinconstructs}{no more implementation issue for
+ \lstinline|\\old|}
+\item \changeinsection{at}{more restrictive scoping rule for label references
+in \lstinline|\\at|}
+\end{itemize}
+
+\subsection{Version 1.5-3}
+
+\begin{itemize}
+\item Fix various typos.
+\item Warn about features known to be difficult to implement.
+\item \changeinsection{expressions}{fix semantics of ternary operator}
+\item \changeinsection{expressions}{fix semantics of cast operator}
+\item \changeinsection{expressions}{improve syntax of iterator quantifications}
+\item \changeinsection{semantics}{improve and fix example \ref{ex:semantics}}
+\item \changeinsection{loop_annot}{improve explanations about loop invariants}
+\item \changeinsection{logicalstates}{add hybrid functions and predicates}
+\end{itemize}
+
+\subsection{Version 1.5-2}
+
+\begin{itemize}
+\item \changeinsection{expressions}{remove laziness of operator
+ \lstinline|<==>|}
+\item \changeinsection{expressions}{restrict guarded quantifications to integer}
+\item \changeinsection{expressions}{add iterator quantifications}
+\item \changeinsection{expressions}{extend unguarded quantifications to char}
+\item \changeinsection{locations}{extend syntax of set comprehensions}
+\item \changeinsection{loop_annot}{simplify explanations for loop invariants and
+ add example.}
+\end{itemize}
+
+\subsection{Version 1.5-1}
+
+\begin{itemize}
+\item Fix many typos.
+\item Highlight constructs with semantic changes in grammars.
+\item Explain why unsupported features have been removed.
+\item Indicate that experimental \acsl features are unsupported.
+\item Add operations over memory like \lstinline|\valid|.
+\item \changeinsection{expressions}{lazy operators \lstinline|&&|,
+ \lstinline+||+, \lstinline|\^\^|, \lstinline|==>| and \lstinline|<==>|}
+\item \changeinsection{expressions}{allow unguarded quantification over boolean}
+\item \changeinsection{expressions}{revise syntax of \lstinline|\\exists|}
+\item \changeinsection{semantics}{better semantics for undefinedness}
+\item \changeinsection{locations}{revise syntax of set comprehensions}
+\item \changeinsection{loop_annot}{add loop invariants, but they lose their
+ inductive \acsl nature}
+\item \changeinsection{generalmeasures}{add general measures for termination}
+\item \changeinsection{specmodules}{add specification modules}
+\end{itemize}
+
+\subsection{Version 1.5-0}
+
+\begin{itemize}
+\item Initial version.
+\end{itemize}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\ifthenelse%
+ {\boolean{PrintImplementationRq}}%
+ {
+\section{Changes in \eacsl implementation}
+
+\subsection{Version \eacslversion}
+
+\begin{itemize}
+\item Implement bitwise complementation.
+\end{itemize}
+
+\subsection{Version 0.1}
+
+\begin{itemize}
+\item Initial version.
+\end{itemize}
+
+ }%
+ {}
diff --git a/src/plugins/e-acsl/doc/refman/concl_modern.tex b/src/plugins/e-acsl/doc/refman/concl_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..58ce943e29c189fb4d75b0098c5683e6405c834c
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/concl_modern.tex
@@ -0,0 +1,9 @@
+
+\chapter{Conclusion}
+
+This document presents an Executable ANSI/ISO C Specification Language. It
+provides a subset of \acsl~\cite{acsl} implemented~\cite{acslimplem} in the
+\framac platform~\cite{framac} in which each construct may be evaluated at
+runtime. The specification language described here is intented to evolve in the
+future in two directions. First it is based on \acsl which is itself still
+evolving. Second the considered subset of \acsl may also change.
diff --git a/src/plugins/e-acsl/doc/refman/data_invariants.tex b/src/plugins/e-acsl/doc/refman/data_invariants.tex
new file mode 100644
index 0000000000000000000000000000000000000000..fba204a690117900c7e57da09945e751c0a52c84
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/data_invariants.tex
@@ -0,0 +1,13 @@
+\begin{syntax}
+ declaration ::= { "/*@" data-inv-decl "*/" }
+ \
+ { data-inv-decl } ::= { data-invariant } | { type-invariant }
+ \
+ { data-invariant } ::= { { inv-strength? } "global" "invariant" } ;
+ { id ":" pred ";" }
+ \
+ { type-invariant } ::= { { inv-strength? } "type" "invariant" };
+ { id "(" C-type-expr id ")" "=" pred ";" }
+ \
+ { inv-strength } ::= { "weak" } | { "strong" }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..b1d1d32de62af5112dc875c7cf4b8e1530f4ce4d
Binary files /dev/null and b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl.pdf b/src/plugins/e-acsl/doc/refman/e-acsl.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..83c30a2bc54f9289cf8dba18f13388ed8febe33e
Binary files /dev/null and b/src/plugins/e-acsl/doc/refman/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6ad21205e535e4c491538d22375635051875df3d
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -0,0 +1 @@
+\newcommand{\eacslversion}{0.1+dev}
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
new file mode 100644
index 0000000000000000000000000000000000000000..a9a3b5b40a92cf37ea8840cdda72832a57a9d4dc
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -0,0 +1,26 @@
+\begin{syntax}
+ [ function-contract ] ::= requires-clause*;
+ { decreases-clause? } simple-clause*;
+ named-behavior* { completeness-clause* }
+ \
+ requires-clause ::= "requires" predicate ";"
+ \
+ { decreases-clause } ::= { "decreases" term ("for" ident)? ";" }
+ \
+ [ simple-clause ] ::= { assigns-clause } | ensures-clause
+ \
+ { assigns-clause } ::= { "assigns" locations ";" }
+ \
+ { locations } ::= { location ("," location) * | "\nothing" }
+ \
+ ensures-clause ::= "ensures" predicate ";"
+ \
+ named-behavior ::= "behavior" id ":" behavior-body
+ \
+ behavior-body ::= assumes-clause* requires-clause* simple-clause*
+ \
+ assumes-clause ::= "assumes" predicate ";"
+ \
+ { completeness-clause } ::= { "complete" "behaviors" (id (","id)*)? ";" } ;
+ | { "disjoint" "behaviors" (id (","id)*)? ";" }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-book.cls b/src/plugins/e-acsl/doc/refman/frama-c-book.cls
new file mode 100644
index 0000000000000000000000000000000000000000..562571271e1660418447e02673f904e42fa8ef00
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/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{\setlength\unitlength{1cm}%
+ \begin{picture}(0,0)(#1,#2)
+ \put(0,0){\includegraphics{#3}}
+ \end{picture}}
+\fancypagestyle{plain}{%
+ \fancyfoot{}
+ \fancyhead{}
+ \fancyhead[LE]{\put@bg(2.4,27.425){frama-c-left.pdf}}
+ \fancyhead[LO]{\put@bg(2.7,27.425){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){frama-c-left.pdf}}
+ \fancyhead[LO]{\put@bg(2.7,27.425){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,0){\includegraphics{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={assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
+ boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
+ exit_behavior,ghost,global,inductive,integer,invariant,lemma,logic,loop,
+ model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
+ union,variant},
+% otherkeywords={\\at,\\base_addr,\\block_length,\\false,\\fresh,\\from,
+% \\initialized,\\lambda,\\let,\\match,\\max,\\nothing,\\null,
+% \\numof,\\old,\\result,\\specified,\\strlen,\\sum,\\true,
+% \\valid,\\valid_range},
+ 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={[is]{//NOPP-BEGIN}{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}}
+
+\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@basic,%
+}
+
+\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
+\newcommand{\whyinput}[1]%
+{\lstinputlisting[style=why-style]{#1}}
+\newcommand{\whyinline}[1]%
+{\lstinline[style=why-style]{#1}}
+
+% --------------------------------------------------------------------------
+% --- End. ---
+% --------------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-cover.pdf b/src/plugins/e-acsl/doc/refman/frama-c-cover.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..c0b6101f8a9a665f5ca48783d8d1dfefc765ed4a
Binary files /dev/null and b/src/plugins/e-acsl/doc/refman/frama-c-cover.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-left.pdf b/src/plugins/e-acsl/doc/refman/frama-c-left.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..54a64f214ddc0e9dc88eec38303070540962545d
Binary files /dev/null and b/src/plugins/e-acsl/doc/refman/frama-c-left.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/frama-c-right.pdf b/src/plugins/e-acsl/doc/refman/frama-c-right.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..13ba3e3c03fdca91713629b5b115643281f5c109
Binary files /dev/null and b/src/plugins/e-acsl/doc/refman/frama-c-right.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/generalinvariants.tex b/src/plugins/e-acsl/doc/refman/generalinvariants.tex
new file mode 100644
index 0000000000000000000000000000000000000000..246a377d67ff92011258af572e78b8bc3ecc0daf
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/generalinvariants.tex
@@ -0,0 +1,4 @@
+\begin{syntax}
+ assertion ::= [ "/*@" "invariant" pred ";" "*/" ] ;
+ | [ { "/*@" "for" id ("," id)* ":" "invariant" pred ";" "*/" } ] ;
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/ghost.tex b/src/plugins/e-acsl/doc/refman/ghost.tex
new file mode 100644
index 0000000000000000000000000000000000000000..b31bc876a08fd3ceedf966d51c255efb515ec53b
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/ghost.tex
@@ -0,0 +1,37 @@
+\begin{syntax}
+
+ ghost-type-specifier ::= C-type-specifier ;
+ | { logic-type-name } \
+ declaration ::= C-declaration ;
+ | { "/*@" "ghost" } ;
+ { ghost-declaration "*/" } \
+ direct-declarator ::= C-direct-declarator ;
+ | direct-declarator ;
+ "(" parameter-type-list? ")";
+ {"/*@" "ghost"};
+ {"("parameter-list")"};
+ {"*/"}; ghost args
+ \
+ postfix-expression ::= C-postfix-expression ;
+ | postfix-expression ;
+ "(" argument-expression-list? ")";
+ {"/*@" "ghost"} ;
+ { "(" argument-expression-list ")"};
+ { "*/"} ; call with ghosts
+ \
+ statement ::= C-statement ;
+ | { statements-ghost } \
+ { statements-ghost } ::= { "/*@" "ghost" };
+ { ghost-statement+ "*/" } \
+ ghost-selection-statement ::= C-selection-statement ;
+ | "if" "(" expression ")";
+ statement;
+ {"/*@" "ghost" "else"};
+ { C-statement+ };
+ { "*/"} \
+
+ struct-declaration ::= C-struct-declaration ;
+ | {"/*@" "ghost" };
+ {C-struct-declaration "*/"} ; ghost field
+
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..bcf74f8361e7faa8fe8b366869c15deb00a2fcf4
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -0,0 +1,91 @@
+%; whizzy-master "main.tex"
+\chapter{Introduction}
+
+This document is a reference manual for
+\ifthenelse{\boolean{PrintImplementationRq}}%
+{the \eacsl implementation provided by the \eacsl plug-in~\cite{eacsl-plugin}
+ (version\eacslversion) of the \framac framework~\cite{framac}.}%
+{E-ACSL.}
+\eacsl is an acronym for ``Executable ANSI/ISO C
+Specification Language''. It is an ``executable'' subset of
+\emph{stable} \acsl~\cite{acsl} implemented~\cite{acslimplem} in the \framac
+platform~\cite{framac}. ``Stable'' means that no experimental \acsl feature is
+supported by \eacsl. Contrary to \acsl, each \eacsl specification is
+executable: it may be evaluated at runtime.
+
+In this document, we assume that the reader has a good knowledge of both
+ACSL~\cite{acsl} and the ANSI C programming language~\cite{standardc99,KR88}.
+
+\section{Organization of this document}
+
+This document is organized in the very same way that the reference manual of
+\acsl~\cite{acsl}.
+
+Instead of being a fully new reference manual, this document points out the
+differences between \eacsl and \acsl. Each \eacsl construct which is not pointed
+out must be considered to have the very same semantics than its \acsl
+counterpart. For clarity, each relevant grammar rules are given in BNF form
+in separate figures like the \acsl reference manual does. In these rules,
+constructs with semantic changes are displayed in \markdiff{blue}.
+
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+Not all of the features mentioned in this document are currently
+implemented in the \framac's \eacsl plug-in. Those who aren't yet are signaled
+as in the following line:
+\begin{quote}
+\notimplemented[Additional remarks on the feature may appear as footnote.]%
+{This feature is not currently supported by \framac's \eacsl plug-in.}
+\end{quote}
+
+As a summary, Figure~\ref{fig:notyet} synthetizes main features that are not
+currently implemented into the \framac's \eacsl plug-in.
+\begin{figure}[htbp]\label{fig:notyet}
+ \begin{center}
+ \begin{tabular}{|l|l|}
+ \hline
+ typing
+ & mathematical reals \\
+ \hline
+ terms
+ & \lstinline|\\true| and \lstinline|\\false| \\
+ & bitwise operators \\
+ & let binding \\
+ & typeof \\
+ & t-sets \\
+ & \lstinline|base\_addr|, \lstinline|offset| and
+ \lstinline|block\_length|
+ \\
+ \hline
+ predicates
+ & exclusive or operator \\ % \lstinline|^^|
+ & let bindings \\
+ & quantifications over non-integer types \\
+ & \lstinline|valid| and \lstinline|valid\_range| \\
+ & \lstinline|initialized| and \lstinline|specified|
+ \\
+ \hline
+ annotations
+ & behavior-specific annotations \\
+ & loop annotations \\
+ & global annotations
+ \\
+ \hline
+ behavior clauses
+ & assigns \\
+ & decreases \\
+ & abrupt termination \\
+ & complete and disjoint behaviors
+ \\
+ \hline
+ \end{tabular}
+ \end{center}
+ \caption{Summary of not-yet-implemented features.}
+\end{figure}
+}%
+{}
+
+\section{Generalities about Annotations}\label{sec:gener-about-annot}
+\nodiff
+
+\section{Notations for grammars}
+\nodiff
diff --git a/src/plugins/e-acsl/doc/refman/iterator.tex b/src/plugins/e-acsl/doc/refman/iterator.tex
new file mode 100644
index 0000000000000000000000000000000000000000..156f6df939a182541e1b808cb176bcbfbc68778f
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/iterator.tex
@@ -0,0 +1,12 @@
+\begin{syntax}
+ declaration ::= [ { "//@" "iterator" id "("wildcard-param","
+ wildcard-param")" ":" } ] ;
+ [ { "nexts" terms ";" "guards" predicates ";" } ]
+ \
+ [ { wildcard-param } ] ::= { parameter } ;
+ | [ { "_" } ]
+ \
+ [ { terms } ] ::= [ { term (, term)* } ]
+ \
+ [ { predicates } ] ::= [ { predicate (, predicate)* } ]
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/libraries_modern.tex b/src/plugins/e-acsl/doc/refman/libraries_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..862e5a22fe8f7cc66e9e777cf84754daf29ee711
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/libraries_modern.tex
@@ -0,0 +1,6 @@
+\chapter{Libraries}
+\label{chap:lib}
+
+\emph{Disclaimer:} this chapter is yet empty. It is left here to give an idea of
+what the final document will look and to be consistent with the \acsl reference
+manual~\cite{acsl}.
diff --git a/src/plugins/e-acsl/doc/refman/link.c b/src/plugins/e-acsl/doc/refman/link.c
new file mode 100644
index 0000000000000000000000000000000000000000..e003ebf7ff4ddef5b22c38b3c4272061bd53c378
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/link.c
@@ -0,0 +1,11 @@
+struct btree {
+ int val;
+ struct btree *left, *right;
+};
+
+/*@ iterator access(_, struct btree *t):
+ @ nexts t->left, t->right;
+ @ guards \valid(t->left), \valid(t->right); */
+
+/*@ predicate is_even(struct btree *t) =
+ @ \forall struct btree *tt; access(tt, t) ==> tt->val % 2 == 0; */
diff --git a/src/plugins/e-acsl/doc/refman/loc.tex b/src/plugins/e-acsl/doc/refman/loc.tex
new file mode 100644
index 0000000000000000000000000000000000000000..23fbf3635333081f7164e4636227fbf5f204a2c1
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/loc.tex
@@ -0,0 +1,18 @@
+\begin{syntax}
+ tset ::= { "\empty" } ; empty set
+ | tset "->" id ;
+ | tset "." id ;
+ | "*" tset ;
+ | "&" tset ;
+ | tset "[" tset "]" ;
+ | [ { term ".." term } ] ; range
+ | { "\union" "(" tset ("," tset)* ")" } ; union of locations
+ | { "\inter" "(" tset ("," tset)* ")" }; intersection
+ | tset "+" tset ;
+ | "(" tset ")" ;
+ | [ { "{" tset "|" binder ";" guards ("&&" pred)? "}" } ]; set comprehension
+ | { "{" term "}" } ; explicit singleton
+ | term ; implicit singleton
+ \
+ pred ::= { "\subset" "(" tset "," tset ")" } ; set inclusion
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/logic.tex b/src/plugins/e-acsl/doc/refman/logic.tex
new file mode 100644
index 0000000000000000000000000000000000000000..283d438702d4e1cf0ca96627fa14e09c27728fbf
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/logic.tex
@@ -0,0 +1,19 @@
+\begin{syntax}
+ C-global-decl ::= { "/*@" logic-def+ "*/" }
+ \
+ [ { logic-def } ] ::= { logic-const-def } ;
+ | { logic-function-def } ;
+ | { predicate-def } ;
+ \
+ [ { type-expr } ] ::= { id };
+ \
+ [ { logic-const-def } ] ::= { "logic" type-expr id "=" term ";" }
+ \
+ [ { logic-function-def } ] ::= { "logic" type-expr id parameters "=" term ";" }
+ \
+ [ { predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
+ \
+ { parameters } ::= { "(" parameter (, parameter)* ")" }
+ \
+ { parameter } ::= { type-expr id }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6c4ffe3b7cc5b72cbc3f11bd3caff8e5ab10f13a
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -0,0 +1,28 @@
+\begin{syntax}
+ statement ::= { "/*@" loop-annot "*/" } ;
+ "while" "(" expr ")" statement ;
+ | { "/*@" loop-annot "*/" } ;
+ "for";
+ "(" expr ";" expr ";" expr ")";
+ statement ;
+ | { "/*@" loop-annot "*/" } ;
+ "do" statement ;
+ "while" "(" expr ")" ";"
+ \
+ { loop-annot } ::= { loop-clause* } ;
+ { loop-behavior* } ;
+ { loop-variant? }
+ \
+ { loop-clause } ::= { loop-invariant } ;
+ | { loop-assigns }
+ \
+ [ { loop-invariant } ] ::= [ { "loop" "invariant" pred ";" } ]
+ \
+ { loop-assigns } ::= { "loop" "assigns" locations ";" } ;
+ \
+ { loop-behavior } ::= { "for" id ("," id)* ":" } ;
+ { loop-clause* } ; annotation for behavior $id$
+ \
+ { loop-variant } ::= { "loop" "variant" term ";" } ;
+ | { "loop" "variant" term "for" id ";" } ; variant for relation $id$
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..51719d3d384b090aface34a61becfd4faa963e13
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/macros_modern.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/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5f968cf265420bd1e073549506154d0bf05c748a
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -0,0 +1,120 @@
+%; whizzy section -pdf -initex "pdflatex -ini"
+\documentclass[a4paper,web]{frama-c-book}
+\usepackage{hevea}
+\usepackage{ifthen}
+
+\input{./macros_modern}
+\input{eacslversion.tex}
+%Do not touch the following line. It is used in a Makefile hack to
+%produce the ACSL documents for the ACSL working group.
+%--\setboolean{PrintRemarks}{false}
+
+%Do not touch the following line. It is used in a Makefile hack to
+%produce the ACSL document shipped with the Frama-C distribution.
+%--\setboolean{PrintImplementationRq}{false}
+
+%\setboolean{ColorImplementationRq}{false}
+
+\usepackage{amssymb}
+\usepackage{graphicx}
+\usepackage{color}
+\usepackage{xspace}
+\usepackage{makeidx}
+\usepackage[normalem]{ulem}
+\usepackage[leftbars]{changebar}
+\usepackage{alltt}
+\makeindex
+
+\newcommand{\acslversion}{1.5\xspace}
+\newcommand{\version}{\acslversion-4+dev\xspace}
+
+\renewcommand{\textfraction}{0.01}
+\renewcommand{\topfraction}{0.99}
+\renewcommand{\bottomfraction}{0.99}
+
+\begin{document}
+\sloppy
+\hbadness=10000
+
+\ifthenelse{\boolean{PrintImplementationRq}}%
+ {\coverpage{\vbox{\mbox{E-ACSL Version \version}\\[5mm]
+\mbox{\huge{Implementation in Frama-C plug-in E-ACSL
+ version \eacslversion{}}}}}}%
+ {\coverpage{\vbox{\mbox{E-ACSL}\\[2mm]\vbox{\mbox{\huge{Executable ANSI/ISO C
+ Specification Language}}}\\[2mm]
+ \mbox{Version \version}}}}
+
+\begin{titlepage}
+\includegraphics[height=14mm]{cealistlogo.jpg}
+\vfill
+\title{E-ACSL\\[5mm]\huge{Executable ANSI/ISO C Specification Language}}%
+{Version \version{}\ifthenelse{\boolean{PrintImplementationRq}}%
+{~--~Frama-C plug-in E-ACSL version \eacslversion}{}}
+
+\author{Julien Signoles}
+
+CEA LIST, Software Reliability Laboratory\\
+\vfill
+\begin{flushleft}
+ \textcopyright 2011-2012 CEA LIST
+
+ This work has been supported by the `Hi-Lite' FUI project (FUI AAP 9).
+\end{flushleft}
+\end{titlepage}
+
+%%Contents should open on right
+\cleardoublepage
+\phantomsection
+\label{chap:contents}
+\tableofcontents
+
+\chapter*{Foreword}
+
+This is a preliminary design of the \eacsl language, a deliverable of
+the task 3.4 of the FUI-9 project Hi-Lite
+(\url{http://www.open-do.org/projects/hi-lite}).
+
+This is the version \version{} of \eacsl design based on \acsl version
+\acslversion~\cite{acsl}. Several features may still evolve in the future.
+
+\section*{Acknowledgements}
+
+We gratefully thank all the people who contributed to this document:
+Patrick Baudin,
+Bernard Botella,
+Loïc Correnson,
+Pascal Cuoq,
+Johannes Kanig,
+Benjamin Monate,
+Yannick Moy and
+Virgile Prevosto.
+
+\include{intro_modern}
+
+\include{speclang_modern}
+
+\include{libraries_modern}
+
+\include{concl_modern}
+
+\appendix
+
+\chapter{Appendices}
+\label{chap:appendix}
+
+\include{changes_modern}
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\bibname}
+\bibliographystyle{plain}
+\bibliography{./biblio}
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\listfigurename}
+\listoffigures
+
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\indexname}
+\printindex
+
+\end{document}
diff --git a/src/plugins/e-acsl/doc/refman/model.tex b/src/plugins/e-acsl/doc/refman/model.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6e2a728555951a84b122230fb772badab6b01621
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/model.tex
@@ -0,0 +1,7 @@
+\begin{syntax}
+ declaration ::= C-declaration ;
+ | { "/*@" "model" C-declaration "*/" } ; model variable
+ \
+ struct-declaration ::= C-struct-declaration ;
+ | { "/*@" "model" C-struct-declaration "*/" } ; model field
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/oldandresult.tex b/src/plugins/e-acsl/doc/refman/oldandresult.tex
new file mode 100644
index 0000000000000000000000000000000000000000..1e2bfd448d38abfad87769315da0be7997359923
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/oldandresult.tex
@@ -0,0 +1,11 @@
+\begin{syntax}
+ term ::= "\old" "(" term ")" ; old value
+ | "\result" ; result of a function
+ \
+ pred ::= "\old" "(" pred ")"
+\end{syntax}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End:
diff --git a/src/plugins/e-acsl/doc/refman/predicate.tex b/src/plugins/e-acsl/doc/refman/predicate.tex
new file mode 100644
index 0000000000000000000000000000000000000000..ecddda6bc58b811f2eb86ca9d941d1da3c7d4498
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/predicate.tex
@@ -0,0 +1,39 @@
+\begin{syntax}
+ rel-op ::= "==" | "!=" | "<=" | ">=" | ">" | "<"
+ \
+ pred ::= "\true" | "\false" ;
+ | term (rel-op term)+ ; comparisons
+ | { id "(" term ("," term)* ")" } ; predicate application
+ | "(" pred ")" ; parentheses
+ | [ pred "&&" pred ] ; conjunction
+ | [ pred "||" pred ] ; disjunction
+ | [ pred "==>" pred ] ; implication
+ | pred "<==>" pred ; equivalence
+ | "!" pred ; negation
+ | [ { pred "^^" pred } ] ; exclusive or
+ | [ term "?" pred ":" pred ] ; ternary condition
+ | [ pred "?" pred ":" pred ];
+ | { "\let" id "=" term ";" pred }; local binding
+ | { "\let" id "=" pred ";" pred };
+ | [ "\forall" binders ";" ] ;
+ [ integer-guards "==>" pred ]; univ. integer quantification
+ | [ "\exists" binders ";" ];
+ [ integer-guards "&&" pred ] ; exist. integer quantification
+ | [ { "\forall" binders ";" } ] ;
+ [ { iterator-guard "==>" pred } ]; univ. iterator quantification
+ | [ { "\exists" binders ";" } ];
+ [ { iterator-guard "&&" pred } ] ; exist. iterator quantification
+ | [ { "\forall" binders ";" pred } ]; univ. quantification
+ | [ { "\exists" binders ";" pred } ]; exist. quantification
+ | id ":" pred ; syntactic naming
+ \
+ [ integer-guards ] ::= [ interv ("&&" interv)* ]
+ \
+ [ interv ] ::= [ (term integer-guard-op)+ ] ;
+ [ id ] ;
+ [ (integer-guard-op term)+ ]
+ \
+ [ integer-guard-op ] ::= [ "<=" | "<" ]
+ \
+ [ { iterator-guard } ] ::= [ { id "(" term"," term ")" } ]
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
new file mode 100644
index 0000000000000000000000000000000000000000..b418fcf6fb5c11950dcc75366e656f275307c233
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -0,0 +1,768 @@
+%; whizzy-master "main.tex"
+
+\chapter{Specification language}
+\label{chap:base}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Lexical rules}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Logic expressions}
+\label{sec:expressions}
+
+\except{guarded quantificatication}.
+
+More precisely, grammars of terms and binders presented respectively
+Figures~\ref{fig:gram:term} and~\ref{fig:gram:binders} are the same than the one
+of \acsl, while Figure~\ref{fig:gram:pred} presents grammar of predicates. The
+only difference between \eacsl and \acsl predicates are quantifications.
+
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{term_modern.bnf}
+ \end{cadre}
+ \caption{Grammar of terms}
+\label{fig:gram:term}
+\end{figure}
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{predicate_modern.bnf}
+ \end{cadre}
+ \caption{Grammar of predicates}
+\label{fig:gram:pred}
+\end{figure}
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\textwidth} \input{binders_modern.bnf}
+ \end{minipage}}
+ \caption{Grammar of binders and type expressions}
+\label{fig:gram:binders}
+\end{figure}
+
+\subsection*{Quantification}
+\eacsl quantification must be computable. They are limited to two limited forms.
+
+\begin{description}
+\item[Guarded integer quantification] Guarded universal quantification is
+ denoted by
+\begin{lstlisting}
+\forall $\tau$ $x_1$,$\ldots$,$x_n$;
+ $a_1$ <= $x_1$ <= $b_1$ $\ldots$ && $a_n$ <= $x_n$ <= $b_n$
+ ==> p
+\end{lstlisting} and guarded existential quantification by
+\begin{lstlisting}
+\exists $\tau$ $x_1$,$\ldots$,$x_n$;
+ $a_1$ <= $x_1$ <= $b_1$ $\ldots$ && $a_n$ <= $x_n$ <= $b_n$
+ && p
+\end{lstlisting}
+Each variable must be guarded exactly once and the guard of $x_i$ must appear
+before the guard of $x_j$ if $i < j$ (\emph{i.e.} order of guards must follow
+order of binders).
+
+Following the definition, each quantified variable belongs to a finite
+interval. Since finite interval is only computable in practice for integers,
+this form of quantifier is limited to \texttt{integer} and its subtype. Thus
+there is no guarded quantification over \texttt{float}, \texttt{real}, \C
+pointers or logic types.
+
+\item[\notimplemented{Iterator quantification}] In order to iterate over
+ non-integer types, \eacsl introduces a notion of $iterators$ over types:
+ standard \acsl unguarded quantifications are only allowed over a type which an
+ iterator is attached to.
+
+ Iterators are introduced by a specific construct which attachs two sets ---
+ namely \texttt{nexts} and the \texttt{guards} --- to a binary predicate over a
+ type $\tau$. Both sets must have the same cardinal. This construct is
+ described by the grammar of Figure~\ref{fig:gram:iterator}.
+ \begin{figure}[htbp]
+ \begin{cadre}
+ \input{iterator_modern.bnf}
+ \end{cadre}
+ \caption{Grammar of iterator declarations}
+ \label{fig:gram:iterator}
+ \end{figure}
+ For a type $\tau$, \texttt{nexts} is a set of terms which take an argument of
+ type $\tau$ and return a value of type $\tau$ which computes the next element
+ in this type, while \texttt{guards} is a set of predicates which take an
+ argument of type $\tau$ and are valid (resp. invalid) to continue (resp. stop)
+ the iteration.
+
+ Furthermore, the guard of a quantification using an iterator must be the
+ predicate given in the definition of the iterator. This abstract binary
+ predicate takes two arguments of the same type. One of them must be unnamed by
+ using a wildcard (character underscore \texttt{'\_'}). The unnamed argument
+ must be binded to the guantifier, while the other corresponds to the term from
+ which the iteration begins.
+ \begin{example}
+ The following example introduces binary trees and a predicate which is valid
+ if and only if each value of a binary tree is even.
+ \cinput{link.c}
+ \end{example}
+
+\item[\notimplemented{Unguarded quantification}] They are only allowed over
+ boolean and char.
+\end{description}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Operators precedence}
+\nodiff
+
+Figure~\ref{fig:precedence} summarizes operator precedences.
+\begin{figure}[htbp]
+ \begin{center}
+ \begin{tabular}{|l|l|l|}
+ \hline
+ class & associativity & operators \\
+ \hline
+ selection & left & \lstinline|[$\cdots$]| \lstinline|->| \lstinline|.| \\
+ unary & right & \lstinline|!| \lstinline|~| \lstinline|+|
+ \lstinline|-| \lstinline|*| \lstinline|&| \lstinline|(cast)|
+ \lstinline|sizeof| \\
+ multiplicative & left & \lstinline|*| \lstinline|/| \lstinline|%| \\
+ additive & left & \lstinline|+| \lstinline|-| \\
+ shift & left & \lstinline|<<| \lstinline|>>| \\
+ comparison & left & \lstinline|<| \lstinline|<=| \lstinline|>| \lstinline|>=| \\
+ comparison & left & \lstinline|==| \lstinline|!=| \\
+ bitwise and & left & \lstinline|&| \\
+ bitwise xor & left & \lstinline|^| \\
+ bitwise or & left & \lstinline+|+ \\
+ bitwise implies & left & \lstinline+-->+ \\
+ bitwise equiv & left & \lstinline+<-->+ \\
+ connective and & left & \lstinline|&&| \\
+ connective xor & left & \lstinline+^^+ \\
+ connective or & left & \lstinline+||+ \\
+ connective implies & right & \lstinline|==>| \\
+ connective equiv & left & \lstinline|<==>| \\
+ ternary connective & right & \lstinline|$\cdots$?$\cdots$:$\cdots$| \\
+ binding & left & \Forall{} \Exists{} \Let{} \\
+ naming & right & \lstinline|:| \\
+ \hline
+ \end{tabular}
+ \end{center}
+ \caption{Operator precedence}
+\label{fig:precedence}
+\end{figure}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Semantics}
+\label{sec:semantics}
+
+\except{undefinedness and same laziness than \C}
+
+More precisely, while \acsl is a 2-valued logic with only total
+functions, \eacsl is a 3-valued logic with partial functions since
+terms and predicates may be ``undefined''.
+
+In this logic, the semantics of a term denoting a \C expression $e$ is undefined
+if $e$ leads to a runtime error. Consequently the semantics of any term $t$
+(resp. predicate $p$) containing a \C expression $e$ leading to a runtime error
+is undefined if $e$ has to be evaluated in order to evaluate $t$ (resp. $p$).
+\begin{remark}[Julien]
+$e$ always terminates, thus no termination issue.
+\end{remark}
+\begin{example}
+The semantics of all the below predicates are undefined:
+\begin{itemize}
+\item \lstinline|1/0 == 1/0|
+\item \lstinline|f(*p)| for any logic function \lstinline|f| and invalid pointer
+ \lstinline|p|
+\end{itemize}
+\end{example}
+
+Furthermore, \C-like operators \lstinline|&&|, \lstinline+||+, \lstinline|^^|
+and \lstinline|_ ? _ : _| are lazy like in \C: their right members are evaluated
+only if required. Thus the amount of undefinedness is limited. Consequently,
+predicate \lstinline|p ==> q| is also lazy since it is equivalent
+to \lstinline+!p || q+. It is also the case for guarded quantifications since
+guards are conjunctions and for ternary condition since it is equivalent to a
+disjunction of implications.
+
+\begin{example}\label{ex:semantics}
+Below, the first, second and fourth predicates are invalid while the third
+one is valid:
+\begin{itemize}
+\item \lstinline|\false && 1/0 == 1/0|
+\item \lstinline|\forall integer x, -1 <= x <= 1 ==> 1/x > 0|
+\item \lstinline|\forall integer x, 0 <= x <= 0 ==> \false ==> -1 <= 1/x <= 1|
+\item \lstinline|\exists integer x, 1 <= x <= 0 && -1 <= 1/x <= 1|
+\end{itemize}
+In particular, the second one is invalid since the quantification is in fact an
+enumeration over a finite number of elements, it amounts to
+\lstinline|1/-1 > 0 && 1/0 > 0 && 1/1 > 0|. The first atomic proposition is
+invalid, so the rest of the conjunction (and in particular 1/0) is not
+evaluated. The fourth one is invalid since it is an existential quantification
+over an empty range.
+
+\emph{A contrario} the semantics of predicates below is undefined:
+\begin{itemize}
+\item \lstinline|1/0 == 1/0 && \false|
+\item \lstinline|-1 <= 1/0 <= 1 ==> \true|
+\item \lstinline|\exists integer x, -1 <= x <= 1 && 1/x > 0 |
+\end{itemize}
+\end{example}
+
+Furthermore, casting a term denoting a \C expression $e$ to a smaller type
+$\tau$ is undefined if $e$ is not representable in $\tau$.
+
+\begin{example}
+Below, the first term is well-defined, while the second one is undefined.
+\begin{itemize}
+\item \lstinline|(char)127|
+\item \lstinline|(char)128|
+\end{itemize}
+\end{example}
+
+\paragraph{Handling undefinedness in tools}
+
+\notimplemented{It is the responsibility of the tools which interprets \eacsl
+ to ensure that an undefined term is never evaluated. For instance, they may
+ exit with a proper error message or, if they generate \C code, they may guard
+ each generated undefined \C expression in order to be sure that they are
+ always safely used.}
+
+This behavior is consistent with both \acsl~\cite{acsl} and mainstream
+specification languages for runtime assertion checking like
+\jml~\cite{jml}. Consistency means that, if it exists and is defined, the \eacsl
+predicate corresponding to a valid (resp. invalid) \acsl predicate is valid
+(resp. invalid). Thus it is possible to reuse tools interpreting \acsl like the
+\framac's value analysis plug-in~\cite{value} in order to interpret \eacsl, and
+it is also possible to perform runtime assertion checking of \eacsl predicates
+in the same way than \jml predicates. Reader interested by the implications
+(especially issues) of such a choice may read articles of Patrice
+Chalin~\cite{chalin05,chalin07}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Typing}\label{sec:typing}
+\except{no user-defined types}
+
+It is not possible to define logic types introduced by the specification writer
+(see Section~\ref{sec:logicspec}).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Integer arithmetic and machine integers}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Real numbers} and floating point numbers}
+\nodiff
+
+\difficults{\notimplemented{Exact real numbers} and even floating point numbers}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{C arrays and pointers}
+\nodiff
+
+\difficultwhy{\notimplemented{Ensuring validity of memory accesses}}{the
+ implementation of a memory model}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Structures, Unions and Arrays in logic}
+\nodiff
+
+\difficults{\notimplemented{Logic arrays} without an explicit length}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{String literals}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Function contracts}
+\label{sec:fn-behavior}
+\index{function contract}\index{contract}
+
+\except{no \lstinline|terminates| and \lstinline|abrupt| clauses}
+
+Figure~\ref{fig:gram:contracts} shows grammar of function
+contracts. This is a simplified version of \acsl one without
+\lstinline|terminates| and \lstinline|abrupt|
+clauses. Section~\ref{sec:termination} (resp.~\ref{sec:abrupt}) explains why
+\eacsl has no \lstinline|terminates| (resp. \lstinline|abrupt|) clause.
+
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{fn_behavior_modern.bnf}
+ \end{cadre}
+ \caption{Grammar of function contracts}
+ \label{fig:gram:contracts}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Built-in constructs %
+ \texorpdfstring{\old}{\textbackslash{}old} %
+ and \texorpdfstring{\result}{\textbackslash{}result}}
+\label{sec:builtinconstructs}
+
+\nodiff
+
+Figure~\ref{fig:gram:oldandresult} summarizes grammar extension of terms with
+\lstinline|\old| and \lstinline|\result|.
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{oldandresult_modern.bnf}
+ \end{cadre}
+ \caption{\protect\old and \protect\result in terms}
+ \label{fig:gram:oldandresult}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Simple function contracts}
+\label{sec:simplecontracts}
+
+\nodiff
+
+\difficultwhy{\notimplemented{\lstinline|\\assigns|}}{the implementation of a
+ memory model}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Contracts with named behaviors}
+\label{subsec:behaviors}
+\index{function behavior}\index{behavior}
+
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Memory locations and sets of terms}
+\label{sec:locations}
+
+\except{\notimplemented{ranges and set comprehensions} are limited in order to
+ be finite}
+
+Figure~\ref{fig:gram:locations} describes grammar of sets of terms. The only
+differences with \acsl are that both lower and upper bounds of ranges are
+mandatory and that the predicate inside set comprehension must be guarded and
+bind only one variable. In that way, each set of terms is finite and their
+members easily identifiable.
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\textwidth}
+ \input{loc_modern.bnf}
+ \end{minipage}}
+ \caption{Grammar for sets of terms}
+\label{fig:gram:locations}
+\end{figure}
+
+\begin{notimplementedenv}
+\begin{example}
+The set \lstinlineµ{ x | integer x; 0 <= x <= 9 && 20 <= x <= 29 }µ denotes the
+set of all integers between 0 and 9 and between 20 and 29.
+\end{example}
+\end{notimplementedenv}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Default contracts, multiple contracts}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Statement annotations}
+\index{annotation}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Assertions}
+\label{sec:assertions}
+\indextt{assert}
+\nodiff
+
+Figure~\ref{fig:gram:assertions} summarizes grammar for assertions.
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{assertions_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for assertions}
+ \label{fig:gram:assertions}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Loop annotations}
+\label{sec:loop_annot}
+
+\except{\notimplemented{loop invariants} lose their inductive nature}
+
+Figure~\ref{fig:gram:loops} shows grammar for loop annotations. There is no
+syntactic difference with \acsl.
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{loops_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for loop annotations}
+ \label{fig:gram:loops}
+\end{figure}
+
+\difficultwhy{\notimplemented{\lstinline|loop assigns|}}{the implementation of a
+ memory model}
+
+\subsubsection{\notimplemented{Loop invariants}}
+
+\index{invariant} The semantics of \notimplemented{loop invariants} is the same
+than the one defined in \acsl, except that they are not inductive. More
+precisely, if one does not take care of side effects (semantics of
+specifications about side effects in loop is the same in \eacsl than the one in
+\acsl), a loop invariant $I$ is valid in \acsl if and only if:
+\begin{itemize}
+\item $I$ holds before entering the loop; and
+\item if $I$ is assumed true in some state where the loop condition $c$ is also
+ true, and if execution of the loop body in that state ends normally at the end
+ of the body or with a "continue" statement, $I$ is true in the resulting
+ state.
+\end{itemize}
+
+In \eacsl, the same loop invariant $I$ is valid if and only if:
+\begin{itemize}
+\item $I$ holds before entering the loop; and
+\item if execution of the loop body in that state ends normally at the end of
+ the body or with a "continue" statement, $I$ is true in the resulting state.
+\end{itemize}
+
+Thus the only difference with \acsl is that \eacsl does not assume that the
+invariant previously holds when one checks that it holds at the end of the loop
+body. In other words a loop invariant \lstinline|I| is equivalent to put an
+assertion \lstinline|I| just before entering the loop and at the very end of the
+loop body.
+
+\begin{example}
+In the following, \lstinline|bsearch(t,n,v)| searches for element \lstinline|v|
+in array \lstinline|t| between indices \lstinline|0| and \lstinline|n-1|.
+
+\cinput{bsearch.c}
+
+In \eacsl, this annotated function is equivalent to the following one since
+loop invariants are not inductive.
+
+\cinput{bsearch2.c}
+
+\end{example}
+
+\subsubsection{General inductive invariant}
+
+Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
+\begin{figure}[t]
+ \begin{cadre}
+ \input{generalinvariants_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for general inductive invariants}
+ \label{fig:advancedinvariants}
+\end{figure}
+
+In \eacsl, these kinds of invariants put everywhere in a loop body is exactly
+equivalent to an assertion.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Built-in construct \texorpdfstring{\at}{\textbackslash{}at}}
+\label{sec:at}\indexttbs{at}
+
+\except{no forward references}
+
+The construct \verb|\at(t,id)| (where \verb|id| is a regular C label, a label
+added within a \notimplemented{ghost statement} or a default logic label)
+follows the same rule than its \acsl counterpart, except that a more restrictive
+scoping rule must be respected in addition to the standard \acsl scoping rule:
+when evaluating \verb|\at(t,id)| at a propram point $p$, the program point $p'$
+denoted by \verb|id| must be executed after $p$ the program execution flow.
+
+\begin{example}
+In the following example, both assertions are accepted and valid in \acsl, but
+only the first one is accepted and valid in \eacsl since evaluating the term
+\verb|\at(*(p+\at(*q,Here)),L1)| at \verb|L2| requires to evaluate the term
+ \verb|\at(*q,Here)| at \verb|L1|: that is forbidden since \verb|L1| is executed
+ before \verb|L2|.
+\cinput{at.c}
+
+\end{example}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Statement contracts}
+\label{sec:statement_contract}
+\index{statement contract}\index{contract}
+
+\except{no \lstinline|abrupt| clauses}
+
+Figure~\ref{fig:gram:contracts} shows grammar of statement contracts. Like
+function contracts, this is a simplified version of \acsl with no
+\lstinline|abrupt| clauses. All other constructs are unchanged.
+
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{st_contracts_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for statement contracts}
+ \label{fig:gram:stcontracts}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Termination}
+\label{sec:termination}
+\index{termination}
+
+\except{no \lstinline|terminates| clauses}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Integer measures}}
+\label{sec:integermeasures}
+\indexttbs{decreases}\indexttbs{variant}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{General measures}}
+\label{sec:generalmeasures}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Recursive function calls}}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Non-terminating functions}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Logic specifications}
+\label{sec:logicspec}
+\index{logic specification}\index{specification}
+
+\limited{stable and computable features}
+
+Figure~\ref{fig:gram:logic} presents grammar of logic definitions. This is the
+same than the one of \acsl without polymorphic definitions, lemmas, nor
+axiomatics.
+
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\linewidth}\vfill \input{logic_modern.bnf}
+ \vfill\end{minipage}}
+ \caption{Grammar for global logic definitions}
+\label{fig:gram:logic}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Predicate and function definitions}}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Lemmas}
+\absentwhy{lemmas are user-given propositions. They are written usually to help
+ theorem provers to establish validity of specifications. Thus they are mostly
+ useful for verification activities based on deductive methods which are out of
+ the scope of \eacsl. Furthermore, they often requires human help to be proven,
+ although \eacsl targets are automatic tools}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Inductive predicates}\label{sec:inductive}
+\absentwhy{inductive predicates are not computable if they really use their
+ inductive nature}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Axiomatic definitions}
+\absentwhy{by nature, an axiomatic is not computable}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Polymorphic logic types}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Recursive logic definitions}}
+\index{recursion}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Higher-order logic constructions}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Concrete logic types}\label{sec:concrete-logic-types}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Hybrid functions and predicates}}
+\label{sec:logicalstates}
+\index{hybrid!function}
+\index{hybrid!predicate}
+\nodiff
+
+\difficultswhy{\notimplemented{Hybrid functions and predicates}}{the
+ implementation of a memory model (or at least to support \lstinline|\\at|)}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Memory footprint specification: \texorpdfstring{\lstinline|reads|}{reads} clause}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Specification Modules}}
+\label{sec:specmodules}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Pointers and physical adressing}
+\label{sec:pointers}
+
+\except{separation, allocation and deallocation is unsupported}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Memory blocks and pointer dereferencing}
+\label{subsec:memory}
+\nodiff
+
+\difficultswhy{\notimplemented{\lstinline|\\base\_addr|,
+ \lstinline|\\block\_length|, \lstinline|\\valid| and
+ \lstinline|\\offset|}}{the implementation of a memory model}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Separation}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Allocation and deallocation}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Sets as first-class values}
+\index{location}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Abrupt termination}\label{sec:abrupt}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Dependencies information}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{\notimplemented{Data invariants}}
+\label{sec:invariants}
+\index{data invariant}\index{global invariant}\index{type invariant}
+\index{invariant!data}\index{invariant!global}\index{invariant!type}
+
+\nodiff
+
+Figure~\ref{fig:gram:datainvariants} summarizes grammar for declarations of data
+invariants.
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\linewidth}
+ \input{data_invariants_modern.bnf}
+ \end{minipage}}
+ \caption{Grammar for declarations of data invariants}
+\label{fig:gram:datainvariants}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Semantics}
+\nodiff
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{\notimplemented{Model variables and model fields}}
+\index{model}
+
+\nodiff
+
+Figure~\ref{fig:gram:model} summarizes grammar for declarations of model
+variables and fields.
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\linewidth}
+ \input{model_modern.bnf}
+ \end{minipage}}
+ \caption{Grammar for declarations of model variables and fields}
+\label{fig:gram:model}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{\notimplemented{Ghost variables and statements}}
+\label{sec:ghost}
+\index{ghost}
+
+\except{no specific construct for volatile variables}
+
+Figure~\ref{fig:gram:ghost} summarizes grammar for ghost statements which is the
+same than the one of \acsl.
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.98\linewidth}
+ \input{ghost_modern.bnf}
+ \end{minipage}}
+ \caption{Grammar for ghost statements}
+\label{fig:gram:ghost}
+\end{figure}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Volatile variables}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Undefined values, dangling pointers}
+\nodiff
+
+\difficultswhy{\notimplemented{\lstinline|\\initialized| and
+ \lstinline|\\specified|}}{the implementation of a memory model}
diff --git a/src/plugins/e-acsl/doc/refman/st_contracts.tex b/src/plugins/e-acsl/doc/refman/st_contracts.tex
new file mode 100644
index 0000000000000000000000000000000000000000..7e574f5690e265a62b7c218c0d00b9928894e779
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/st_contracts.tex
@@ -0,0 +1,6 @@
+\begin{syntax}
+ statement ::= "/*@" statement-contract "*/" statement
+ \
+ [ statement-contract ] ::= {("for" id ("," id)* ":")?} requires-clause* ;
+ simple-clause* behavior-body*
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/support/MakeLaTeXModern b/src/plugins/e-acsl/doc/refman/support/MakeLaTeXModern
new file mode 100644
index 0000000000000000000000000000000000000000..d1b204a14b1ea83265f8686f43d31cfa3f116629
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/support/MakeLaTeXModern
@@ -0,0 +1,25 @@
+FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
+
+frama-c-book.cls: ../frama-c-book.cls
+ @rm -f $@
+ @cp $< .
+ @chmod a-w $@
+ @echo "import $<"
+
+frama-c-cover.pdf: ../frama-c-cover.pdf
+ @rm -f $@
+ @cp $< .
+ @chmod a-w $@
+ @echo "import $<"
+
+frama-c-right.pdf: ../frama-c-right.pdf
+ @rm -f $@
+ @cp $< .
+ @chmod a-w $@
+ @echo "import $<"
+
+frama-c-left.pdf: ../frama-c-left.pdf
+ @rm -f $@
+ @cp $< .
+ @chmod a-w $@
+ @echo "import $<"
diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex
new file mode 100644
index 0000000000000000000000000000000000000000..aad67173b9b88acafb3efecb3ab67f46b9abde78
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -0,0 +1,33 @@
+\begin{syntax}
+ bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ];
+ | "==" | "!=" | "<=" | ">=" | ">" | "<" ;
+ | [ "&&" ] | [ "||" ] | ; boolean operations
+ | { "&" } | { "|" } | { "-->" }
+ | { "<-->" } | { "^" } ; bitwise operations
+ \
+ unary-op ::= "+" | "-" ; unary plus and minus
+ | "!" ; boolean negation
+ | "~" ; bitwise complementation
+ | [ "*" ]; pointer dereferencing
+ | "&" ; address-of operator
+ \
+ term ::= { "\true" } | { "\false" };
+ | integer ; integer constants
+ | { real } ; real constants
+ | id ; variables
+ | unary-op term ;
+ | term bin-op term ;
+ | term "[" term "]" ; array access
+ | { "{" term "\with" "[" term "]" "=" term "}" } ; array functional modifier
+ | term "." id ; structure field access
+ | { "{" term "\with" "."id "=" term "}" } ; field functional modifier
+ | term "->" id ;
+ | [ "(" type-expr ")" term ] ; cast
+ | { id "(" term ("," term)* ")" } ; function application
+ | "(" term ")" ; parentheses
+ | [ term "?" term ":" term ] ; ternary condition
+ | { "\let" id "=" term ";" term } ; local binding
+ | "sizeof" "(" term ")" ;
+ | "sizeof" "(" C-type-expr ")" ;
+ | id ":" term ; syntactic naming
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/transf.mll b/src/plugins/e-acsl/doc/refman/transf.mll
new file mode 100644
index 0000000000000000000000000000000000000000..c56692b20e37edb33519844e84a1a84d6c96675a
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/transf.mll
@@ -0,0 +1,169 @@
+(* $Id: transf.mll,v 1.11 2009-03-03 09:53:08 uid562 Exp $ *)
+
+{ open Lexing;;
+ let idx = Buffer.create 5
+ let full_kw = Buffer.create 5
+
+ let modern = ref false
+
+ let escape_keyword s =
+ let buf = Buffer.create 5 in
+ String.iter
+ (function
+ c when ('A' <= c && c <= 'Z') ||
+ ('a' <= c && c <= 'z') ||
+ ('0' <= c && c <= '9')
+ -> Buffer.add_char buf c
+ | c -> Buffer.add_string buf
+ (Printf.sprintf "\\char%d" (int_of_char c))) s;
+ Buffer.contents buf
+
+ let make_keyword () =
+ let keyword = Buffer.contents full_kw in
+ let index = Buffer.contents idx in
+ print_string "\\addspace";
+ if !modern then
+ Printf.printf
+ "\\lstinline$%s$" keyword
+ else
+ Printf.printf "\\texttt{%s}" (escape_keyword keyword);
+ if index <> "" then
+ Printf.printf "\\indextt%s{%s}"
+ (if keyword.[0] = '\\' then "bs" else "") index;
+ print_string "\\spacetrue";
+ Buffer.clear idx;
+ Buffer.clear full_kw
+}
+
+rule main = parse
+ "\\begin{syntax}" {
+ print_string "\\begin{syntax}";
+ syntax lexbuf }
+ | "\\@" {
+ print_string "@";
+ main lexbuf }
+ | _ {
+ print_char (lexeme_char lexbuf 0); main lexbuf }
+ | eof {
+ () }
+
+and syntax = parse
+ "\\end{syntax}" {
+ print_string "\\end{syntax}";
+ main lexbuf }
+ | ";" ([^ '\n']* as s) '\n' [' ''\t']* '|' {
+ print_string "& \\textrm{";
+ print_string s;
+ print_string "} \\alt{}";
+ syntax lexbuf }
+ | ";" ([^ '\n']* as s) '\n' [' ''\t']* '\\' [' ''\t']* '\n' {
+ print_string "& \\textrm{";
+ print_string s;
+ print_string "} \\sep{}";
+ syntax lexbuf }
+ | ";" ([^ '\n']* as s) '\n' {
+ print_string "& \\textrm{";
+ print_string s;
+ print_string "} \\newl{}";
+ syntax lexbuf }
+ | "@" {
+ print_string "}";
+ main lexbuf }
+ | '\'' {
+ Buffer.clear idx;
+ Buffer.clear full_kw;
+ inquote lexbuf }
+ | '"' {
+ Buffer.clear idx;
+ Buffer.clear full_kw;
+ indoublequote lexbuf }
+ | "below" { print_string "\\below"; syntax lexbuf }
+ | "epsilon" { print_string "\\emptystring"; syntax lexbuf }
+ | ['A'-'Z''a'-'z''-'] + {
+ print_string "\\nonterm{";
+ print_string (lexeme lexbuf);
+ print_string"}";
+ check_nonterm_note lexbuf }
+ | '\\' ['a'-'z''A'-'Z'] + {
+ print_string (lexeme lexbuf);
+ syntax lexbuf }
+ | ['_' '^'] _ {
+ print_string (lexeme lexbuf);
+ syntax lexbuf }
+ | "*" { print_string "\\repetstar{}"; syntax lexbuf }
+ | "+" { print_string "\\repetplus{}"; syntax lexbuf }
+ | "?" { print_string "\\repetone{}"; syntax lexbuf }
+ | "(" { print_string "\\lparen{}"; syntax lexbuf }
+ | ")" { print_string "\\rparen{}"; syntax lexbuf }
+ | "::=" { print_string "\\is{}"; syntax lexbuf }
+ | "|" { print_string "\\orelse{}"; syntax lexbuf }
+ | "\\" { print_string "\\sep{}"; syntax lexbuf }
+ | "{" { print_string "\\begin{notimplementedenv}"; check_implementation_note lexbuf }
+ | "}" { print_string "\\end{notimplementedenv}"; syntax lexbuf }
+ | "[" { print_string "\\begin{markdiffenv}"; syntax lexbuf }
+ | "]" { print_string "\\end{markdiffenv}"; syntax lexbuf }
+ | _ {
+ print_char (lexeme_char lexbuf 0);
+ syntax lexbuf }
+
+and inquote = parse
+ ['A'-'Z' 'a'-'z' '0'-'9' '?'] as c {
+ Buffer.add_char full_kw c;
+ Buffer.add_char idx c;
+ inquote lexbuf }
+ | '\'' {
+ make_keyword ();
+ syntax lexbuf }
+ | '_' {
+ Buffer.add_char full_kw '_';
+ Buffer.add_string idx "\\_";
+ inquote lexbuf
+ }
+ | _ as c {
+ Buffer.add_char full_kw c;
+ inquote lexbuf }
+
+and indoublequote = parse
+ ['A'-'Z' 'a'-'z' '0'-'9' '?'] as c {
+ Buffer.add_char full_kw c;
+ Buffer.add_char idx c;
+ indoublequote lexbuf }
+ | '"' {
+ make_keyword();
+ syntax lexbuf }
+ | '_' {
+ Buffer.add_char full_kw '_';
+ Buffer.add_string idx "\\_";
+ indoublequote lexbuf
+ }
+ | _ as c {
+ Buffer.add_char full_kw c;
+ indoublequote lexbuf }
+and check_implementation_note = parse
+ | "[" { print_string "["; implementation_note lexbuf }
+ | "" { syntax lexbuf }
+and implementation_note = parse
+ "]" { print_string "]"; syntax lexbuf }
+ | _ { print_char (lexeme_char lexbuf 0);
+ implementation_note lexbuf }
+and check_nonterm_note = parse
+ | "[" { print_string "{"; nonterm_note lexbuf }
+ | "" { print_string "{}"; syntax lexbuf }
+and nonterm_note = parse
+ "]" { print_string "}"; syntax lexbuf }
+ | _ { print_char (lexeme_char lexbuf 0);
+ nonterm_note lexbuf }
+
+{
+
+ let () = Arg.parse
+ [ "-modern", Arg.Set modern, "set modern style"; ]
+ (fun f ->
+ let cin = open_in f in
+ let lb = from_channel cin in
+ main lb;
+ close_in cin)
+ "transf [-modern] file";
+ exit 0
+
+}
diff --git a/src/plugins/e-acsl/doc/refman/transfmain.ml b/src/plugins/e-acsl/doc/refman/transfmain.ml
new file mode 100644
index 0000000000000000000000000000000000000000..aa3bf1f0e3f0b57f4da9b3729c9f2b8c84552d39
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/transfmain.ml
@@ -0,0 +1,8 @@
+(* $Id: transfmain.ml,v 1.1 2007-05-29 08:23:19 uid562 Exp $ *)
+
+let main() =
+ let lexbuf = Lexing.from_channel stdin in
+ print_string "% automatically generated DO NOT EDIT\n";
+ Transf.main lexbuf; flush stdout; exit 0;;
+
+Printexc.print main ();;