diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index f82ebe0f4adad15247f958708010b2df0a12490e..bdfec9acc732ea0b1516a19ee06f899857d7360f 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -72,7 +72,7 @@ at \url{https://dune.readthedocs.io/en/stable/concepts.html\#library-deps}}.
 As is often the case, examples are very instructive; here is an example of
 mandatory dependencies from the \textsf{Dive} plug-in's \verb|dune| file:
 
-\begin{lstlisting}
+\begin{lstlisting}[language=Dune]
 (library
   [...]
   (libraries frama-c.kernel frama-c-studia.core frama-c-server.core)
@@ -113,12 +113,12 @@ Optional dependencies can be detected and disabled in different ways:
 Here is an example of \verb|select| from the \textsf{Aoraï} plug-in,
 which defines an optional dependency on the \textsf{Eva} plug-in:
 
-\begin{lstlisting}
+\begin{lstlisting}[language=Dune]
 (libraries [...]
  (select aorai_eva_analysis.ml from
   (frama-c-eva.core -> aorai_eva_analysis.enabled.ml)
   (  -> aorai_eva_analysis.disabled.ml)
- )
+ ))
 \end{lstlisting}
 
 In the example above, \textsf{Aoraï} defines two files:
@@ -153,7 +153,7 @@ via the \verb|%{lib-available:<lib>}| special variable.
 Here is an example from \textsf{Frama-Clang}, which requires the following
 libraries:
 
-\begin{lstlisting}
+\begin{lstlisting}[language=Dune]
 (libraries frama-c.kernel frama-c-wp.core camlp-streams zarith)
 \end{lstlisting}
 
@@ -161,7 +161,7 @@ Its plug-in library name is \verb|frama-clang.core|. Its availability
 must be displayed as the ``summary'' of the configuration, written as the first
 line, with each dependency as a subitem:
 
-\begin{lstlisting}
+\begin{lstlisting}[language=Dune]
 (rule
  (alias frama-c-configure)
  (deps (universe))
@@ -285,7 +285,7 @@ If you simply want to re-run all tests for your plug-in, run \verb|make tests|.
 This is the file structure of the \verb|tests| directory, where \framac
 plug-ins are expected to place their tests:
 
-\begin{lstlisting}
+\begin{lstlisting}[language={}]
 <plug-in directory>
 +- tests
    +- ptests_config
@@ -911,10 +911,11 @@ explain how to add more information to this file to handle some common cases.
 ( rule
   (alias frama-c-configure)
   (deps (universe))
-  (action ( progn
-            (echo "MyPlugin:" %{lib-available:frama-c-myplugin.core} "\n")
-            (echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n")
-          )
+  (action
+    ( progn
+        (echo "MyPlugin:" %{lib-available:frama-c-myplugin.core} "\n")
+        (echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n")
+    )
   )
 )
 
@@ -928,7 +929,8 @@ explain how to add more information to this file to handle some common cases.
 
 ( plugin
   (optional)
-  (name myplugin) (libraries frama-c-myplugin.core) (site (frama-c plugins))
+  (name myplugin)
+    (libraries frama-c-myplugin.core) (site (frama-c plugins))
 )
 \end{lstlisting}
 
@@ -1000,7 +1002,9 @@ indicated in the \texttt{libraries} field:
   (name myplugin_gui)
   (public_name frama-c-myplugin.gui)
   (optional)
-  (flags -open Frama_c_kernel -open Frama_c_gui -open MyPlugin :standard)
+  (flags -open Frama_c_kernel
+         -open Frama_c_gui
+         -open MyPlugin :standard)
   (libraries frama-c.kernel frama-c.gui frama-c-myplugin.core)
 )
 
@@ -1061,10 +1065,10 @@ DEFAULT_SUITES=basic eva wp
 \end{lstlisting}
 
 For most plug-ins, these modifications should be enough so that:
-\begin{lstlisting}[language=shell]
+\begin{logs}
 dune exec -- frama-c-ptests
 dune build @ptests
-\end{lstlisting}
+\end{logs}
 behaves in expected way.
 
 For more advanced usage of \texttt{ptests} please refer to Section~\ref{adv:ptests}.
@@ -2255,10 +2259,10 @@ Kernel.feedback "%B" (Eva.Analysis.is_computed ()); (* false *)
 \end{ocamlcode}
 As the value analysis has been automatically reset when setting the entry point,
 the above code outputs
-\begin{shell}
+\begin{logs}
 [kernel] true
 [kernel] false
-\end{shell}
+\end{logs}
 \end{example}
 \end{itemize}
 
@@ -2648,11 +2652,11 @@ with Project.IOError _ ->
   Kernel.abort "error while loading"
 \end{ocamlcode}
 displays
-\begin{shell}
+\begin{logs}
 [kernel] false
 [kernel] true
 [kernel] false
-\end{shell}
+\end{logs}
 This example shows that the value analysis has been computed only in project
 \texttt{foo} and not in project \texttt{old}.
 \end{example}
@@ -2688,11 +2692,11 @@ with Project.IOError _ ->
   exit 1
 \end{ocamlcode}
 It displays
-\begin{shell}
+\begin{logs}
 false
 true
 false
-\end{shell}
+\end{logs}
 \end{example}
 
 \subsection{Selections}\label{proj:selection}\index{Selection|bfit}
diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex
index 93447ef6696465ed1fc26150e23670875dbb9c40..c8c9565f28d9561c5cb68f967c644e221560cf60 100644
--- a/doc/developer/developer.tex
+++ b/doc/developer/developer.tex
@@ -120,9 +120,7 @@ making figures of this document.
 
 \medskip
 
-\acknowledgeANR{
-  the French ANR projects CAT~(ANR-05-RNTL-00301)
-}
+\acknowledgeANR{the French ANR projects CAT~(ANR-05-RNTL-00301)}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/doc/developer/examples/callstack/callstack.ml b/doc/developer/examples/callstack/callstack.ml
index 4ef550b94769a896f446ff8fe7d3edd3afa121b5..24ca65abfb8ade19833166c553360a082163f3cb 100644
--- a/doc/developer/examples/callstack/callstack.ml
+++ b/doc/developer/examples/callstack/callstack.ml
@@ -7,8 +7,8 @@ module P =
     end)
 
 (* A callstack is a list of a pair (kf * stmt) where [kf] is the kernel
-   function called at statement [stmt]. Building the datatype also creates the
-   corresponding type value [ty]. *)
+   function called at statement [stmt]. Building the datatype also
+   creates the corresponding type value [ty]. *)
 type callstack = (Kernel_function.t * Cil_datatype.Stmt.t) list
 
 (* Implementation *)
diff --git a/doc/developer/examples/syntactic_check/syntactic_check.ml b/doc/developer/examples/syntactic_check/syntactic_check.ml
index 9b2d02ce56dab7c43f114a00b7b3780898f9aa4d..604d1885603bcdec9502f303603e75d2be66b608 100644
--- a/doc/developer/examples/syntactic_check/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check/syntactic_check.ml
@@ -26,20 +26,21 @@ class non_zero_divisor prj = object (self)
       let denom = Visitor.visitFramacExpr self#frama_c_plain_copy denom in
       let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
       let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
-      (* At this point, we have built the assertion we want to insert. It remains
-         to attach it to the correct statement. The cil visitor maintains the
-         information of which statement and function are currently visited in
-         the [current_stmt] and [current_kf] methods, which return None when
-         outside of a statement or a function , e.g. when visiting a global
-         declaration. Here, it necessarily returns [Some]. *)
+      (* At this point, we have built the assertion we want to insert. It
+         remains to attach it to the correct statement. The cil visitor
+         maintains the information of which statement and function are
+         currently visited in the [current_stmt] and [current_kf] methods,
+         which return None when outside of a statement or a function , e.g.
+         when visiting a global declaration. Here, it necessarily returns
+         [Some]. *)
       let stmt = match self#current_kinstr with
         | Kglobal -> assert false
         | Kstmt s -> s
       in
       let kf = Option.get self#current_kf in
-      (* The above statement and function are related to the original project. We
-         need to attach the new assertion to the corresponding statement and
-         function of the new project. Cil provides functions to convert a
+      (* The above statement and function are related to the original project.
+         We need to attach the new assertion to the corresponding statement
+         and function of the new project. Cil provides functions to convert a
          statement (function) of the original project to the corresponding
          one of the new project. *)
       let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 1a6e0debb5ffef55a4fff74512b1dd83d1afad71..0f68c6a8e95789c32b2ebd7c7bb7048e51388b67 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -322,11 +322,11 @@ general services instead\footnote{However, writing to a new file using standard
 \scodeidx{Plugin}{Register}
 
 Running this script yields the following output:
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c
 [hello] Hello, world!
 [hello] 11 * 5 = 55
-\end{shell}
+\end{frama-c-commands}
 
 The \texttt{result} routine is the function to use to output results of your
 plug-in. The \framac output routines take the same arguments as the \caml
@@ -343,12 +343,12 @@ seeing the progress of a fast operation (simple multiplication). The default
 log level is 1, so by default this message is not displayed. To see
 it, the verbosity of the \texttt{hello} plug-in must be increased:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c -hello-verbose 2
 [hello] Hello, world!
 [hello] Computing the product of 11 and 5...
 [hello] 11 * 5 = 55
-\end{shell}
+\end{frama-c-commands}
 
 For a comprehensive list of logging routines and options, see
 Section~\ref{adv:log}.
@@ -381,17 +381,17 @@ default value (here, \texttt{"-"}). The values of these options are obtained
 
 With this change, the hello message is displayed only if \framac is
 executed with the \texttt{-hello} option.
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c
 \$ dune exec -- frama-c -hello
 [hello] Hello, world!
 \$ dune exec -- frama-c -hello -hello-output hello.out
 \$ ls hello.out
 hello.out
-\end{shell}
+\end{frama-c-commands}
 
 These new options also appear in the inline help for the hello plug-in:
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c -hello-help
 ...
 ***** LIST OF AVAILABLE OPTIONS:
@@ -401,7 +401,7 @@ These new options also appear in the inline help for the hello plug-in:
 -hello-output <output-file>  file where the message is output (default:
                     output to the console)
 ...
-\end{shell}
+\end{frama-c-commands}
 
 \subsection{About the plug-in build process}
 
@@ -486,7 +486,7 @@ to perform the tests is called \ptests\index{Ptests}.
 This is the general layout of the \texttt{tests} directory in a \framac
 plug-in; each file will be explained later.
 
-\begin{shell}[breaklines=true]
+\begin{logs}[breaklines=true]
 <plug-in directory>
 +- tests
    +- ptests_config
@@ -502,7 +502,7 @@ plug-in; each file will be explained later.
          +- test1.0.exec.wtests
          +- ...
   +- ...
-\end{shell}
+\end{logs}
 
 Inside the \texttt{tests} directory, \verb|ptests_config| lists the
 {\em test suites}, \ie directories containing tests.
@@ -562,15 +562,15 @@ Then, one can execute the tests and get the output generated by the plug-in,
 by running \verb|dune build @ptests|. Note that if you forget the intermediate
 step of running \verb|frama-c-ptests|, you may end up with the following error:
 
-\begin{shell}[breaklines=true]
+\begin{logs}[breaklines=true]
 Error: Alias "ptests" specified on the command line is empty.
 It is not defined in tests or any of its descendants.
-\end{shell}
+\end{logs}
 
 But with the \texttt{dune} files generated by \verb|frama-c-ptests|, you can
 run the tests:
 
-\begin{shell}[breaklines=true]
+\begin{frama-c-commands}[breaklines=true]
 \$ dune build @ptests
 Files ../oracle/hello_test.res.oracle and hello_test.res.log differ
 % dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
@@ -585,7 +585,7 @@ index e69de29..5f6ab23 100644
 @@ -0,0 +1,2 @@
 +[kernel] Parsing hello_test.c (with preprocessing)
 +[hello] Hello, world!
-\end{shell}
+\end{frama-c-commands}
 
 There is a lot of information in the output. The relevant parts
 can be summarized as:
@@ -939,9 +939,9 @@ With all of this, we can compile the project with:
 
 And run it as a \framac plugin:
 
-\begin{shell}
+\begin{frama-c-commands}
   dune exec -- frama-c [options] file.c [file2.c]
-\end{shell}
+\end{frama-c-commands}
 
 And the graph can be visualized with an external tool, such as {\em dotty} or
 {\em xdot}.
@@ -953,7 +953,7 @@ This produces a graph like in Figure~\ref{fig:tut:basiccfg}
 
 \begin{figure}[htbp]
   \centering
-  \begin{minipage}[h]{0.45\linewidth}
+  \begin{minipage}[h]{0.47\linewidth}
   \listingname{test.c}
   \cinput[linerange={5-999}]{./tutorial/viewcfg/v1-simple/tests/viewcfg/test.c}
   \end{minipage}%
@@ -1065,9 +1065,9 @@ To test this code, we recompile the plug-in with the modified \texttt{dune}
 file to take into account the dependency on \textsf{Eva}, as well as the
 modified \texttt{vstmt\_aux}. We run \verb|dune build @install| and then
 we run \textsf{Eva}, and then our plug-in:
-\begin{shell}
+\begin{frama-c-commands}
   dune exec -- frama-c test.c -eva -then -cfg && dotty cfg.dot
-\end{shell}
+\end{frama-c-commands}
 
 The relative order of most options and file names is not important
 {\em between} occurrences of \texttt{-then}, but it {\em is} important
@@ -1084,7 +1084,7 @@ The resulting graph is shown in Figure~\ref{fig:tut:coloredcfg}.
 
 \begin{figure}[htbp]
   \centering
-  \begin{minipage}[h]{0.45\linewidth}
+  \begin{minipage}[h]{0.47\linewidth}
   \listingname{test.c}
   \cinput[linerange={5-999}]{./tutorial/viewcfg/v3-eva/tests/viewcfg/test.c}
   \end{minipage}%
@@ -1284,9 +1284,9 @@ saved so that later calls to \texttt{dump\_function} with the same
 
 To check this, we re-run our mini-GUI with:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c <file> -cfg-gui
-\end{shell}
+\end{frama-c-commands}
 
 The first graph for each function will show the message
 ``Computing CFG for function ...'', but subsequent calls will no longer do it.
@@ -1294,18 +1294,18 @@ The first graph for each function will show the message
 Also, we can see the effects of the dependency on the \textsf{Eva} plug-in
 by first launching the value analysis and then our plug-in:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c <file> -eva -then -cfg-gui
-\end{shell}
+\end{frama-c-commands}
 
 In this case, the graphs will be colored.
 
 Finally, to check that the state dependency on \textsf{Eva} works, we will use
 a more complex command line:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c <file> -eva -then -cfg-gui -then -main f
-\end{shell}
+\end{frama-c-commands}
 
 We have three stages: first run \textsf{Eva}, then open the mini-GUI, then
 change the entry point (\verb|-main f| means that the program will start
@@ -1329,16 +1329,16 @@ when we ask again for the CFG.
 Another way to observe how \framac automatically handles states is to display a
 CFG, save the session (option \verb|-save <file>|), and then load it again:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c <file> -eva -then -cfg-gui -save session.sav
-\end{shell}
+\end{frama-c-commands}
 
 Then click on the ``Show CFG'' (see the feedback message), then close the CFG
 and the mini-GUI. Reload the session:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ dune exec -- frama-c -load session.sav
-\end{shell}
+\end{frama-c-commands}
 
 Click ``Show CFG'' and you will {\em not} see the ``Computing CFG'' message:
 the state \texttt{Cfg\_graph\_state} had beem automatically saved by \framac
diff --git a/doc/developer/tutorial/viewcfg/v5-state/dump.ml b/doc/developer/tutorial/viewcfg/v5-state/dump.ml
index bccac711ae0003ecfe59e517e248cf8880f74984..cc49bf0bcb6fc5d9e5f5d25e26873c50504d415f 100644
--- a/doc/developer/tutorial/viewcfg/v5-state/dump.ml
+++ b/doc/developer/tutorial/viewcfg/v5-state/dump.ml
@@ -4,7 +4,8 @@ let dump_to_string fundec =
   Options.Self.feedback "Computing CFG for function %s"
     (fundec.svar.vorig_name);
   ignore
-    (Visitor.visitFramacFunction (new Visit.print_cfg Format.str_formatter) fundec);
+    (Visitor.visitFramacFunction
+      (new Visit.print_cfg Format.str_formatter) fundec);
   Format.flush_str_formatter ()
 
 module Cfg_graph_state = State_builder.Hashtbl