diff --git a/.gitignore b/.gitignore
index 7b6e963424996402da1ae8c6ba24d04f5d3c5633..fccad8e706ba06202443d4e05fd631b2d1543d15 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,7 +82,6 @@ _build
 /doc/*/*.fls
 /doc/*/*.fdb_latexmk
 /doc/*/*.synctex.gz
-/doc/*/frama-c-affiliation.tex
 
 /doc/acsl/
 
diff --git a/doc/MakeLaTeXModern b/doc/MakeLaTeXModern
index 3ce60c391f19c7c56ae4c73e94dd7c02865343f4..2067d82c3aeb8c130d014fa6bc189bfad743f7a1 100644
--- a/doc/MakeLaTeXModern
+++ b/doc/MakeLaTeXModern
@@ -1,5 +1,5 @@
 FRAMAC_DOC_ROOT_DIR?=..
-FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf frama-c-affiliation.tex eu-flag.jpg anr-logo.png
+FRAMAC_MODERN=frama-c-book.cls fc-macros.tex eu-flag.jpg anr-logo.png logos
 
 frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
 	@rm -f $@
@@ -7,38 +7,26 @@ frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
 	@chmod a-w $@
 	@echo "import $<"
 
-frama-c-cover.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-cover.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-right.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-right.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-left.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-left.pdf
+eu-flag.jpg: $(FRAMAC_DOC_ROOT_DIR)/eu-flag.jpg
 	@rm -f $@
 	@cp $< .
 	@chmod a-w $@
 	@echo "import $<"
 
-frama-c-affiliation.tex: $(FRAMAC_DOC_ROOT_DIR)/frama-c-affiliation.tex
+anr-logo.png: $(FRAMAC_DOC_ROOT_DIR)/anr-logo.png
 	@rm -f $@
 	@cp $< .
 	@chmod a-w $@
 	@echo "import $<"
 
-eu-flag.jpg: $(FRAMAC_DOC_ROOT_DIR)/eu-flag.jpg
+fc-macros.tex: $(FRAMAC_DOC_ROOT_DIR)/fc-macros.tex
 	@rm -f $@
 	@cp $< .
 	@chmod a-w $@
 	@echo "import $<"
 
-anr-logo.png: $(FRAMAC_DOC_ROOT_DIR)/anr-logo.png
+logos: $(FRAMAC_DOC_ROOT_DIR)/logos
 	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
+	@ln -s $< $@
+	@chmod a-w $@/*
 	@echo "import $<"
diff --git a/doc/developer/.gitignore b/doc/developer/.gitignore
index 2a5270788248055f10119ae94c106e82f525eff7..13fff2e3450d4b314e878a4d3f3dcd841f201649 100644
--- a/doc/developer/.gitignore
+++ b/doc/developer/.gitignore
@@ -2,10 +2,8 @@
 /developer.pdf
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
-/frama-c-affiliation.tex
+/fc-macros.tex
+/logos
 /hello_world/
 /tutorial/viewcfg/generated/
 /examples/generated/
diff --git a/doc/developer/Makefile.config b/doc/developer/Makefile.config
index fc17098b3fd20bf615deaf6cbac24cc2f44749e4..ab8f24e4228fc9367450834087981ebcc3a2b92e 100644
--- a/doc/developer/Makefile.config
+++ b/doc/developer/Makefile.config
@@ -22,5 +22,5 @@
 
 MAKECONFIG_DIR=../../share
 include $(MAKECONFIG_DIR)/Makefile.common
-MAKEPDF ?= latexmk -pdf -quiet
+MAKEPDF ?= latexmk -pdf
 FRAMAC_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' ../../VERSION)
diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex
index 1c1be46cc0d7c1fb3df4bf3105ad3401d232078b..62e0d4c5b33ca3f774d86083439d872d927191f9 100644
--- a/doc/developer/developer.tex
+++ b/doc/developer/developer.tex
@@ -2,7 +2,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%MODERN \documentclass[a4paper,11pt,twoside,openright]{report}
-\documentclass[web,svgnames]{frama-c-book}
+\documentclass[svgnames]{frama-c-book}
 
 \usepackage{xspace,alltt,calc,multirow,tabularx,bigdelim,spverbatim}
 \usepackage{amsmath}
@@ -15,7 +15,6 @@
 \usepackage{framed}
 \usepackage{makeidx}
 \usepackage{graphicx}
-\usepackage{enumerate}
 \usepackage{longtable}
 \usepackage{varwidth}
 \usepackage{tikz}
@@ -30,36 +29,48 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \input{./macros.sty}
-\input{./frama-c-affiliation.tex}
 \makeindex
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{document}
-\sloppy
-\hbadness=10000
-
-\coverpage{Developer Manual}
-\begin{titlepage}
-\includegraphics[height=14mm]{../images/cealistlogo.jpg}
-\hfill~
-\vfill
-\title{Plug-in Development Guide}%
-{Release \framacversion}
+\title{Plug-in Development Guide}
 \author{Julien~Signoles with Thibaud~Antignac, Loïc~Correnson, Matthieu~Lemerre
 and Virgile~Prevosto}
-\begin{center}
-  \fcaffiliationen
-\end{center}
-\vfill
-\begin{flushleft}
-  \textcopyright 2009-{\the\year} CEA LIST
-\end{flushleft}
-\end{titlepage}
-
-%%Contents should open on right
-\cleardoublepage
-\markright{}
+
+\acknowledge{Michele Alberti}
+\acknowledge{Gergö Barany}
+\acknowledge{Patrick Baudin}
+\acknowledge{Allan Blanchard}
+\acknowledge{Richard Bonichon}
+\acknowledge{David B\"uhler}
+\acknowledge{Pascal Cuoq}
+\acknowledge{Zaynah Dargaye}
+\acknowledge{Basile Desloges}
+\acknowledge{Florent Garnier}
+\acknowledge{Pierre-Loïc Garoche}
+\acknowledge{Philippe Herrmann}
+\acknowledge{Boris Hollas}
+\acknowledge{Nikolaï Kosmatov}
+\acknowledge{Jean-Christophe Léchenet}
+\acknowledge{Romain Maliach-Auguste}
+\acknowledge{André Maroneze}
+\acknowledge{Benjamin Monate}
+\acknowledge{Yannick Moy}
+\acknowledge{Anne Pacalet}
+\acknowledge{Valentin Perrelle}
+\acknowledge{Armand Puccetti}
+\acknowledge{Muriel Roger}
+\acknowledge{Boris Yakobowski}
+
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+
+\copyrightstarts{2009}
+
+\begin{document}
+
+\maketitle
 \tableofcontents
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -90,48 +101,26 @@ and Virgile~Prevosto}
 
 This is the documentation of the \framac
 implementation\footnote{\url{http://frama-c.com}} which aims at
-helping developers integrate new plug-ins inside this platform. It started as
-a deliverable of the task 2.3 of the ANR RNTL project
-CAT\footnote{\url{http://www.rntl.org/projet/resume2005/cat.htm}}.
+helping developers integrate new plug-ins inside this platform.
 
-The content of this document corresponds to the version \framacversion,
-released on \today,
-of \framac. However the development of \framac is still ongoing: features
+The content of this document corresponds to the version \framacversion,released on \today,of \framac. However the development of \framac is still ongoing: features
 described here may still evolve in the future.
 
 \section*{Acknowledgements}
 %\addcontentsline{toc}{chapter}{Acknowledgements}
 
-We gratefully thank all the people who contributed to this document:
-Michele Alberti,
-Gergö Barany,
-Patrick Baudin,
-Allan Blanchard,
-Richard Bonichon,
-David B\"uhler,
-Pascal Cuoq,
-Zaynah Dargaye,
-Basile Desloges,
-Florent Garnier,
-Pierre-Loïc Garoche,
-Philippe Herrmann,
-Boris Hollas,
-Nikolaï Kosmatov,
-Jean-Christophe Léchenet,
-Romain Maliach-Auguste,
-André Maroneze,
-Benjamin Monate,
-Yannick Moy,
-Anne Pacalet,
-Valentin Perrelle,
-Armand Puccetti,
-Muriel Roger and
-Boris Yakobowski.
+\insertpeople
 
 We also thank Johannes Kanig for his \langage{Mlpost}
 support\footnote{\url{http://mlpost.lri.fr}}, the tool formerly used for
 making figures of this document.
 
+\medskip
+
+\acknowledgeANR{
+  the French ANR projects CAT~(ANR-05-RNTL-00301)
+}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \include{introduction}
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 076cf179d056e9744d2d08665863d6ae1ae6aff9..1a6e0debb5ffef55a4fff74512b1dd83d1afad71 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -52,8 +52,8 @@ platform. This tutorial focuses on specific parts of this figure.
 \savebox{\designbox}{\begin{varwidth}{\textwidth}\centering Design\\(GUI extension point)\end{varwidth}}
 \newlength{\designheight}
 \setlength{\designheight}{\totalheightof{\usebox\designbox}}
-\newsavebox{\captionbox}\savebox{\captionbox}{\textbf{Caption:}}
-\newlength{\captionheight}\settototalheight{\captionheight}{\captionbox}
+\newsavebox{\capbox}\savebox{\capbox}{\textbf{Caption:}}
+\newlength{\captionheight}\settototalheight{\captionheight}{\capbox}
 \begin{tikzpicture}[remember picture,txt/.style={inner xsep=3pt}]
   \node[inner sep=0pt] (implem) {
     \tikztitleboxbig{Plug-in\\implementation}{darkgreen}{
@@ -113,7 +113,7 @@ platform. This tutorial focuses on specific parts of this figure.
    \draw[Latex-] ($(registration.west)+(-\padding,0)$) -- +(-\bigpadding,0);
 
    \node[anchor=south east,xshift=-\padding] at (registration.north west)
-   {\usebox{\captionbox}};
+   {\usebox{\capbox}};
 
    \newlength{\kernelwidth}
    \setlength{\kernelwidth}{\widthof{Dynamic}}%TODO:compute dynamically
diff --git a/doc/eva/.gitignore b/doc/eva/.gitignore
index 4cb469371c39fba5dc990341e237f39aab91592c..29354296e97dd657cfc8f2f71d7d62b9b8d452b9 100644
--- a/doc/eva/.gitignore
+++ b/doc/eva/.gitignore
@@ -1,9 +1,6 @@
 /anr-logo.png
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
-/frama-c-affiliation.tex
 /main.pdf
-
+/logos
+/fc-macros.tex
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 038f0c4ab1bcce65b598a5ad004f6d01061004cc..ebe77d9085853588012dbdc10faab821e6a5370d 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -1,4 +1,4 @@
-\documentclass[web]{frama-c-book}
+\documentclass{frama-c-book}
 
 \usepackage{microtype}
 \usepackage{lmodern}
@@ -6,6 +6,8 @@
 \usepackage{calc}
 \usepackage{multirow}
 
+\input{fc-macros.tex}
+
 % Commandes pour mettre des ref dans l'index :
 \newcommand{\idb}[1]{\textbf{#1}}
 \newcommand{\indextxt}[1]{\index{#1}{\bf #1}}
@@ -23,52 +25,51 @@
 \definecolor{gris}{gray}{0.85}
 
 \makeatletter
-\newenvironment{important}%
-{\hspace{5pt plus \linewidth minus \marginparsep}%
- \begin{lrbox}{\@tempboxa}%
-   \begin{minipage}{\linewidth - 2\fboxsep}\itshape}
-{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
+\newenvironment{important}{\begin{colbox}{gris}}{\end{colbox}}
 \makeatother
 
 \newcommand{\framacversion}%
            {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
 \newcommand{\isoc}{\textsf{C99}}
 
-\newcommand{\Eva}{\textsf{Eva}}
-
-\input{./frama-c-affiliation.tex}
-
 \lstset{literate=%
 {∈}{{$\in$ }}1
 }
 
+\title{The \Eva{} plug-in}
+\author{David Bühler, Pascal Cuoq and Boris Yakobowski. \\
+With Matthieu Lemerre, André Maroneze,
+Valentin Perrelle and Virgile Prevosto}
+
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+\copyrightstarts{2011}
+
 %==============================================================================
 \begin{document}
 
-\coverpage{Eva – The Evolved Value Analysis plug-in}
+\maketitle
+\tableofcontents
 
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{The \Eva{} plug-in}{\framacversion}
-\author{David Bühler, Pascal Cuoq and Boris Yakobowski. \\
-  With Matthieu Lemerre, André Maroneze,
-  Valentin Perrelle and Virgile Prevosto}
-\begin{tabular}{l}
-  \fcaffiliationen
-\end{tabular}
-\vfill
-\begin{flushleft}
-  \textcopyright 2011-\the\year{} CEA LIST
-
-  This work has been supported by the ANR project U3CAT
-  (ANR-08-SEGI-021-01).
-\end{flushleft}
-\end{titlepage}
+\chapter*{Foreword}
+\markright{}
+\addcontentsline{toc}{chapter}{Foreword}
 
-\tableofcontents
+This is the documentation of the \FramaC plug-in \Eva.
+
+The content of this document corresponds to the version \framacversion, released
+on \today, of \FramaC. However the development of \FramaC is still ongoing:
+features described here may still evolve in the future.
+
+\section*{Acknowledgements}
+%\addcontentsline{toc}{chapter}{Acknowledgements}
+
+\medskip
+
+\acknowledgeANR{
+the French ANR projects U3CAT~(08-SEGI-021-01)
+}
 
 \chapter{Introduction}\label{introduction}
 \vspace{2cm}
@@ -673,7 +674,7 @@ We can then Ctrl+click on the loop condition in the original source view
   can be defined via the menu {\em File - Preferences}.} centered on the loop, and
 then add the loop unroll annotation, as follows:
 
-\begin{lstlisting}
+\begin{lstlisting}[style=c]
   //@ loop unroll 4;
   for (i=0;i < WCNT; i++)
       {
@@ -2288,7 +2289,7 @@ developing a custom plug-in.
 
 \chapter{Graphical interface (GUI)}\label{gui}
 \vspace{2cm}
-\include{gui}
+\input{gui}
 
 \chapter{Limitations and specificities}\label{limitations_specificities}
 \vspace{2cm}
diff --git a/doc/fc-macros.tex b/doc/fc-macros.tex
new file mode 100644
index 0000000000000000000000000000000000000000..4465fd6c753d2c97e76cf9bbf095ecad3f891c7e
--- /dev/null
+++ b/doc/fc-macros.tex
@@ -0,0 +1,158 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Date
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Useful for today's short date
+\def\shorttoday{\leavevmode\hbox{\the\year-\twodigits\month-\twodigits\day}}
+\def\twodigits#1{\ifnum#1<10 0\fi\the#1}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Indexed Keywords
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Frama-C plug-in names (e.g., \plugin{Eva})
+\newcommand{\plugin}[1]{\textsf{#1}\xspace}
+
+% Tools (e.g., \tool{Why3})
+\newcommand{\tool}[1]{\textsf{#1}\xspace}
+
+% Languages (e.g., \lang{ACSL}, \lang{C})
+\newcommand{\lang}[1]{\textsf{#1}\xspace}
+
+% Libraries (e.g., \library{Gmp})
+\newcommand{\library}[1]{\textsf{#1}\xspace}
+
+% Benchmarks (e.g, \benchmark{SpecCPU})
+\newcommand{\benchmark}[1]{\textsf{#1}\xspace}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frama-C Related Names
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\FramaC}{\tool{Frama-C}}
+\newcommand{\acsl}{\lang{ACSL}}
+\newcommand{\eacsllang}{\lang{E-ACSL}}
+
+% plug-ins
+\newcommand{\aorai}{\plugin{Aora\"i}}
+\newcommand{\cafe}{\plugin{CaFE}}
+\newcommand{\callgraph}{\plugin{Callgraph}}
+\newcommand{\constfold}{\plugin{Consfold}}
+\newcommand{\dive}{\plugin{Dive}}
+\newcommand{\dominators}{\plugin{Dominators}}
+\newcommand{\eacsl}{\plugin{E-ACSL}}
+\newcommand{\Eva}{\plugin{Eva}}
+\newcommand{\framaclang}{\plugin{Frama-Clang}}
+\newcommand{\from}{\plugin{From}}
+\newcommand{\GUI}{\plugin{GUI}}
+\newcommand{\impact}{\plugin{Impact}}
+\newcommand{\inout}{\plugin{InOut}}
+\newcommand{\instantiate}{\plugin{Instantiate}}
+\newcommand{\ltest}{\plugin{LTest}}
+\newcommand{\mdr}{\plugin{MdR}}
+\newcommand{\metacsl}{\plugin{MetAcsl}}
+\newcommand{\metrics}{\plugin{Metrics}}
+\newcommand{\nonterm}{\plugin{NonTerm}}
+\newcommand{\obfuscator}{\plugin{Obfuscator}}
+\newcommand{\occurrence}{\plugin{Occurrence}}
+\newcommand{\pathcrawler}{\plugin{PathCrawler}}
+\newcommand{\pdg}{\plugin{Pdg}}
+\newcommand{\pilat}{\plugin{Pilat}}
+\newcommand{\postdominators}{\plugin{Postdominators}}
+\newcommand{\printinterface}{\plugin{PrintInterface}}
+\newcommand{\reduction}{\plugin{Reduction}}
+\newcommand{\report}{\plugin{Report}}
+\newcommand{\rpp}{\plugin{RPP}}
+\newcommand{\rte}{\plugin{Rte}}
+\newcommand{\scope}{\plugin{Scope}}
+\newcommand{\secureflow}{\plugin{SecureFlow}}
+\newcommand{\securityslicing}{\plugin{SecuritySlicing}}
+\newcommand{\server}{\plugin{Server}}
+\newcommand{\slicing}{\plugin{Slicing}}
+\newcommand{\sparecode}{\plugin{SpareCode}}
+\newcommand{\stady}{\plugin{StaDy}}
+\newcommand{\studia}{\plugin{Studia}}
+\newcommand{\users}{\plugin{Users}}
+\newcommand{\variadic}{\plugin{Variadic}}
+\newcommand{\Wp}{\plugin{WP}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Standard Keywords
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Some programming languages
+\newcommand{\ada}{\lang{Ada}}
+\newcommand{\awk}{\lang{Awk}}
+\newcommand{\C}{\lang{C}}
+\newcommand{\coq}{\lang{Coq}}
+\newcommand{\Cpp}{\lang{C++}}
+\newcommand{\csharp}{\lang{C\#}}
+\newcommand{\dafny}{\lang{Dafny}}
+\newcommand{\dotnet}{\lang{.NET}}
+\newcommand{\eiffel}{\lang{Eiffel}}
+\newcommand{\fortran}{\lang{Fortran}}
+\newcommand{\isabelle}{\lang{Isabelle}}
+\newcommand{\java}{\lang{Java}}
+\newcommand{\javacard}{\lang{JavaCard}}
+\newcommand{\K}{\ensuremath{\mathbb{K}}}
+\newcommand{\ocaml}{\lang{OCaml}}
+\newcommand{\php}{\lang{PHP}}
+\newcommand{\python}{\lang{Python}}
+\newcommand{\smalltalk}{\lang{Smalltalk}}
+\newcommand{\spark}{\lang{Spark2014}}
+\newcommand{\vbnet}{\lang{VB.NET}}
+
+% Some modeling languages
+\newcommand{\lustre}{\lang{Lustre}}
+\newcommand{\scade}{\lang{Scade}}
+\newcommand{\simulink}{\lang{Simulink}}
+
+% Some specification languages
+\newcommand{\codecontract}{\lang{Code Contract}}
+\newcommand{\ltl}{\lang{LTL}}
+\newcommand{\jml}{\lang{JML}}
+\newcommand{\specsharp}{\lang{Spec\#}}
+\newcommand{\vcc}{\lang{VCC}}
+
+% Some libraries
+\newcommand{\cil}{\library{Cil}}
+\newcommand{\gtk}{\library{Gtk2}}
+\newcommand{\gtkt}{\library{Gtk3}}
+\newcommand{\gmp}{\library{Gmp}}
+\newcommand{\lablgtk}{\library{LablGtk2}}
+\newcommand{\lablgtkt}{\library{LablGtk3}}
+\newcommand{\libc}{\library{libc}}
+\newcommand{\libtomcrypt}{\library{LibTomCrypt}}
+
+% Some analysis and verification tools
+\newcommand{\addresssanitizer}{\tool{AddressSanitizer}}
+\newcommand{\aiT}{\tool{aiT}}
+\newcommand{\astree}{\tool{Astr\'ee}}
+\newcommand{\caduceus}{\tool{Caduceus}}
+\newcommand{\drmemory}{\tool{Dr.~Memory}}
+\newcommand{\insurepp}{\tool{Insure++}}
+\newcommand{\memcheck}{\tool{MemCheck}}
+\newcommand{\memorysanitizer}{\tool{MemorySanitizer}}
+\newcommand{\memsanitizer}{\tool{MemorySanitizer}}
+\newcommand{\openjml}{\tool{OpenJML}}
+\newcommand{\polyspace}{\tool{PolySpace}}
+\newcommand{\purify}{\tool{Purify}}
+\newcommand{\rvmatch}{\tool{RV-Match}}
+\newcommand{\stackanalyzer}{\tool{Stackanalyzer}}
+\newcommand{\threadsanitizer}{\tool{ThreadSanitizer}}
+\newcommand{\undefsanitizer}{\tool{UndefinedBehaviorSanitizer}}
+\newcommand{\valgrind}{\tool{Valgrind}}
+\newcommand{\verasco}{\tool{Verasco}}
+\newcommand{\why}{\tool{Why}}
+\newcommand{\whyt}{\tool{Why3}}
+
+% Some other tools
+\newcommand{\altergo}{\tool{Alt-Ergo}}
+\newcommand{\clang}{\tool{Clang}}
+\newcommand{\clousot}{\tool{Clousot}}
+\newcommand{\compcert}{\tool{CompCert}}
+\newcommand{\gcc}{\tool{Gcc}}
+\newcommand{\gdb}{\tool{gdb}}
+\newcommand{\git}{\tool{Git}}
+\newcommand{\llvm}{\tool{LLVM}}
+\newcommand{\opam}{\tool{opam}}
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 879f10eef8a61904ae416523a777feb8899c448f..6978714adb9ddcf454335b538b983290db96ec5c 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -1,379 +1,558 @@
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesClass{frama-c-book}
+
+\LoadClass[a4paper]{report}
+
+\RequirePackage[
+  left=.125\paperwidth,
+  right=.125\paperwidth,
+  top=.125\paperheight,
+  bottom=.125\paperheight
+]{geometry}
+\RequirePackage[dvipsnames,table]{xcolor}
+\RequirePackage{graphicx}
+\RequirePackage{xspace}
+\RequirePackage{anyfontsize}
+\RequirePackage{titletoc}
+\RequirePackage{titlesec}
+\RequirePackage[shortlabels]{enumitem}
+\RequirePackage{fancyhdr}
+\RequirePackage{lmodern}
+\RequirePackage{microtype}
+\RequirePackage{etoolbox}
+
+% Do I keep it there:
+\RequirePackage{babel}
+\RequirePackage[T1]{fontenc}
+\RequirePackage[utf8]{inputenc}
+\RequirePackage{amssymb}
+\RequirePackage{comment}
+
+
+\definecolor{frama-c-orange}{HTML}{F36521}
+\definecolor{frama-c-dark-orange}{HTML}{D04604}
+\definecolor{frama-c-bronze}{HTML}{F39D21}
+\definecolor{frama-c-green}{HTML}{16A371}
+\definecolor{frama-c-dark-green}{HTML}{0E6647}
+
+\RequirePackage[
+  pdftex,pdfstartview=FitH,
+  bookmarks=true,
+  hyperindex=true,
+  bookmarksopen=true,
+  bookmarksnumbered=true,
+  colorlinks=true,
+  allcolors={frama-c-dark-orange}
+]{hyperref}
+
 % --------------------------------------------------------------------------
-% ---  LaTeX Class for Frama-C Books                                     ---
+% CEA commands
 % --------------------------------------------------------------------------
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
-\newif\ifusecc
-\usecctrue
+
+\newcommand{\cealist}{CEA-List}
+\newcommand
+  {\fcaffiliationen}
+  {\cealist, Université Paris-Saclay\\ Software Safety and Security Lab\xspace}
+\newcommand
+  {\fcaffiliationfr}
+  {\cealist, Université Paris-Saclay\\ Laboratoire de Sûreté et Sécurité des Logiciels\xspace}
+
+\newcommand{\cealogo}{logos/cea_tech_list.jpg}
+
 % --------------------------------------------------------------------------
-% ---  Base Class management                                             ---
+% LICENSE commands
 % --------------------------------------------------------------------------
-\makeatletter
-\RequirePackage{kvoptions}
-\SetupKeyvalOptions{
-family=framacbook,
-prefix=framacbook@,
+
+\def\@licence{}
+\def\@licencelogo{}
+\def\@licencelink{}
+\newcommand{\licence}[3]{
+  \def\@licence{#1}
+  \def\@licencelogo{#2}
+  \def\@licencelink{#3}
+}
+\newcommand{\cclicence}[1]{
+  \licence
+    {Creative Commons \uppercase{#1}}
+    {logos/#1.png}
+    {\url{https://creativecommons.org/licenses/#1/4.0/}}
 }
-\RequirePackage{ifthen}
-\DeclareVoidOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
-\DeclareVoidOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
-\DeclareStringOption[{type=CC,version=4.0,modifier=by-sa}]{license}
-\DeclareStringOption[english]{lang}
-\DeclareDefaultOption{\PassOptionsToClass{\CurrentOption}{report}}
-\PassOptionsToClass{a4paper,11pt,twoside,openright}{report}
 
-\ProcessKeyvalOptions*
+% --------------------------------------------------------------------------
+% Copyright commands
+% --------------------------------------------------------------------------
 
-\LoadClass{report}
+\def\@copyrightfrom{}
+\newcommand{\copyrightstarts}[1]{
+  \def\@copyrightfrom{#1}
+}
 
-\PassOptionsToPackage{\framacbook@lang}{babel}
+\newcommand{\addcopyrightowner}[1]{
+  \listadd{\@copyrightowner}{#1}
+}
+\addcopyrightowner{CEA LIST} % add it by default
 
-\ifthenelse{\equal{\framacbook@license}{no}}{\useccfalse}{}
-\ifusecc
-  \PassOptionsToPackage{\framacbook@license}{doclicense}
-\fi
-\RequirePackage{babel}
-\RequirePackage{fullpage}
-\RequirePackage{lmodern}
-\RequirePackage[T1]{fontenc}
-\RequirePackage[utf8]{inputenc}
-\RequirePackage{amssymb}
-\RequirePackage[table]{xcolor}
-\RequirePackage[pdftex]{graphicx}
-\RequirePackage{ifthen}
-\RequirePackage{xspace}
-\RequirePackage{makeidx}
-\RequirePackage[leftbars]{changebar}
-\RequirePackage{fancyhdr}
-\RequirePackage{titlesec}
-\RequirePackage{upquote}
-\RequirePackage[pdftex,pdfstartview=FitH]{hyperref}
-\ifusecc\RequirePackage{doclicense}\else\fi
-% --------------------------------------------------------------------------
-% ---  Page Layout                                                       ---
-% --------------------------------------------------------------------------
-\setlength{\voffset}{-6mm}
-\setlength{\headsep}{8mm}
-\setlength{\footskip}{21mm}
-\setlength{\textheight}{238mm}
-\setlength{\topmargin}{0mm}
-\setlength{\textwidth}{155mm}
-\setlength{\oddsidemargin}{2mm}
-\setlength{\evensidemargin}{-2mm}
-\setlength{\changebarsep}{0.5cm}
-\setlength{\headheight}{13.6pt}
-\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
-  \begin{picture}(0,0)(#1,#2)
-    \put(0,0){\includegraphics[width=#3cm]{#4}}
-  \end{picture}}
-\fancypagestyle{plain}{%
-  \fancyfoot{}
-  \fancyhead{}
-  \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
-  \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
-  \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
-  \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
-  \fancyfoot[C]{\small\textsf{\thepage}}
-  \renewcommand{\headrulewidth}{0pt}
-  \renewcommand{\footrulewidth}{0pt}
-}
-\fancypagestyle{blank}{%
-  \fancyfoot{}
-  \fancyhead{}
-  \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
-  \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
-}
-%% Redefinition of cleardoublepage for empty page being blank
-\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
-\hbox{}
-\thispagestyle{#1}
-\newpage
-\fi\fi}
-\def\cleardoublepage{\cleardoublepagewith{blank}}
-\pagestyle{plain}
-
-% --------------------------------------------------------------------------
-% ---  Cover Page                                                        ---
-% --------------------------------------------------------------------------
-\newcommand{\coverpage}[1]{%
-\thispagestyle{empty}
-\setlength\unitlength{1cm}
-\begin{picture}(0,0)(3.27,26.75)
-\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
-\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
-\end{picture}
-}
-
-% --------------------------------------------------------------------------
-% ---  Title Page                                                        ---
-% --------------------------------------------------------------------------
-\renewenvironment{titlepage}%
-{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
-{\end{center}}
-\renewcommand{\title}[2]{
-\vspace{20mm}
-{\Huge\bfseries #1}
-
-\bigskip
-
-{\LARGE #2}
-\vspace{20mm}
-}
-\renewcommand{\author}[1]{
-\vspace{20mm}
-
-{#1}
-
-\medskip
-\ifusecc\doclicenseThis\else\fi
-}
-
-% \acknowledge{<flag image file>}{<text inside box>}
-\newcommand{\acknowledge}[2]{
-  \fbox{
-    \begin{minipage}{0.97\textwidth}
+\newcommand{\insertcopyrightowners}{{
+  \def\listsep{\def\listsep{, }}%
+  \renewcommand{\do}[1]{\listsep##1}%
+  \dolistloop\@copyrightowner
+}}
+
+\newcommand{\insertcopyright}{
+  \textcopyright\xspace \@copyrightfrom-\the\year{} \insertcopyrightowners
+}
+
+% --------------------------------------------------------------------------
+% Logos
+% --------------------------------------------------------------------------
+
+\def\@logos{}
+\newcommand{\addlogo}[1]{
+  \listadd{\@logos}{#1}
+}
+
+\newcommand{\insertlogos}{{
+  \def\listsep{\def\listsep{\hspace{2em}}}%
+  \renewcommand{\do}[1]{\listsep\includegraphics[height=7em]{##1}}%
+  \dolistloop\@logos
+}}
+
+% --------------------------------------------------------------------------
+% Subtitle
+% --------------------------------------------------------------------------
+
+\def\@subtitle{}
+
+\newcommand{\subtitle}[1]{
+  \def\@subtitle{#1}
+}
+
+% --------------------------------------------------------------------------
+% Frama-C commands
+% --------------------------------------------------------------------------
+
+\def\@fcversion{}
+\newcommand{\fcversion}[1]{
+  \subtitle{For Frama-C #1}
+}
+
+\def\fchrulefill{\leavevmode\leaders\hrule height 1.25pt\hfill\kern\z@}
+
+
+% --------------------------------------------------------------------------
+% Title page
+% --------------------------------------------------------------------------
+
+\renewcommand{\maketitle}{%
+  \newgeometry{top=1cm, bottom=1cm, right=1cm,left=1cm}
+  \thispagestyle{empty}
+  \noindent\includegraphics{logos/frama-c.png}
+
+  \vspace{12em}
+  \begin{center}
+    \textbf{\Huge\@title}
+
+    \medskip
+    \ifx\@subtitle\empty\else{
+      \Large \@subtitle
+    }\fi
+  \end{center}
+
+  \vspace{-1em}
+  {\noindent\color{frama-c-orange}\fchrulefill}
+
+  \begin{center}
+    \begin{minipage}{.8\textwidth}
+      \centering
+      \large\@author
+    \end{minipage}
+  \end{center}
+
+  \bigskip
+
+  \begin{center}
+    \insertlogos
+  \end{center}
+
+  \vfill
+
+  \noindent
+  \ifx\@licencelogo\empty
+  \else{
+  \begin{minipage}{.14\textwidth}
+    \includegraphics[height=25pt]{\@licencelogo}
+  \end{minipage}
+  \hfill
+  }
+  \fi
+  \begin{minipage}{.84\textwidth}
+    \vspace{.2em}
+    \ifx\@licence\empty
+    \else{\large Work licensed under \@licence\xspace licence}\fi\\
+    \ifx\@licencelink\empty
+    \else{\large\@licencelink}\fi
+  \end{minipage}
+  \medskip
+
+  \noindent\insertcopyright
+
+  \restoregeometry%
+
+  \cleardoublepage
+}
+
+% --------------------------------------------------------------------------
+% Table of contents
+% --------------------------------------------------------------------------
+
+\newcommand\tocdotfill{{\normalfont\normalsize \TOCLineLeaderFill}}
+
+\titlecontents{chapter}
+  [0em]
+  {\bigskip}
+  {\makebox[2em][l]{\thecontentslabel}\bfseries}
+  {\hspace*{2em}\bfseries}
+  {\space\hfill\makebox[1.5em]{\contentspage}}[]
+
+\titlecontents{section}
+  [2em]
+  {\medskip}
+  {\makebox[3em][l]{\thecontentslabel}}
+  {\hspace*{3em}}
+  {\space\tocdotfill\makebox[1.5em]{\contentspage}}[]
+
+\titlecontents{subsection}
+  [5em]
+  {\smallskip}
+  {\makebox[4.5em][l]{\thecontentslabel}}
+  {\hspace*{4.5em}}
+  {\space\tocdotfill\makebox[1.5em]{\contentspage}}[]
+
+% --------------------------------------------------------------------------
+% Acknoledgements
+% --------------------------------------------------------------------------
+
+\def\@people{}
+\newcommand{\acknowledge}[1]{
+  \listadd{\@people}{#1}
+}
+
+\def\@anrprojects{}
+\newcommand{\acknowledgeANRproject}[1]{
+  \listadd{\@anrprojects}{#1}
+}
+
+\def\@euprojects{}
+\newcommand{\acknowledgeEUproject}[1]{
+  \listadd{\@euprojects}{#1}
+}
+
+\newcommand{\commaorandlist}[1]{%
+  \count255=0
+  \def\do##1{\advance\count255 1 \chardef\finalitem=\count255 }%
+  \dolistloop{#1}%
+  \count255=0
+  \def\do##1{\advance\count255 1
+    \ifnum\count255=\finalitem
+      \space and\space
+    \else
+      \ifnum\count255=1\else,\space\fi
+    \fi##1}
+  \dolistloop{#1}}
+
+\newcommand{\insertpeople}{{
+  \ifx\@people\empty\else
+  {We gratefully thank all the people who contributed to this document: \commaorandlist\@people.}
+  \fi
+}}
+
+
+% \acknowledgeprogram{<flag image file>}{<text inside box>}
+\newcommand{\acknowledgeprogram}[2]{
+  \noindent\fbox{
+    \begin{minipage}{.97\textwidth}
       \begin{minipage}{1.2cm}
         \includegraphics[width=\linewidth]{#1}
       \end{minipage}
-      \begin{minipage}{0.90\textwidth}
+      \hfill
+      \begin{minipage}{0.9\textwidth}
         This project has received funding from #2.
       \end{minipage}
     \end{minipage}
   }
 }
 
-\newcommand{\acknowledgeANR}{
-  \acknowledge{anr-logo.png}{the French ANR projects
-    CAT~(ANR-05-RNTL-00301) and U3CAT~(08-SEGI-021-01)
-  }
+\newcommand{\acknowledgeANR}[1]{
+  \acknowledgeprogram{anr-logo.png}{#1}
 }
 
-\newcommand{\acknowledgeEU}{
-  \acknowledge{eu-flag.jpg}{the
-    European Union's Seventh Framework Programme (FP7/2007-2013)
-    under grant agreement N$^\circ$\,317753 (\mbox{STANCE}).\\
-    It has also received funding from the Horizon 2020 research
-    and innovation programme, under grant agreements
-    N$^\circ$\,731453~(\mbox{VESSEDIA}),
-    N$^\circ$\,824231~(\mbox{DECODER}),
-    N$^\circ$\,830892~(\mbox{SPARTA}),
-    and N$^\circ$\,883242~(\mbox{ENSURESEC})
-  }
+\newcommand{\acknowledgeEU}[1]{
+  \acknowledgeprogram{eu-flag.jpg}{#1}
 }
 
 % --------------------------------------------------------------------------
-% ---  Sectionning                                                       ---
+% Header
 % --------------------------------------------------------------------------
-\titleformat{\chapter}[display]{\Huge\raggedleft}%
-{\huge\chaptertitlename\,\thechapter}{0.5em}{}
-\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
-[\vspace{-14pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
-\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
-[\vspace{-8pt}]
+
+\pagestyle{fancy}
+\fancyhf{}
+\fancyhead[L]{\vspace{1.25em}\raggedleft\rightmark\vspace{-1.25em}}
+\fancyfoot[C]{\thepage}
+\renewcommand{\headrulewidth}{0pt}
 
 % --------------------------------------------------------------------------
-% ---  Main Text Style                                                   ---
+% Chapters
 % --------------------------------------------------------------------------
-%\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}
+
+\titleformat{\chapter}[display]
+  {\sc\Huge}
+  {\filleft\fontsize{50}{0}\selectfont\thechapter}
+  {-1.1em}
+  {\filright}
+  [\normalsize\vspace{-.5em}\color{frama-c-orange}\fchrulefill]
+
+\titleformat{\section}[hang]
+  {\Large\bfseries}
+  {\thesection}
+  {1em}
+  {}
+  [\vspace{-10pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
+
+\titlespacing*{\section}{0pt}{20pt}{20pt}
+
 % --------------------------------------------------------------------------
-% ---  Listings                                                          ---
+% Itemize style
 % --------------------------------------------------------------------------
+
+\renewcommand\labelitemi{--}
+\setitemize{noitemsep,topsep=5pt,parsep=0pt,partopsep=0pt}
+\setenumerate{noitemsep,topsep=5pt,parsep=0pt,partopsep=0pt}
+
+% --------------------------------------------------------------------------
+% Footnote style
+% --------------------------------------------------------------------------
+
+\renewcommand\footnoterule{%
+  \kern-3\p@%
+  {\color{frama-c-orange}\hrule\@width\columnwidth}%
+  \kern2.6\p@%
+}
+
+\renewcommand{\@makefntext}[1]{
+ \setlength{\parindent}{0pt}
+ \begin{list}{}{\setlength{\labelwidth}{1.5em}
+ \setlength{\leftmargin}{\labelwidth}
+ \setlength{\labelsep}{3pt}
+ \setlength{\itemsep}{0pt}
+ \setlength{\parsep}{0pt}
+ \setlength{\topsep}{3pt}
+ \footnotesize}
+ \item[\@makefnmark\hfil]#1
+ \end{list}
+}
+
+% --------------------------------------------------------------------------
+% Warning & information style
+% --------------------------------------------------------------------------
+
+\newsavebox{\fcsavebox}
+\newenvironment{colbox}[1]{%
+  \newcommand\colboxcolor{#1}%
+  \begin{lrbox}{\fcsavebox}%
+  \begin{minipage}{\dimexpr\columnwidth-2\fboxsep\relax}
+  \itshape
+}{%
+  \end{minipage}\end{lrbox}%
+  \begin{center}
+    \colorbox{\colboxcolor}{\usebox{\fcsavebox}}
+  \end{center}
+}
+
+\newenvironment{warning}{\begin{colbox}{frama-c-dark-orange!30}}{\end{colbox}}
+\newenvironment{information}{\begin{colbox}{frama-c-green!30}}{\end{colbox}}
+
+% --------------------------------------------------------------------------
+% Code
+% --------------------------------------------------------------------------
+
+\RequirePackage{scrhack} % avoids warning about \float@addtolists related to lstlisting
 \RequirePackage{listings}
+\RequirePackage{caption}
+\RequirePackage{accsupp}
 
-\lstdefinelanguage{ACSL}{%
-  morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
-    boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
-    exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
-    model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
-    union,variant},
-  keywordsprefix={\\},
-  alsoletter={\\},
-  morecomment=[l]{//}
+\newcommand{\noncopynumber}[1]{%
+  \BeginAccSupp{method=escape,ActualText={}}%
+  #1%
+  \EndAccSupp{}%
 }
 
-\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}
+\renewcommand{\ttdefault}{pcr} % so that keywords can be bold
+
+% CAPTION
+
+\DeclareCaptionFormat{listing}{
+  \raggedright\textbf{#1 #2} #3
+  \vspace{-2mm}
+  {\color{gray}\rule{\textwidth}{0.1pt}}
+}
+\DeclareCaptionLabelSeparator{listing}{--}
+\captionsetup[lstlisting]{format=listing,labelsep=listing}
+
+% Basic style
+% --------------------------------------------------------------------------
+
+\definecolor{lstnum}{gray}{0.3}
 \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{lstmodule}{rgb}{0.3,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\small\else\normalfont\ttfamily\mdseries\small\fi}
-\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
+
+\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\small\else\normalfont\ttfamily\mdseries\normalsize\fi}
+\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\normalsize\fi}
 \def\lp@keyword{}
-\def\lp@special{\color{lstfg}}
+\def\lp@special{\color{frama-c-dark-orange}}
 \def\lp@comment{\normalfont\ttfamily\mdseries}
-\def\lp@string{\color{lstfg}} \def\lp@ident{}
-\def\lp@number{\rmfamily\tiny\color{lstnum}}
+\def\lp@string{\color{frama-c-dark-green}} \def\lp@ident{}
+\def\lp@number{\rmfamily\tiny\color{lstnum}\noncopynumber}
+
 \lstdefinestyle{frama-c-style}{%
+  captionpos=b,%
   columns=flexible,%
   basicstyle=\lp@inline,%
   identifierstyle=\lp@ident,%
   commentstyle=\lp@comment,%
-  keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
-  keywordstyle=[2]\lp@special,%
+  keywordstyle={\bfseries\ifmmode\mathsf\else\ttfamily\fi\color{blue}},%
+  keywordstyle=[2]\bfseries\lp@special,%
   stringstyle=\lp@string,%
   emphstyle=\lp@ident\underbar,%
   showstringspaces=false,%
   numberstyle=\lp@number,%
-  xleftmargin=6ex,xrightmargin=2ex,%
+  xleftmargin=1.82em,%
   framexleftmargin=1ex,%
   frame=l,%
   framerule=1pt,%
-  rulecolor=\color{lstrule},%
-  backgroundcolor=\color{lstbg},%
+  rulecolor=\color{frama-c-orange!60},%
+  backgroundcolor=\color{frama-c-bronze!10},%
   moredelim={*[s]{/*@}{*/}},%
   moredelim={*[l]{//@}},%
   morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
   morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
   mathescape=true,
   escapechar=`,
-% breaklines is broken when using a inline and background
-%  breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
+  literate={\ }{\ }1
+  % ^~~~~  Without this, spaces starting a line does not have the right size ...
 }
 
+% Code styles
+% --------------------------------------------------------------------------
+
+\lstdefinestyle{framac-code-style}{%
+  basicstyle=\lp@inline,%
+  keywordstyle=[1]\sffamily\color{lstmodule},%
+  keywordstyle=[2]\sffamily\color{lstspecial},%
+  keywordstyle=[3]\sffamily\bfseries,%
+  identifierstyle=\rmfamily,%
+  stringstyle=\ttfamily\color{frama-c-orange},%
+  commentstyle=\rmfamily\bfseries\color{lsttxt},%
+}
+\lstdefinestyle{framac-shell-style}{%
+  mathescape=false,%
+  basicstyle=\lp@basic,%
+  keywordstyle=\sffamily\bfseries,%
+  keywordstyle=[1]\sffamily\color{lstmodule},%
+  keywordstyle=[2]\sffamily\color{lstspecial},%
+  keywordstyle=[3]\sffamily\bfseries,%
+  identifierstyle=\ttfamily,%
+  stringstyle=\ttfamily\color{frama-c-orange},%
+  commentstyle=\rmfamily\bfseries\color{lsttxt},%
+  literate={\\\$}{\$}1%
+  {€}{\textbackslash}1%
+,%
+}
+
+% ACSL + C
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{ACSL}{%
+	escapechar={},
+	literate=,
+	breaklines=false,
+	classoffset=1,
+	morekeywords={admit,allocates,assert,assigns,assumes,axiom,axiomatic,behavior,
+	  behaviors,boolean,breaks,check,complete,continues,data,decreases,disjoint,
+		ensures,exits,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
+	  model,predicate,reads,real,requires,sizeof,strong,struct,terminates,
+	  %returns,
+	  type,union,variant
+	  Here,LoopCurrent,LoopEntry,Pre,Post,Old,
+		\\at,\\allocable,\\base_addr,\\block_length,\\exists,\\false,\\forall,
+    \\freeable,\\fresh,\\from,\\initialized,\\nothing,\\numof,\\object_pointer,
+    \\offset,\\old,\\result,\\separated,\\sum,\\true,\\valid,\\valid_read},
+  classoffset=0,
+	alsoletter={\\},
+	morecomment=[l]{//}
+}
+
+\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
+
 \lstdefinestyle{c}%
 {language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
 \lstdefinestyle{c-basic}%
 {language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
 
-
-% --- C/ACSL Stuff ---------------------------------------------------------
-% Make 'c' the default style
-\lstset{style=c}
-
 \newcommand{\listinginput}[3][1]%
 {\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
-
 \newcommand{\listinginputcaption}[4][1]%
-{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}
+{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,caption={#3}]{#4}}
 
 \lstnewenvironment{listing}[2][1]%
 {\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
-
 \lstnewenvironment{listing-nonumber}%
 {\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
 
-% --- Verbatim Stuff -------------------------------------------------------
-\lstdefinelanguage{Shell}[]{csh}%
-{escapechar=@
- identifierstyle=\lp@basic,
- mathescape=false,
- backgroundcolor=,
- literate={\\\$}{\$}1
-}
+% ACSL + C (developers)
+% --------------------------------------------------------------------------
 
-\lstnewenvironment{shell}[1][]
-{\lstset{language=Shell,basicstyle=\lp@basic,#1}}
-{}
+\lstdefinestyle{framac-code}%
+{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
 
-% ---- 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}}
+\newcommand{\cinput}[2][]%
+{\lstinputlisting[
+    language={[ANSI]C},
+    alsolanguage=ACSL,
+    style=framac-code-style,basicstyle=
+    \lp@basic,#1]{#2}
+}
+\newcommand{\cinline}[1]%
+{\lstinline[style=framac-code]{#1}}
 
-% --------------------------------------------------------------------------
-% ---  Developer Code Stuff                                              ---
-% --------------------------------------------------------------------------
+\lstnewenvironment{ccode}[1][]%
+{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
 
-\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
+% Configure
+% --------------------------------------------------------------------------
 
-% --- 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%
-{€}{\textbackslash}1%
-,%
-}
-% --- Configure ------------------------------------------------------------
 \lstdefinelanguage{Configure}[]{csh}{%
-style=framac-shell-style,%
-morekeywords={fi},%
+  style=framac-shell-style,%
+  morekeywords={fi},%
 }
+
+\newcommand{\configureinput}[1]%
+{\lstinputlisting[language=Configure]{#1}}
+
 \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}[2][]%
-{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1]{#2}}
-\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%
-{€}{\textbackslash}1%
-{à}{{\`a}}1%
-{é}{{\'e}}1%
-}
-\lstdefinestyle{ocaml-basic}{
-  language=Ocaml,
-  basicstyle=\lp@basic
-}
+
+% Dune
+% --------------------------------------------------------------------------
 
 \lstdefinelanguage{Dune}{%
-literate=%
-{à}{{\`a}}1%
-{é}{{\'e}}1%
-,
+  literate=%
+    {à}{{\`a}}1%
+    {é}{{\'e}}1%
+  ,
   style=framac-code-style,%
   morekeywords={
     action, alias, as, deps, dune, executable, files, flags, from,
@@ -387,25 +566,112 @@ literate=%
   },
   morecomment=[l]{;},
 }
+
 \lstdefinestyle{dune-basic}{%
   language=Dune,%
   style=framac-code-style,%
   basicstyle=\lp@inline,%
 }
 
+\newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}}
+
+\lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{}
+
+% Logs
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{Logs}[]{csh}{%
+  identifierstyle=\lp@basic,%
+  backgroundcolor=
+}
+
+\newcommand{\logsinput}[1]%
+{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
+
+\lstnewenvironment{logs}[1][]%
+{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
+
+% Makefile
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{Makefile}[]{make}{%
+  style=framac-shell-style,%
+  morekeywords={include},%
+}
+
 \lstdefinestyle{make-basic}{%
   language=Makefile,%
   style=framac-code-style,%
   basicstyle=\lp@inline,%
 }
 
+\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
+\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}}
+
+\lstnewenvironment{makefilecode}[1][]%
+{\lstset{language=Makefile,#1}}{}
+
+\lstnewenvironment{makecode}[1][]%
+{\lstset{style=make-basic,#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%
+  {€}{\textbackslash}1%
+  {à}{{\`a}}1%
+  {é}{{\'e}}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}}{}
-\newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}}
-\lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{}
-\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}}
-\lstnewenvironment{makecode}[1][]{\lstset{style=make-basic,#1}}{}
+
+% Shell
+% --------------------------------------------------------------------------
+
+\lstdefinelanguage{Shell}[]{csh}{%
+  escapechar=@
+  identifierstyle=\lp@basic,
+  mathescape=false,
+  backgroundcolor=,
+  literate={\\\$}{\$}1
+}
+
+\newcommand{\listingname}[1]%
+{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
+
+\lstnewenvironment{shell}[1][]
+{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
+
+% Why
 % --------------------------------------------------------------------------
+
 \lstdefinelanguage{Why}{%
   morekeywords={
     type, logic, axiom, predicate, goal,
@@ -419,22 +685,22 @@ literate=%
   {not}{$\neg$}1%
   {<>}{$\neq$}1%
   {...}{$\dots$}1%
-  %{_}{\_}1%
-  %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
-  }
+}
 
 \lstdefinestyle{why-style}{%
-language=Why,%
-style=framac-code-style,%
-basicstyle=\lp@inline,%
+  language=Why,%
+  style=framac-code-style,%
+  basicstyle=\lp@inline,%
 }
 
-\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
 \newcommand{\whyinput}[1]%
 {\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
 \newcommand{\whyinline}[1]%
 {\lstinline[style=why-style]{#1}}
-\makeatother
-% --------------------------------------------------------------------------
-% ---  End.                                                              ---
+
+\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
+
+% Default style is empty
 % --------------------------------------------------------------------------
+
+\lstset{style=frama-c-style}
diff --git a/doc/logos/by-nc-nd.eu.png b/doc/logos/by-nc-nd.eu.png
new file mode 100644
index 0000000000000000000000000000000000000000..1653db7476561b663b0a7804a6d57df932e63fb6
Binary files /dev/null and b/doc/logos/by-nc-nd.eu.png differ
diff --git a/doc/logos/by-nc-nd.png b/doc/logos/by-nc-nd.png
new file mode 100644
index 0000000000000000000000000000000000000000..5a8dbd0652e37cc2d89b4899e307abcac8bda553
Binary files /dev/null and b/doc/logos/by-nc-nd.png differ
diff --git a/doc/logos/by-nc-sa.eu.png b/doc/logos/by-nc-sa.eu.png
new file mode 100644
index 0000000000000000000000000000000000000000..433bc81751d21ffbfc2c13456a23ff60dc341eff
Binary files /dev/null and b/doc/logos/by-nc-sa.eu.png differ
diff --git a/doc/logos/by-nc-sa.png b/doc/logos/by-nc-sa.png
new file mode 100644
index 0000000000000000000000000000000000000000..b9a55533c0cb035de1769b2a5ac63ce9b194fc69
Binary files /dev/null and b/doc/logos/by-nc-sa.png differ
diff --git a/doc/logos/by-nc.eu.png b/doc/logos/by-nc.eu.png
new file mode 100644
index 0000000000000000000000000000000000000000..efdb6af68507a180a0fef0398415ff2b92516012
Binary files /dev/null and b/doc/logos/by-nc.eu.png differ
diff --git a/doc/logos/by-nc.png b/doc/logos/by-nc.png
new file mode 100644
index 0000000000000000000000000000000000000000..25e284099a07df1ba95e4140fbfe7a8d1740fdc5
Binary files /dev/null and b/doc/logos/by-nc.png differ
diff --git a/doc/logos/by-nd.png b/doc/logos/by-nd.png
new file mode 100644
index 0000000000000000000000000000000000000000..fc3d26789a0b4f529a132bcae501dca6ce208f45
Binary files /dev/null and b/doc/logos/by-nd.png differ
diff --git a/doc/logos/by-sa.png b/doc/logos/by-sa.png
new file mode 100644
index 0000000000000000000000000000000000000000..8770732928cb20d8aeafee32bec9c5de89d51238
Binary files /dev/null and b/doc/logos/by-sa.png differ
diff --git a/doc/logos/by.png b/doc/logos/by.png
new file mode 100644
index 0000000000000000000000000000000000000000..c8473a24786ab016d9c3e717a380910f7cbb0fff
Binary files /dev/null and b/doc/logos/by.png differ
diff --git a/doc/logos/cc-zero.png b/doc/logos/cc-zero.png
new file mode 100644
index 0000000000000000000000000000000000000000..4ff09a0bb26016cef37b018a23d191be5a1cd0c9
Binary files /dev/null and b/doc/logos/cc-zero.png differ
diff --git a/doc/logos/cea_tech_list.jpg b/doc/logos/cea_tech_list.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..2242a2fa3af021450d34b9a536b55ec28fb61542
Binary files /dev/null and b/doc/logos/cea_tech_list.jpg differ
diff --git a/doc/logos/frama-c.png b/doc/logos/frama-c.png
new file mode 100644
index 0000000000000000000000000000000000000000..b9ca5b60d7d2a1476350b68779794e28a2731f0c
Binary files /dev/null and b/doc/logos/frama-c.png differ
diff --git a/doc/logos/publicdomain.png b/doc/logos/publicdomain.png
new file mode 100644
index 0000000000000000000000000000000000000000..df2c82f3dd0f862e820855a81f7e6123808b0340
Binary files /dev/null and b/doc/logos/publicdomain.png differ
diff --git a/doc/metrics/.gitignore b/doc/metrics/.gitignore
index 58acfccd3f95d479e49545c1041c63d0f4fbcef6..a51348c397434abe7af3b018702dc72de0260b11 100644
--- a/doc/metrics/.gitignore
+++ b/doc/metrics/.gitignore
@@ -1,8 +1,6 @@
 /anr-logo.png
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
-/frama-c-affiliation.tex
 /metrics.pdf
+/logos
+/fc-macros.tex
diff --git a/doc/metrics/metrics.tex b/doc/metrics/metrics.tex
index 11b1f4ada005edcff0f2e4660c999e36440640df..06586c962d25027c83c450003860509184233fbf 100644
--- a/doc/metrics/metrics.tex
+++ b/doc/metrics/metrics.tex
@@ -3,27 +3,17 @@
 \usepackage{amsmath}
 \newcommand{\framacversion}%
            {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
-\input{./frama-c-affiliation.tex}
 
-\begin{document}
-\coverpage{Metrics}
-
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{img/cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{Frama-C's metrics plug-in}{\framacversion}
+\title{The Metrics plug-in}
 \author{Richard Bonichon \& Boris Yakobowski}
-\begin{tabular}{l}
-  \fcaffiliationen
-\end{tabular}
-\vfill
-\begin{flushleft}
-  \textcopyright 2011--\the\year{} CEA LIST
-\end{flushleft}
-\end{titlepage}
 
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+\copyrightstarts{2011}
+
+\begin{document}
+\maketitle
 \tableofcontents
 
 \chapter{Quick overview}
diff --git a/doc/release/.gitignore b/doc/release/.gitignore
index 8590f2c47f97ebace19b519fd9329e39501fc4bc..83a46ab116d3bf74b6080246fd061f79d54ad03f 100644
--- a/doc/release/.gitignore
+++ b/doc/release/.gitignore
@@ -1,7 +1,6 @@
 /anr-logo.png
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
 /release.pdf
+/fc-macros.tex
+/logos
diff --git a/doc/release/deploy.tex b/doc/release/deploy.tex
index a6fc41606db765acbd3ba965ceab4f7db7335e3e..1de8304b27dacdfe3eebfff7b12998008f035a17 100644
--- a/doc/release/deploy.tex
+++ b/doc/release/deploy.tex
@@ -133,15 +133,15 @@ version in \url{https://git.frama-c.com/pub/frama-c/-/tags}.
 
 \section{Opam package}
 
-You'll need a GitHub account to create a pull request on the official opam repository,
-\texttt{ocaml/opam-repository.git}. Go to the Frama-C GitHub organization opam
-repository (\url{https://github.com/Frama-C/opam-repository}). Find the branch
-corresponding to the release and create the pull-request on the official opam
-repository.
+You'll need a GitHub account to create a pull request on the official opam
+repository\footnote{\texttt{ocaml/opam-repository.git}}. Go to the \FramaC
+GitHub organization opam repository (\url{https://github.com/Frama-C/opam-repository}).
+Find the branch corresponding to the release and create the pull-request on the
+official opam repository.
 
 \section{Other repositories to update}
 
-Check if other Frama-C (and related) repositories need to be updated:
+Check if other \FramaC (and related) repositories need to be updated:
 
 \begin{itemize}
 \item \texttt{acsl-language/acsl} (if last minute patches were applied)
diff --git a/doc/release/release.tex b/doc/release/release.tex
index 08d23cef1011d33c4b193dd4ff969ef19052efbe..343dcad56856c245bf738f113de791f3a1ef0c24 100644
--- a/doc/release/release.tex
+++ b/doc/release/release.tex
@@ -1,18 +1,21 @@
 \documentclass{frama-c-book}
+\input{fc-macros}
 
-\newcommand{\tool}[1]{\textsf{#1}\xspace}
 \newcommand{\expertise}[1]{{\color{gray}{[#1]}}}
 \newcommand{\todo}[1]{{\color{red}{[#1]}}}
 
 
 \makeatletter\@openrightfalse\makeatother
 
-\begin{document}
-\coverpage{Release Management}
-\begin{titlepage}
-\title{Release Management Manual}{CEA -- Private}
+\title{Release Management Manual}
 \author{Loïc Correnson, Patrick Baudin, François Bobot, Julien Signoles and Boris Yakobowski}
-\end{titlepage}
+
+\cclicence{by-sa}
+\copyrightstarts{2009}
+
+\begin{document}
+
+\maketitle
 \tableofcontents
 
 \input{intro}
diff --git a/doc/release/validation.tex b/doc/release/validation.tex
index a67ecd661261e239546f109e03d0b561dbd0b77e..fd9ccc5fe0b912b7d783f7ceb074d0a0487e6a18 100644
--- a/doc/release/validation.tex
+++ b/doc/release/validation.tex
@@ -173,9 +173,10 @@ precise configuration:
   \item \verb+docker build . -t framac/frama-c:dev --target frama-c-gui-slim \+\\
         \verb+  -f Dockerfile.dev --build-arg=from_archive=frama-c-<VERSION>.tar.gz+
 \end{itemize}
-For the GUI: you might want to install the
-\href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script, in
-order to be able to launch \verb+x11docker framac/frama-c:dev frama-c-gui+
+For the GUI: in order to be able to launch
+\verb+x11docker framac/frama-c:dev frama-c-gui+,
+you might want to install the
+\href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script.
 
 \section{Validate release}
 
diff --git a/doc/rte/.gitignore b/doc/rte/.gitignore
index 77ccbb7eaf92e390d1162ea9f3af03b698423f9a..89a70250372e530d5e08302ff1de19d4cca9e839 100644
--- a/doc/rte/.gitignore
+++ b/doc/rte/.gitignore
@@ -1,9 +1,7 @@
 /anr-logo.png
 /eu-flag.jpg
 /frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
 /framacversion.tex
-/frama-c-affiliation.tex
+/fc-macros.tex
+/logos
 /main.pdf
diff --git a/doc/rte/main.tex b/doc/rte/main.tex
index f1582267f5d792036d0e425fc8b69ac95780f7bf..b8b7efe2b7de11b92b8cb7390785bd6c86618857 100644
--- a/doc/rte/main.tex
+++ b/doc/rte/main.tex
@@ -1,10 +1,12 @@
 \documentclass[a4paper,11pt,twoside,openright,web]{frama-c-book}
 
+\usepackage{ifthen}
+%\input{fc-macros.tex}
+
 \newcommand{\framacversion}%
            {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
 %%\usepackage{microtype}
 \input{macros_modern}
-\input{./frama-c-affiliation.tex}
 %%modern \usepackage{pslatex}
 %%modern \usepackage{a4wide}
 
@@ -15,7 +17,7 @@
 
 %-----------------------------------------------
 % barre de révision (utilisée pour A FAIRE)
-%%modern \usepackage[outerbars]{changebar} 
+%%modern \usepackage[outerbars]{changebar}
 
 %\definecolor{bleu}{rgb}{0.15,0.3,0.7}
 %\definecolor{orange}{rgb}{1.00,0.50,0.00}
@@ -49,26 +51,19 @@
 %%modern \renewcommand{\labelitemi}{$\bullet$}
 \renewcommand{\labelitemii}{$\triangleright$}
 %==============================================================================
+
+\title{RTE\\\bigskip Runtime Error Annotation Generation}
+\author{Philippe Herrmann and Julien Signoles}
+
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+\copyrightstarts{2010}
+
 \begin{document}
 
-\coverpage{RTE --- Runtime Error Annotation Generation}
+\maketitle
 
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{Frama-C's RTE plug-in}{for Frama-C \framacversion}
-\author{Philippe Herrmann and Julien Signoles}
-\begin{tabular}{l}
-  \fcaffiliationen
-\end{tabular}
-\vfill
-\begin{flushleft}
-  \textcopyright 2010-{\the\year} CEA LIST
-
-\end{flushleft}
-\end{titlepage}
 \input{rte.tex}
 
 \end{document}
diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex
index bcb27b675a6a94c0e78e7086a2330f7834c6ade2..200338121c64c797a03ab97c02b81aff7cf536ed 100644
--- a/doc/rte/rte.tex
+++ b/doc/rte/rte.tex
@@ -923,4 +923,3 @@ annotations even when they trivially hold \\
 \addcontentsline{toc}{chapter}{\bibname}
 \bibliographystyle{plain}
 \bibliography{./biblio}
-
diff --git a/doc/userman/.gitignore b/doc/userman/.gitignore
index a2dae99658f6339db386901d057bf1f5368eccf6..68d73f9e795bab5c3388735d975f1ab8a70c44c6 100644
--- a/doc/userman/.gitignore
+++ b/doc/userman/.gitignore
@@ -1,10 +1,8 @@
 anr-logo.png
 eu-flag.jpg
 frama-c-book.cls
-frama-c-cover.pdf
-frama-c-left.pdf
-frama-c-right.pdf
-frama-c-affiliation.tex
+fc-macros.tex
+logos
 userman.idx
 userman.out
 userman.pdf
diff --git a/doc/userman/macros.tex b/doc/userman/macros.tex
index 89afeea7155d1c80625056be00277497f3a0a9fb..97b84a5b5dc1ad82022e6447f7429c999ca7903e 100644
--- a/doc/userman/macros.tex
+++ b/doc/userman/macros.tex
@@ -2,20 +2,12 @@
            {\input{../../VERSION}\unskip{} (\input{../../VERSION_CODENAME}\unskip)}
 \newcommand{\nextframacversion}{Frama-C+dev}
 
-\newcommand{\tool}[1]{\textsf{#1}\xspace}
-
-\newcommand{\C}{\tool{C}}
 \newcommand{\caml}{\tool{OCaml}}
-\newcommand{\acsl}{\tool{ACSL}\index{ACSL@\tool{ACSL}}}
-\newcommand{\gcc}{\tool{GCC}}
-\newcommand{\Value}{\tool{Eva}}
-\newcommand{\Eva}{\tool{Eva}}
-\newcommand{\From}{\tool{From}}
-\newcommand{\WP}{\tool{WP}}
-\newcommand{\Report}{\tool{Report}}
-\newcommand{\Slicing}{\tool{Slicing}}
-\newcommand{\GUI}{\tool{GUI}}
-\newcommand{\opam}{\tool{opam}}
+\newcommand{\Value}{\Eva}
+\newcommand{\From}{\from}
+\newcommand{\WP}{\Wp}
+\newcommand{\Report}{\report}
+\newcommand{\Slicing}{\slicing}
 
 \newenvironment{commands}%
 {\par\hspace{2cm}\begin{tabular}{l}}%
diff --git a/doc/userman/userman.tex b/doc/userman/userman.tex
index 61ee7253a303b16b1f2a01e9bf29729cbc66bd7c..aeb3cb8dcba7efd6f0147ba25517c5ecdf8b3274 100644
--- a/doc/userman/userman.tex
+++ b/doc/userman/userman.tex
@@ -1,39 +1,36 @@
 % rubber: depend ../../VERSION
-\documentclass[web]{frama-c-book}
+\documentclass{frama-c-book}
 
 \usepackage{graphicx}
 \usepackage{calc}
 \usepackage{array}
 \usepackage{longtable}
 \usepackage{hyperref}
+\usepackage{makeidx}
 
-\include{macros}
-\input{./frama-c-affiliation.tex}
+\input{fc-macros}
+\input{macros}
 
 \makeindex
 
-\begin{document}
-
-\coverpage{User Manual}
-
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{Frama-C User Manual}{Release \framacversion}
+\title{Frama-C User Manual}
 \author{Loïc Correnson, Pascal Cuoq, Florent Kirchner, André
   Maroneze, Virgile Prevosto, Armand Puccetti, Julien Signoles and Boris
   Yakobowski}
-\begin{tabular}{l}
-  \fcaffiliationen
-\end{tabular}
-\vfill
-\begin{flushleft}
-  \textcopyright 2009-2022 CEA LIST
-\end{flushleft}
-\end{titlepage}
 
+\acknowledge{Patrick Baudin}
+\acknowledge{Mickaël Delahaye}
+\acknowledge{Philippe Hermann}
+\acknowledge{Benjamin Monate}
+\acknowledge{Dillon Pariente}
+
+\fcversion{\framacversion}
+\cclicence{by-sa}
+\copyrightstarts{2009}
+
+\begin{document}
+
+\maketitle
 \tableofcontents
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -48,12 +45,26 @@ content of this document corresponds to the version \framacversion, on \today, o
 
 \section*{Acknowledgements}
 
-We gratefully thank all the people who contributed to this document: Patrick
-Baudin, Mickaël Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente.
+\insertpeople
+
+\medskip
+
+\acknowledgeANR{
+  the French ANR projects CAT~(ANR-05-RNTL-00301) and U3CAT~(08-SEGI-021-01)
+}
 
-\acknowledgeANR
+\medskip
 
-\acknowledgeEU
+\acknowledgeEU{
+  the European Union's Seventh Framework Programme (FP7/2007-2013)
+  under grant agreement N$^\circ$\,317753 (\mbox{STANCE}).\\
+  It has also received funding from the Horizon 2020 research
+  and innovation programme, under grant agreements
+  N$^\circ$\,731453~(\mbox{VESSEDIA}),
+  N$^\circ$\,824231~(\mbox{DECODER}),
+  N$^\circ$\,830892~(\mbox{SPARTA}),
+  and N$^\circ$\,883242~(\mbox{ENSURESEC})
+}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/src/plugins/e-acsl/doc/Makefile.common b/src/plugins/e-acsl/doc/Makefile.common
index 401488851dffe90acdef46c2121e429d115d41c2..a8008ee15af8b8ead4f5676d16b741de770bcc1c 100644
--- a/src/plugins/e-acsl/doc/Makefile.common
+++ b/src/plugins/e-acsl/doc/Makefile.common
@@ -16,7 +16,7 @@ eacslversion.tex: Makefile $(VERSION_FILE) $(CODENAME_FILE)
 	rm -f $@
 	printf '\\newcommand{\\eacslpluginversion}{$(EACSL_VERSION)\\xspace}\n' > $@
 	printf '\\newcommand{\\eacslplugincodename}{$(EACSL_CODENAME)\\xspace}\n' >> $@
-	printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
+	printf '\\fcversion{$(FC_VERSION)\\xspace}\n' >> $@
 	chmod a-w $@
 
 %.1: %.mp
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index 3436ea4bc793f4beec375ee0b723b7edd82527eb..f9c6a2942e27bf9746e5645ed53a2f5388757865 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -1,10 +1,10 @@
 anr-logo.png
 eu-flag.jpg
 frama-c-book.cls
-frama-c-cover.pdf
-frama-c-left.pdf
-frama-c-right.pdf
-frama-c-affiliation.tex
 e-acsl.pdf
 e-acsl-implementation.pdf
 eacslversion.tex
+fc-macros.tex
+logos
+*.fls
+*.fdb_latexmk
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index b11d30f118e5d43228b31a5093c2c35987946a9e..3681c6f83dc772f0f7dbc16741dd89964f65b99e 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -1,10 +1,9 @@
 %; whizzy section -pdf -initex "pdflatex -ini"
-\documentclass[web]{frama-c-book}
+\documentclass{frama-c-book}
 %\usepackage{hevea}
 \usepackage{ifthen}
 
 \input{./macros_modern}
-\input{./frama-c-affiliation.tex}
 \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.
@@ -32,36 +31,42 @@
 \renewcommand{\topfraction}{0.99}
 \renewcommand{\bottomfraction}{0.99}
 
-\begin{document}
-\sloppy
-\hbadness=10000
+\title{
+  \huge % We are forced to reduce the size so that the second line fits into the page
+  E-ACSL \\
+  \medskip
+  Executable ANSI/ISO C Specification Language
+}
 
 \ifthenelse{\boolean{PrintImplementationRq}}%
-  {\coverpage{\vbox{\mbox{E-ACSL Version \eacsllangversion}\\[5mm]
-\mbox{\huge{Implementation in Frama-C plug-in E-ACSL}}\\[2mm]
-\mbox{\huge{version \eacslpluginversion{}}}}}}%
-  {\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 \eacslpluginversion}{}}
+{\subtitle{Version \eacsllangversion \space --
+ Implementation in \framac \eacsl version \eacslpluginversion}}
+{\subtitle{Version \eacsllangversion}}
 
 \author{Julien Signoles}
 
-\fcaffiliationen
-\vfill
-\begin{flushleft}
-  \textcopyright 2011-2022 CEA LIST
+\acknowledge{Patrick Baudin}
+\acknowledge{Bernard Botella}
+\acknowledge{Thibaut Benjamin}
+\acknowledge{Lo\"ic Correnson}
+\acknowledge{Pascal Cuoq}
+\acknowledge{Basile Desloges}
+\acknowledge{Johannes Kanig}
+\acknowledge{Andr\'e Maroneze}
+\acknowledge{Fonenantsoa Maurica}
+\acknowledge{David Mentr\'e}
+\acknowledge{Benjamin Monate}
+\acknowledge{Yannick Moy}
+\acknowledge{Virgile Prevosto}
+
+\cclicence{by-sa}
+\copyrightstarts{2011}
+
+\begin{document}
+\sloppy
+\hbadness=10000
 
-  This work has been initially supported by the `Hi-Lite' FUI project (FUI AAP
-  9).
-\end{flushleft}
-\end{titlepage}
+\maketitle
 
 %%Contents should open on right
 \cleardoublepage
@@ -80,20 +85,13 @@ These features are marked with \experimental.
 
 \section*{Acknowledgements}
 
-We gratefully thank all the people who contributed to this document:
-Patrick Baudin,
-Bernard Botella,
-Thibaut Benjamin,
-Lo\"ic Correnson,
-Pascal Cuoq,
-Basile Desloges,
-Johannes Kanig,
-Andr\'e Maroneze,
-Fonenantsoa Maurica,
-David Mentr\'e,
-Benjamin Monate,
-Yannick Moy and
-Virgile Prevosto.
+\insertpeople
+
+\medskip
+
+This work has been initially supported by the ‘Hi-Lite’ FUI project (FUI AAP 9).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \include{intro_modern}
 
diff --git a/src/plugins/e-acsl/doc/refman/transf.mll b/src/plugins/e-acsl/doc/refman/transf.mll
index c56692b20e37edb33519844e84a1a84d6c96675a..ff2096653ce9e6484fabcec17642c624f01686a4 100644
--- a/src/plugins/e-acsl/doc/refman/transf.mll
+++ b/src/plugins/e-acsl/doc/refman/transf.mll
@@ -42,6 +42,7 @@ rule main = parse
   | "\\@" {
       print_string "@";
       main lexbuf }
+  | "\n" { print_char '\n'; main lexbuf }
   | _ {
       print_char (lexeme_char lexbuf 0); main lexbuf }
   | eof {
@@ -102,6 +103,7 @@ and syntax = parse
   | "}" { print_string "\\end{notimplementedenv}"; syntax lexbuf }
   | "[" { print_string "\\begin{markdiffenv}"; syntax lexbuf }
   | "]" { print_string "\\end{markdiffenv}"; syntax lexbuf }
+  | "\n" { print_char '\n'; syntax lexbuf }
   | _ {
       print_char (lexeme_char lexbuf 0);
       syntax lexbuf }
diff --git a/src/plugins/e-acsl/doc/userman/.gitignore b/src/plugins/e-acsl/doc/userman/.gitignore
index 539ba638159cd08695034fbb376305cf552ba474..b89e361862c7254e7d5f40030e099f01e2438198 100644
--- a/src/plugins/e-acsl/doc/userman/.gitignore
+++ b/src/plugins/e-acsl/doc/userman/.gitignore
@@ -6,3 +6,7 @@ frama-c-left.pdf
 frama-c-right.pdf
 frama-c-affiliation.tex
 main.pdf
+fc-macros.tex
+logos
+*.fls
+*.fdb_latexmk
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index f44e40b6666b66e4477cf552e4644151e9f7bdee..b504f1029ab868f884460df433e02b28ccb8ca14 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -1,38 +1,33 @@
-\documentclass[web]{frama-c-book}
+\documentclass{frama-c-book}
 
 \usepackage{graphicx}
 \usepackage{calc}
+\usepackage{ifthen}
+\usepackage{imakeidx}
 
-\include{macros}
-\include{eacslversion}
-\input{./frama-c-affiliation.tex}
+\input{macros}
+\input{eacslversion}
 
 \makeindex
 
-\begin{document}
+\title{E-ACSL Plug-in}
+\author{Julien Signoles, Basile Desloges and Kostyantyn Vorobyov}
 
-\coverpage{\eacsl User Manual}
+\acknowledge{Pierre-Lo\"ic Garoche}
+\acknowledge{Jens Gerlach}
+\acknowledge{Florent Kirchner}
+\acknowledge{Nikola\"i Kosmato}
+\acknowledge{Andr\'e Maroneze}
+\acknowledge{Fonenantsoa Maurica}
+\acknowledge{Guillaume Petio}
+
+\cclicence{by-sa}
+\copyrightstarts{2013}
+
+\begin{document}
 
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{\eacsl Plug-in}{Release \eacslpluginversion (\eacslplugincodename)
- \ifthenelse{\equal{\eacslpluginversion}{\fcversion}}{}{%
-   \\[1em] compatible with \framac \fcversion}}
-\author{Julien Signoles, Basile Desloges and Kostyantyn Vorobyov}
-\begin{center}
-\fcaffiliationen
-\end{center}
-\vfill
-\begin{flushleft}
-  \textcopyright 2013-2022 CEA LIST
-%%
-  %% This work has been supported by the `Hi-Lite' FUI project (FUI AAP 9).
-\end{flushleft}
-\end{titlepage}
 
+\maketitle
 \tableofcontents
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -50,9 +45,7 @@ evolve in the future.
 
 \section*{Acknowledgements}
 
-We gratefully thank the people who contributed to this document:
-Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola\"i Kosmatov,
-Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot.
+\insertpeople
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/src/plugins/wp/doc/MakeDoc b/src/plugins/wp/doc/MakeDoc
index b31bc125bb71eba3f874f3e7202b56e62c2f0f9e..54cb6b118b3990b1819993724442be79e8e93235 100644
--- a/src/plugins/wp/doc/MakeDoc
+++ b/src/plugins/wp/doc/MakeDoc
@@ -25,7 +25,7 @@
 # --------------------------------------------------------------------------
 FRAMAC_DOC= .make-class .make-images .make-icons VERSION VERSION_CODENAME
 # --------------------------------------------------------------------------
-FRAMAC_CLASS=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf frama-c-affiliation.tex
+FRAMAC_CLASS=frama-c-book.cls fc-macros.tex logos anr-logo.png
 FRAMAC_BULLETS=never_tried.png unknown.png valid_under_hyp.png surely_valid.png
 FRAMAC_IMAGES=cealistlogo.jpg
 # --------------------------------------------------------------------------
@@ -35,7 +35,7 @@ FRAMAC_TRUNK?=../../../../..
 RES_CLASS=$(addprefix $(FRAMAC_TRUNK)/doc/,$(FRAMAC_CLASS))
 .make-class: $(RES_CLASS)
 	@echo "Import Frama-C Class"
-	@cp -fv $(RES_CLASS) .
+	@cp -rfv $(RES_CLASS) .
 	@touch .make-class
 
 RES_IMAGES=$(addprefix $(FRAMAC_TRUNK)/doc/images/,$(FRAMAC_IMAGES))
diff --git a/src/plugins/wp/doc/manual/.gitignore b/src/plugins/wp/doc/manual/.gitignore
index 2006f84eb8f8a22fe252c27be26e6d27f227b729..ae43a86a634148a0a0314d6b19a1bf951803dae7 100644
--- a/src/plugins/wp/doc/manual/.gitignore
+++ b/src/plugins/wp/doc/manual/.gitignore
@@ -5,3 +5,7 @@
 /*.log-file
 /wp.fls
 /wp.fdb_latexmk
+/logos
+/macros.tex
+/anr-logo.png
+/fc-macros.tex
diff --git a/src/plugins/wp/doc/manual/wp.tex b/src/plugins/wp/doc/manual/wp.tex
index f843fe3c40bbf4075410b24b52e4029d39f6a183..1738ab83a3390840b217cca2e8cbfa842579bfe0 100644
--- a/src/plugins/wp/doc/manual/wp.tex
+++ b/src/plugins/wp/doc/manual/wp.tex
@@ -1,44 +1,50 @@
-%rubber: watch main.tdo main.cb wp.bbl wp.bib 
+%rubber: watch main.tdo main.cb wp.bbl wp.bib
 %rubber: depend swap1.log-file swap2.log-file swap3.log-file
 %rubber: depend ../../tests/wp_manual/working_dir/swap.c
 %rubber: depend ../../tests/wp_manual/working_dir/swap1.h
 %rubber: depend ../../tests/wp_manual/working_dir/swap2.h
-%rubber: depend wp-complete.png wp-gui-main.png wp-gui-run.png 
+%rubber: depend wp-complete.png wp-gui-main.png wp-gui-run.png
 %rubber: depend wp-invalid.png  wp-unknown.png  wp-valid.png
 
-\documentclass[web]{frama-c-book}
+\documentclass{frama-c-book}
 \usepackage{amsmath}
 \usepackage{longtable}
 \usepackage{pifont}
 
-\input{./frama-c-affiliation.tex}
+\input{fc-macros}
 
-%\anticopyCEA{} % To comments for public version.
-\begin{document}
 \newcommand{\FCVERSION}{\input{VERSION}(\input{VERSION_CODENAME}\unskip)}
-\coverpage{Frama-C / WP {\hspace{1cm}\normalsize\tt \FCVERSION}}
-\begin{titlepage}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\hfill~
-\vfill
-\title{WP Plug-in Manual}%
-{\tt Frama-C \FCVERSION}
+
+\title{WP Plug-in Manual}
 \author{Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, Allan Blanchard}
-\begin{center}
-  \fcaffiliationen
-\end{center}
-\vfill
-\begin{flushleft}
-  \textcopyright 2010-{\the\year} CEA LIST
+\fcversion{\FCVERSION}
 
-  This work has been partially supported by the 'U3CAT' ANR project.
-\end{flushleft}
-\end{titlepage}
+\cclicence{by}
+\copyrightstarts{2010}
 
+%\anticopyCEA{} % To comments for public version.
+\begin{document}
+\maketitle
 \cleardoublepage
 \markright{}
 \tableofcontents
 
+\chapter*{Foreword}
+\markright{}
+\addcontentsline{toc}{chapter}{Foreword}
+
+This is the user manual of the WP plug-in of \FramaC\footnote{\url{http://frama-c.com}}.
+The content of this document corresponds to the version \FCVERSION, on \today, of
+\FramaC.
+
+\section*{Acknowledgements}
+
+\medskip
+
+\acknowledgeANR{
+  the French ANR project U3CAT~(08-SEGI-021-01)
+}
+
 \input{wp_intro.tex}
 \input{wp_plugin.tex}
 \input{wp_models.tex}
@@ -49,4 +55,3 @@
 \bibliography{wp}
 
 \end{document}
-
diff --git a/src/plugins/wp/doc/manual/wp_builtins.tex b/src/plugins/wp/doc/manual/wp_builtins.tex
index 4454601c8d3cd38a8eb861d195ac1ba37a7ac09b..5c04a947a4d802c007d8814f5814ba2cb43a10ad 100644
--- a/src/plugins/wp/doc/manual/wp_builtins.tex
+++ b/src/plugins/wp/doc/manual/wp_builtins.tex
@@ -51,8 +51,8 @@ from which all the properties are automatically imported and communicated to the
     \hline
     \end{tabular}
 \end{center}
-\label{wp-builtins-list}
 \caption{Supported \textsf{ACSL} builtins}
+\label{wp-builtins-list}
 \end{figure}
 
 Below in the section, additional informations are given for each supported builtin, with a brief