diff --git a/doc/developer/introduction.tex b/doc/developer/introduction.tex
index b19747d9410c7c05624f397b2074fe6c8302c8a6..05c4ca9f5bf730e07df9bc776c382088323702ed 100644
--- a/doc/developer/introduction.tex
+++ b/doc/developer/introduction.tex
@@ -14,7 +14,7 @@ transformation through a new plug-in. For this purpose, it provides a
 step-by-step tutorial, a general presentation of the \framac software
 architecture and an overview of the
 API of the \framac kernel. However it does not provide a complete documentation
-of the \framac API and, in particular, it does not describe the API of 
+of the \framac API and, in particular, it does not describe the API of
 existing \framac plug-ins.
 %This API is documented in the \html source code
 %generated by \texttt{make doc} (see
@@ -27,11 +27,11 @@ nor the use of plug-ins which are documented in separated and dedicated
 manuals~\cite{slicing,wp,value,rte,aorai}.  We assume that the reader of this
 guide already read the \framac user manual and knows the main \framac concepts.
 
-The reader of this guide may be either a \framac beginner who just finished 
+The reader of this guide may be either a \framac beginner who just finished
 reading the user manual and wishes to develop their own analysis with the help
-of \framac, an intermediate-level plug-in developer who would like to have 
-a better understanding of one particular aspect of the framework, 
-or a \framac expert who wants to remember details about one specific point 
+of \framac, an intermediate-level plug-in developer who would like to have
+a better understanding of one particular aspect of the framework,
+or a \framac expert who wants to remember details about one specific point
 of the \framac development.
 
 \framac is fully developed within the \ocaml programming
@@ -49,10 +49,10 @@ the category of readers they are intended for and a set of prerequisites.
 Appendix \ref{chap:changes} references all the changes made to
 this document between successive \framac releases.
 
-In the index, page numbers written in bold italics (e.g.  
+In the index, page numbers written in bold italics (e.g.
 \textcolor{red}{\textit{\textbf{1}}}) reference the defining sections for the
 corresponding entries while other numbers (e.g. \textcolor{red}{1}) are
-less important references. 
+less important references.
 Furthermore, the name of each \caml value
 in the index corresponds to an actual \framac value.
 
@@ -76,9 +76,9 @@ This guide is organised in three parts.
 \item[Chapter~\ref{chap:tutorial}] is a step-by-step tutorial for developing a
   new plug-in within the \framac platform. At the end of this tutorial, a
   developer should be able to extend \framac with a simple analysis available
-  as a \framac plug-in. 
+  as a \framac plug-in.
 \item[Chapter~\ref{chap:archi}] presents the \framac software
-  architecture. 
+  architecture.
 \item[Chapter~\ref{chap:advance}] details how to use all the services provided
-  by \framac in order to develop a fully integrated plug-in. 
+  by \framac in order to develop a fully integrated plug-in.
 \end{description}
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 6dafa681fcd42e4ca6f3091ef20bf617af091759..4403388e929e6f3fa1e68f2eb5ca3654e4204c03 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -1,4 +1,4 @@
-\chapter{\acsl extensions}
+\chapter{ACSL extensions} % here we do not use the macro (avoids a warning)
 \label{cha:acsl-extensions}
 \section{Handling indirect calls with \texttt{calls}}
 \label{acsl:calls}
diff --git a/doc/userman/user-intro.tex b/doc/userman/user-intro.tex
index 9f60b97c9197c4208b4f690e71ef654599a68526..b89a4fd4268988d87e5ade5340b4045c28b17fb7 100644
--- a/doc/userman/user-intro.tex
+++ b/doc/userman/user-intro.tex
@@ -1,15 +1,15 @@
 \chapter{Introduction}
 \label{user-intro}
 
-This is \FramaC's user manual. 
+This is \FramaC's user manual.
 \FramaC is an open-source platform dedicated to
 the analysis of source code written in the \tool{C} programming
 language. The \FramaC platform gathers several analysis techniques into
-a single collaborative framework. 
+a single collaborative framework.
 
-This manual gives an overview of \FramaC for newcomers, 
+This manual gives an overview of \FramaC for newcomers,
 and serves as a reference for expert users.
-It only describes those platform features that are common to all analyzers. 
+It only describes those platform features that are common to all analyzers.
 Thus it \emph{does not cover} the use of the analyzers provided in the \FramaC
 distribution (Eva, WP, E-ACSL, \ldots). Each of these analyses has its
 own specific documentation~\cite{wp,value,eacsl}. Furthermore, research
@@ -23,19 +23,19 @@ Guide~\cite{plugin-dev-guide}.
 Appendix \ref{chap:changes} references all the changes made to this document
 between successive \FramaC releases.
 
-In the index, page numbers written in bold italics (e.g.  
+In the index, page numbers written in bold italics (e.g.
 \textcolor{red}{\textit{\textbf{1}}}) reference the defining sections for the
 corresponding entries while other numbers (e.g. \textcolor{red}{1}) are
-less important references. 
+less important references.
 
 \begin{important}
-The most important paragraphs are displayed inside gray boxes like this one.
+The most important paragraphs are displayed inside orange boxes like this one.
 A plug-in developer \textbf{must} follow them very carefully.
 \end{important}
 
 \section{Outline}
 
-The remainder of this manual is organized in several chapters. 
+The remainder of this manual is organized in several chapters.
 
 \begin{description}
 \item[Chapter~\ref{user-overview}] provides a general overview of the platform.
diff --git a/doc/userman/user-services.tex b/doc/userman/user-services.tex
index 838b5974d334a8ad6200e619d374bbea35f2273c..eba49f2f30f94d895a9fbf0fc6f063cec34260ce 100644
--- a/doc/userman/user-services.tex
+++ b/doc/userman/user-services.tex
@@ -66,9 +66,9 @@ When loading, the following actions are done in sequence:
 \end{enumerate}
 
 Consider for instance the following command.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -load foo.sav -eva
-\end{shell}
+\end{frama-c-commands}
 It loads all projects saved in the file \texttt{foo.sav}. Then, it runs the
 value analysis in the new current project if and only if it was not already
 computed at save time.
@@ -103,10 +103,10 @@ analysis when one of the analysis parameters changes.
 Consider the two following
 commands.\optionidx{-}{save}\optionidx{-}{load}\optionidx{-}{absolute-valid-range}%
 \optionidx{-}{ulevel}
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -save foo.sav -ulevel 5 -absolute-valid-range 0-0x1000 -eva foo.c
 \$ frama-c -load foo.sav
-\end{shell}
+\end{frama-c-commands}
 \FramaC runs the value analysis plug-in on the file \texttt{foo.c} where loops
 are unrolled $5$ times (option \texttt{-ulevel}, see
 Section~\ref{sec:normalize}). To compute its result, the value analysis
@@ -121,10 +121,10 @@ analysis since the parameters have not been changed.
 Consider now the two following commands.
 \optionidx{-}{save}\optionidx{-}{load}\optionidx{-}{absolute-valid-range}%
 \optionidx{-}{ulevel}
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -save foo.sav -ulevel 5 -absolute-valid-range 0-0x1000 -eva foo.c
 \$ frama-c -load foo.sav -absolute-valid-range 0-0x2000
-\end{shell}
+\end{frama-c-commands}
 The first command produces the very same result than above. However, in the
 second (load) command, \FramaC knows that one parameter has changed. Thus it
 discards the saved results of the value analysis and recomputes it on the same
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 09b331badf4c5ffc70bad9d102f24fc0263169cd..b748156775df3412b336012ef6b37269a5608bef 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -76,13 +76,13 @@ the following placeholders:
 \end{tabular}
 
 Here are some examples for using this option.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -cpp-command 'gcc -C -E -I. -x c' file1.src file2.i
 \$ frama-c -cpp-command 'gcc -C -E -I. %args -o %o %i' file1.c file2.i
 \$ frama-c -cpp-command 'cp %i %o'  file1.c file2.i
 \$ frama-c -cpp-command 'cat %i > %o' file1.c file2.i
 \$ frama-c -cpp-command 'CL.exe /C /E %args %i > %o' file1.c file2.i
-\end{shell}
+\end{frama-c-commands}
 
 When using \optionuse{-}{cpp-command}, you may add \optiondef{-}{cpp-frama-c-compliant}
 to indicate that the custom preprocessor accepts the same set of options as GNU
@@ -233,9 +233,9 @@ should be used for a given enumerated type. Namely, the C standard allows the us
 of any integral type in which all the corresponding tags can be represented.
 Default is \texttt{gcc-enums}. A list of supported
 options can be obtained by typing:
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -enums help
-\end{shell}
+\end{frama-c-commands}
 This includes:
 \begin{itemize}
 \item \texttt{int}: treat everything as \texttt{int} (including enumerated types
@@ -292,9 +292,9 @@ a negative value, and choose the smallest rank possible starting from
   automatically, but otherwise option \optionuse{-}{cpp-command} can be used.
 
 The list of supported platforms can be obtained by typing:
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -machdep help
-\end{shell}
+\end{frama-c-commands}
 
 The process for adding a new platform is described in the Plug-in
 Development Guide~\cite{plugin-dev-guide}.
@@ -345,9 +345,9 @@ used by plug-ins which support it. Note however that since \verb|-load| implies
 files given on the command line are ignored, \verb|-load| and \verb|-ast-diff| with
 the list of C files to consider must be properly sequenced through the use of
 \verb|-then| or one of its variants (Section~\ref{sec:then}), as in:
-\begin{lstlisting}[language=shell]
-frama-c -load previous.sav -then -ast-diff file1.c file2.c [...]
-\end{lstlisting}
+\begin{frama-c-commands}
+\$ frama-c -load previous.sav -then -ast-diff file1.c file2.c [...]
+\end{frama-c-commands}
 
 {\em Note: currently, parsing and type-checking are systematically performed
   even with this option, and \verb|-ast-diff| compares the normalized ASTs.
@@ -518,16 +518,16 @@ emitted by \FramaC during the normalization phase.
 If the steps up to normalization succeed, the project is then ready for
 analysis by any \FramaC plug-in. It is possible to test that the source code
 preparation itself succeeds, by running \FramaC without any option.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c <input files>
-\end{shell}
+\end{frama-c-commands}
 
 If you need to use other options for preprocessing or normalizing the source
 code, you can use the option \optiondef{-}{typecheck} for
 the same purpose. For instance:
-\begin{shell}
-frama-c -cpp-command 'gcc -C -E -I. -x c' -typecheck file1.src file2.i
-\end{shell}
+\begin{frama-c-commands}
+\$ frama-c -cpp-command 'gcc -C -E -I. -x c' -typecheck file1.src file2.i
+\end{frama-c-commands}
 
 
 % Local variables:
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index af7ddd445d68f192633b3b8b63b6dd81592d51ed..24122924c5e0240d95fc0962d448b81b17b3ace8 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -268,10 +268,11 @@ of it, several possibilities exist.
 content of the file to \texttt{\~{}/.bash\_completion}
 \item You can \texttt{source} the file, e.g. from your \texttt{.bashrc} with
 the following command:
+\end{itemize}
 \begin{verbatim}
 source $(frama-c-config -print-share-path)/autocomplete_frama-c || true
 \end{verbatim}
-\end{itemize}
+
 
 There is also an autocompletion script for zsh, \texttt{\_frama-c}, also
 in the shared resources directory. Look inside for installation instructions.
@@ -292,9 +293,9 @@ next occurrence of \texttt{-then}) and runs its actions according to the read
 options. Note that this second run starts with the results of the first one.
 
 Consider for instance the following command.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -eva -ulevel 4 file.c -then -ulevel 5
-\end{shell}
+\end{frama-c-commands}
 It first runs the value analysis plug-in (option
 \optionuse{-}{eva},~\cite{value}) with an unrolling level of 4 (option
 \optionuse{-}{ulevel}, Section~\ref{sec:normalize}). Then it re-runs the value
@@ -304,34 +305,34 @@ level of 5.
 It is also possible to specify a project (see Section~\ref{sec:project}) on
 which the actions are applied thanks to the option \optiondef{-}{then-on}.
 Consider for instance the following command.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -semantic-const-fold main file.c -then-on propagated -eva
-\end{shell}
+\end{frama-c-commands}
 It first propagates constants in function \texttt{main} of \texttt{file.c}
 (option \optionuse{-}{semantic-const-fold}) which generates a new project
 called \texttt{propagated}. Then it runs the value analysis plug-in on this new
 project. Finally it restores the initial default project, except if the option
-\optiondef{-}{set-project-as-default} is used as follow:
-\begin{shell}
+\optiondef{-}{set-project-as-default} is used as follows:
+\begin{frama-c-commands}
 \$ frama-c -semantic-const-fold main file.c \
           -then-on propagated -eva -set-project-as-default
-\end{shell}
+\end{frama-c-commands}
 
 Another possibility is the option \optiondef{-}{then-last} which applies the
 next actions on the last project created by a program transformer. For
 instance, the following command is equivalent to the previous one.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -semantic-const-fold main file.c -then-last -eva
-\end{shell}
+\end{frama-c-commands}
 
 The last option is \optiondef{-}{then-replace} which behaves like
 \optionuse{-}{then-last} but also definitively destroys the previous current
 project. It might be useful to prevent a prohibitive memory consumption. For
 instance, the following command is equivalent to the previous one, but also
 destroys the initial default project.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -semantic-const-fold main file.c -then-replace -eva
-\end{shell}
+\end{frama-c-commands}
 
 \subsection{Verbosity and Debugging Levels}
 
diff --git a/doc/userman/user-variadic.tex b/doc/userman/user-variadic.tex
index 45d55547225e43ab87604c5304f000bc24a9b663..bc3cfd40688f4473ff74e39cf9c275c2233a12ab 100644
--- a/doc/userman/user-variadic.tex
+++ b/doc/userman/user-variadic.tex
@@ -144,9 +144,9 @@ possibly earlier) also enables some extra diagnostics:
   printf("%p", "string");
 \end{ccode}
 
-\begin{shell}
+\begin{logs}
   warning: format specifies type 'void *' but the argument has type 'char *'.
-\end{shell}
+\end{logs}
 
 Note that no single tool is currently able to emit all diagnostics emitted
 by the other two.
diff --git a/doc/userman/userman.bib b/doc/userman/userman.bib
index 23e1f375ea1dc7f92c9b2ca538280afd795b9e1b..1cf15671d1896043f436ca78316dc342067c24f0 100644
--- a/doc/userman/userman.bib
+++ b/doc/userman/userman.bib
@@ -95,7 +95,7 @@ note={Extended version of \cite{sefm12}},
 
 @inproceedings{sac13,
   author = {M. Delahaye and N. Kosmatov and J. Signoles},
-  title  = {Common Specification Language for Static and Dynamic Analysis of 
+  title  = {Common Specification Language for Static and Dynamic Analysis of
            {C} Programs},
   booktitle = {the 28th Annual ACM Symposium on Applied Computing ({SAC})},
   publisher = {ACM},
@@ -151,7 +151,7 @@ note={Extended version of \cite{sefm12}},
   author = {David Cok},
   title  = {{Frama-C}'s {Frama-Clang} plug-in},
   year   = 2021,
-  note   = {\mbox{\url{https://www.frama-c.com/download/frama-clang-manual.pdf}}},
+  note   = {\url{https://www.frama-c.com/download/frama-clang-manual.pdf}},
 }
 
 @inproceedings{metacsl,