diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 1e84ae3f41bba4b63949db5436f46daebf8424ae..29b1224a65adea79c4ef487797cfac343a301956 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -588,8 +588,8 @@
 
 \lstdefinelanguage{frama-c-commands}[]{}{%
   mathescape=false,%
-  alsoletter=-,%
-  keywords={frama-c,frama-c-gui,frama-c-script},%
+  alsoletter=-.,%
+  keywords={e-acsl-gcc.sh,frama-c,frama-c-gui,frama-c-script},%
   classoffset=1,%
   morekeywords={-load,-then,-then-last,-then-on,-then-replace,-save},%
   classoffset=0,%
@@ -638,7 +638,9 @@
 
 \lstdefinelanguage{Logs}[]{}{%
   style=frama-c-basic-style,
-  backgroundcolor=
+  mathescape=false,
+  backgroundcolor=,
+  literate={\\\$}{\$}1
 }
 
 \newcommand{\logsinput}[1]%
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index e6b5595433569541dee778ed6abe3702a5ab5f0f..3e816ad9239fb352d2bc753276f595603fa0b819 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -38,7 +38,7 @@ as in the following line:
 
 As a summary, Figure~\ref{fig:notyet} synthetizes main features that are not
 currently implemented into the \framac's \eacsl plug-in.
-\begin{figure}[htbp]\label{fig:notyet}
+\begin{figure}[htbp]
   \begin{center}
     \begin{tabular}{|l|l|}
       \hline
@@ -99,6 +99,7 @@ currently implemented into the \framac's \eacsl plug-in.
     \end{tabular}
   \end{center}
   \caption{Summary of not-yet-implemented features.}
+  \label{fig:notyet}
 \end{figure}
 }%
 {}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index c25d099a06f8dc41760646ccead9cbcf8c34ed6d..f23a0c27675b37eca732b9e47b47476262db032b 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -107,7 +107,7 @@ This work has been initially supported by the ‘Hi-Lite’ FUI project (FUI AAP
 \chapter{Appendices}
 \label{chap:appendix}
 
-\include{changes_modern}
+\input{changes_modern}
 
 \cleardoublepage
 \addcontentsline{toc}{chapter}{\bibname}
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
index 1610681b16dbce6e48a5f08934ecb5fb1c24320d..07ec57256901d02d302a3a43f0054de5871f1f90 100644
--- a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
+++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
@@ -1,5 +1,5 @@
-\begin{shell}
-\$ frama-c -e-acsl first.i -then-last -print
+\begin{logs}
+$ frama-c -e-acsl first.i -then-last -print
 [kernel] Parsing first.i (no preprocessing)
 [e-acsl] beginning translation.
 [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
@@ -69,4 +69,4 @@ int main(void)
   __retres = 0;
   return __retres;
 }
-\end{shell}
+\end{logs}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 1a20cd3d97cc68c063e915f3819b1d27b1404a4c..276fb6d76c7c805b261bce6776ae8e498826b5e9 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -55,13 +55,13 @@ actually undefined because the assertion reads the uninitialized variable
 \lstinline|x|. You should be caught by the \eacsl plug-in, but that is not
 the case yet.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh uninitialized.i -c -Omonitored_uninitialized
 monitored_uninitialized.i: In function 'main':
 monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function
 [-Wuninitialized]
 \$ ./monitored_uninitialized.e-acsl
-\end{shell}
+\end{logs}
 
 This is more a design choice than a limitation: should the \eacsl plug-in
 generate additional instrumentation to prevent such values from being evaluated,
@@ -98,7 +98,7 @@ Consider the following example.
 \cinput{examples/valid_no_main.c}
 
 You can generate the instrumented program as follows.
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -M -omonitored_valid_no_main.i valid_no_main.c
 [kernel] Parsing valid_no_main.c (with preprocessing)
 [e-acsl] beginning translation.
@@ -107,7 +107,7 @@ You can generate the instrumented program as follows.
   you must call functions `__e_acsl_globals_init', `__e_acsl_globals_clean',
   `__e_acsl_memory_init' and `__e_acsl_memory_clean' by yourself.
 [e-acsl] translation done in project "e-acsl".
-\end{shell}
+\end{logs}
 
 The last warning states an important point: if this program is linked against
 another file containing \texttt{main} function, then this main function must
@@ -129,7 +129,7 @@ While it is possible to add such intrumentation manually we recommend using
 
 Then just compile and run it as explained in Section~\ref{sec:memory}.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
 \$ e-acsl-gcc.sh -C -Ovalid_no_main monitored_modified_main.i monitored_valid_no_main.i
 \$ ./valid_no_main.e-acsl
@@ -137,7 +137,7 @@ Assertion failed at line 11 in function f.
 The failing predicate is:
 freed: \valid(x).
 Aborted
-\end{shell}
+\end{logs}
 
 Also, if the unprovided main initializes some variables, running the
 instrumented code (linked against this main) could print some warnings from the
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index fd162c8c44db96a546cbf505d83dd8dc0e6ef730..7e5b59bf5687c3bfe9de36e114919d0d0b0fe5fc 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -94,9 +94,9 @@ Section~\ref{sec:exec}.
 
 Using \shortopt{ocode} \framac~\cite{userman} option, the code generated by the
 \eacsl plug-in can be redirected into a file as follows:
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c
-\end{shell}
+\end{frama-c-commands}
 
 \framac uses architecture-dependent configuration which
 affects sizes of integer types, endianness and potentially other features.  It
@@ -112,17 +112,17 @@ important that the architecture used by \framac matches the architecture
 corresponding to your compiler and your system. For instance, in a 32-bit
 machine you should also pass
 \shortopt{machdep} \texttt{x86\_32} option as follows:
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -machdep x86_32 -e-acsl first.i -then-last \
   -print -ocode monitored_first.c
-\end{shell}
+\end{frama-c-commands}
 
 This file can be compile with a \C compiler (for instance \gcc), as follows:
 
 \lstset{escapechar=£}
-\begin{shell}
+\begin{frama-c-commands}
 \$ gcc -c -Wno-attributes monitored_first.c
-\end{shell}
+\end{frama-c-commands}
 
 However, creating an executable through a proper invokation to \gcc is painful
 and is not documented. Instead, \eacsl comes with a companion wrapper script for
@@ -149,9 +149,9 @@ In this section we describe \eacslgcc and provide several examples of its use.
 The default behaviour of \eacslgcc is to instrument an annotated C program
 with runtime assertions via a run of \framac.
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -omonitored_first.i first.i
-\end{shell}
+\end{frama-c-commands}
 
 The above command instruments \texttt{first.i} with runtime assertions and
 outputs the generated code to \texttt{monitored\_first.i}. Unless the name of
@@ -162,9 +162,9 @@ code is placed to a file named \texttt{a.out.frama.c}.
 Compilation and Linking of the original and the instrumented sources
 is enabled using the \shortopt{c} option.  For instance, command
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -c -omonitored_first.i first.i
-\end{shell}
+\end{frama-c-commands}
 
 instruments the code in \texttt{first.i}, outputs it to
 \texttt{monitored\_first.i} and produces 2 executables: \texttt{a.out} and
@@ -174,7 +174,7 @@ instruments the code in \texttt{first.i}, outputs it to
 
 You can execute the generate binaries, in particular \texttt{a.out.e-acsl} which
 detects at runtime the incorrect annotation.
-\begin{shell}
+\begin{logs}
 \$ ./a.out.e-acsl
 first.i: In function 'main'
 first.i:4: Error: Assertion failed:
@@ -183,7 +183,7 @@ first.i:4: Error: Assertion failed:
 Aborted (core dumped)
 \$ echo \$?
 134
-\end{shell}
+\end{logs}
 The execution aborts with a non-zero exit code (134) and an error message
 indicating an \eacsl annotation that has been violated. There is no output for
 the valid \eacsl annotation. That is, the run of an executable generated from
@@ -197,9 +197,9 @@ generated from the original program and the executable generated from the
 \eacsl-instrumented code is suffixed \texttt{.e-acsl}.
 
 For example, command
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
-\end{shell}
+\end{frama-c-commands}
 names the executables generated from \texttt{first.i} and
 \texttt{monitored\_first.i}: \texttt{monitored\_first} and
 \texttt{monitored\_first.e-acsl} respectively.
@@ -209,9 +209,9 @@ compile a given program as if it was already instrumented by the \eacsl
 plug-in.  This option is useful if one makes changes to an already
 instrumented source file by hand and only wants to recompile it.
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
-\end{shell}
+\end{frama-c-commands}
 
 The above command generates a single executable named
 \texttt{monitored\_first.e-acsl}. This is because \texttt{monitored\_first.i} is
@@ -226,18 +226,18 @@ with an appropriate error message. Paths to \framac and \gcc executables can
 also be passed using \shortopt{I} and \shortopt{G} options
 respectively, for instance as follows:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
-\end{shell}
+\end{frama-c-commands}
 
 Runs of \framac and \gcc issued by \eacslgcc can further be customized by using
 additional flags.  \framac flags can be passed using the \shortopt{F} option,
 while \shortopt{e} and \shortopt{l} options allow for passing additional
 pre-processor and linker flags during \gcc invocations.  For example, command
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
-\end{shell}
+\end{frama-c-commands}
 
 yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
 are output using the UTF-8 character set. Further, during the compilation of
@@ -260,9 +260,9 @@ instance, to increase the verbosity of plug-ins but suppress the verbosity of
 the \framac kernel while instrumenting \texttt{foo.c} one can use the following
 command:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
-\end{shell}
+\end{frama-c-commands}
 
 Verbosity of the \eacslgcc output can also be reduced using the \shortopt{q}
 option that suppresses any output except errors or warnings issued by \gcc,
@@ -273,9 +273,9 @@ The output of \eacslgcc can also be redirected to a specified file using the
 output during instrumentation and compilation of \texttt{foo.c} to the
 file named \texttt{/tmp/log}.
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
-\end{shell}
+\end{frama-c-commands}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{Architecture Dependency}
@@ -314,9 +314,9 @@ executables with ABI different to the default one.
 using the option \longopt{concurrency} of  \eacslgcc.
 
 Example of compilation with concurrency support using \eacslgcc:
-\begin{shell}
+\begin{frama-c-commands}
   \$ e-acsl-gcc.sh -c foo.c --concurrency -o foo.frama.c -O foo
-\end{shell}
+\end{frama-c-commands}
 
 The concurrency support is a two part activation: first the
 \longopt{e-acsl-concurrency} \framac option is enabled to generate concurrent
@@ -328,7 +328,7 @@ Example of compilation with concurrency support using \framac and \gcc directly
 (where \texttt{\$E\_ACSL\_SHARE} points to the \texttt{share/frama-c/e-acsl}
 folder of \framac and \texttt{\$E\_ACSL\_LIB} points to the
 \texttt{lib/frama-c/e-acsl} folder of \framac):
-\begin{shell}
+\begin{frama-c-commands}
   \$ frama-c \
         -remove-unused-specified-functions \
         -machdep gcc_x86_64 \
@@ -349,7 +349,7 @@ folder of \framac and \texttt{\$E\_ACSL\_LIB} points to the
         -pthread \
         \$E_ACSL_LIB/libeacsl-dlmalloc.a \
         -lgmp -lm
-\end{shell}
+\end{frama-c-commands}
 
 \subsubsection{Function Contracts Limitations}
 
@@ -457,20 +457,20 @@ are undefined in the context of the \T{main} function call since the second
 argument is equal to 0.  However, we can generate an instrumented code and
 compile it using the following command:
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c -omonitored_rte.i -Orte rte.i
-\end{shell}
+\end{logs}
 
 Now, when \T{rte.e-acsl} is executed, you get the following output indicating
 that your function contract is invalid because it contains a division by zero.
 
-\begin{shell}
+\begin{logs}
 \$ ./rte.e-acsl
 RTE failed at line 5 in function is_dividable.
 The failing predicate is:
 division_by_zero: y != 0.
 Aborted
-\end{shell}
+\end{logs}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -554,7 +554,7 @@ allocated via \texttt{malloc} has been deallocated and \T{x} is a stale pointer
 referencing unallocated memory.  The execution of the instrumented program thus
 reports the violation of the second annotation:
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c -Ovalid valid.c
 \$ ./valid.e-acsl
 valid.c: In function 'main'
@@ -562,7 +562,7 @@ valid.c:11: Error: Assertion failed:
         The failing predicate is:
         freed: \valid(x).
 Aborted (core dumped)
-\end{shell}
+\end{logs}
 
 To check memory-related predicates (such as \lstinline|\valid|) \eacsl tracks
 memory allocated by a program at runtime. \eacsl records memory blocks in a
@@ -600,19 +600,19 @@ system-wide \T{malloc} and similar functions (e.g., \T{calloc} or \T{free}).
 At the level of \eacslgcc you can choose between different memory models using
 the \shortopt{m} switch followed by the name of the memory model to link
 against.  For instance, command
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -mbittree -c -Ovalid valid.c
-\end{shell}
+\end{logs}
 links a program generated from \T{valid.c} against the library implementing the
 bittree-based memory model, whereas the following invocation uses shadow-based
 tracking:
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -msegment -c -Ovalid valid.c
-\end{shell}
+\end{logs}
 It is also possible to generate executables using both models as follows:
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -msegment,bittree -c -Ovalid valid.c
-\end{shell}
+\end{logs}
 In this case, \eacslgcc produces 3 executables: \T{valid},
 \T{valid.e-acsl-segment} and \T{valid.e-acsl-bittree} corresponding to an
 executable generated from the original source code, and the executables
@@ -728,9 +728,9 @@ that uses \texttt{exit(CODE)} instead of \texttt{abort}.
 
 For instance, the program generated using the following command
 exits with code \texttt{5} on a predicate violation.
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
-\end{shell}
+\end{logs}
 
 Forceful termination of a monitored program can be disabled using
 \longopt{keep-going} option. If specified, \eacslgcc generates code that
@@ -779,19 +779,19 @@ as follows using \longopt{external-assert} option of \eacslgcc to replace the
 default implementation of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
 with the customized one specified in \texttt{my\_assert.c}.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c -X first.i -Ofirst --external-assert=my_assert.c
 \$ ./first.e-acsl
 Assertion in file first.i at line 3 in function main is valid (trustworthy).
 The verified predicate was: `x == 0'.
 Assertion in file first.i at line 4 in function main is invalid (trustworthy).
 The verified predicate was: `x == 1'.
-\end{shell}
+\end{logs}
 
 The default assertion function prints the values contributing to an assertion
 along with the error message.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c -X first.i -Ofirst
 \$ ./first.e-acsl
 first.i: In function 'main'
@@ -800,19 +800,19 @@ first.i:4: Error: Assertion failed:
         x == 1.
         With values:
         - x: 0
-\end{shell}
+\end{logs}
 
 This behavior can be overriden by using the \longopt{no-assert-print-data}
 option of \eacslgcc.
 
-\begin{shell}
+\begin{logs}
   \$ e-acsl-gcc.sh -c -X first.i -Ofirst --no-assert-print-data
   \$ ./first.e-acsl
   first.i: In function 'main'
   first.i:4: Error: Assertion failed:
           The failing predicate is:
           x == 1.
-\end{shell}
+\end{logs}
 
 As with the assertion function, \eacslgcc provides a way to use an alternative
 definition of
@@ -842,7 +842,7 @@ replace the default implementation of \texttt{\_\_e\_acsl\_print\_value}
 \codeidxdef{e\_acsl\_print\_value} with the customized one specified in
 \texttt{my\_print\_value.c}.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c -X first.i -Ofirst \
     --external-print-value=my_print_value.c
 \$ ./first.e-acsl
@@ -852,13 +852,13 @@ first.i:4: Error: Assertion failed:
         x == 1.
         With values:
         - custom print for x
-\end{shell}
+\end{logs}
 
 The custom definitions of \texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert}
 and \texttt{\_\_e\_acsl\_print\_value}\codeidxdef{e\_acsl\_print\_value} can be
 used at the same time.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -c -X first.i -Ofirst \
     --external-assert=my_assert.c \
     --external-print-value=my_print_value.c
@@ -871,7 +871,7 @@ Assertion in file first.i at line 4 in function main is invalid (trustworthy).
 The verified predicate was: `x == 1'.
 With values:
         - custom print for x
-\end{shell}
+\end{logs}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -894,13 +894,13 @@ format.
 
 This error can be detected by \eacsl as follows.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings printf.c
 \$ ./printf.e-acsl
 printf: directive 1 ('%d') expects argument of type 'int' but the corresponding
 argument has type 'char*'
 Abort
-\end{shell}
+\end{logs}
 
 \subsection{Incorrect Usage of Libc Functions}
 \index{Libc}
@@ -928,12 +928,12 @@ destination string should contain at least 7 \texttt{char} (and not only 6).
 
 This error can be reported by \eacsl as follows.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -Ostrcpy -c --libc-replacements strcpy.c
 \$ ./strcpy.e-acsl
 strlen: insufficient space in destination string, at least 7 bytes required
 Abort
-\end{shell}
+\end{logs}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -964,7 +964,7 @@ Consider for instance the following annotated program without \texttt{main}.
 
 The instrumented code is generated as usual, even though you get an additional
 warning.
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
 [kernel] Parsing no_main.i (no preprocessing)
 [e-acsl] beginning translation.
@@ -974,7 +974,7 @@ warning.
   The generated program may miss memory instrumentation
   if there are memory-related annotations.
 [e-acsl] translation done in project "e-acsl".
-\end{shell}
+\end{logs}
 
 This warning indicates that the instrumentation could be incorrect if the
 program contains memory-related annotations (see
@@ -986,11 +986,11 @@ the following:
 \listingname{main.c}
 \cinput{examples/main.c}
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -C monitored_no_main.i main.c -Owith_main
 \$ ./with_main.e-acsl
 x = 65536
-\end{shell}
+\end{logs}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -1008,7 +1008,7 @@ following annotated program for which the implementation of the function
 
 The instrumented code is generated as usual, even though you get an additional
 warning.
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -omonitored_no_code.i no_code.c
 [kernel] Parsing no_code.c (with preprocessing)
 [e-acsl] beginning translation.
@@ -1017,7 +1017,7 @@ warning.
   if there are memory-related annotations.
 [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
 [e-acsl] translation done in project "e-acsl".
-\end{shell}
+\end{logs}
 
 Similar to the previous Section the warning indicates that the instrumentation
 could be incorrect if the program contains memory-related annotations (see
@@ -1030,7 +1030,7 @@ safely ignore it.
 Similar to the example shown in the previous section you can generate the
 executable by providing definition of \T{my\_pow}.
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i
 \$ ./no_code.e-acsl
 no_code.c: In function 'my_pow'
@@ -1038,7 +1038,7 @@ no_code.c:5: Error: Postcondition failed:
         The failing predicate is:
         even: \result >= 1.
 Aborted (core dumped)
-\end{shell}
+\end{logs}
 
 The execution of the corresponding binary fails at runtime: actually, our
 implementation of the function \texttt{my\_pow} overflows in case of large
@@ -1088,16 +1088,16 @@ Consider the following example in which all assertions are valid.
 
 One can ask to not instrument function \texttt{g} (\emph{i.e.} to instrument
 only functions \texttt{f} and \texttt{main}) through the following command.
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh \
   -c --oexec-e-acsl partial.out \
   --e-acsl-extra="-e-acsl-instrument=+@all,-g" \
   partial.i
-\end{shell}
+\end{logs}
 
 Therefore, running the generated executable \texttt{partial.out} leads to the
 following verdicts.
-\begin{shell}
+\begin{logs}
 \$ ./partial.out
 partial.i: In function 'main'
 partial.i:16: Warning: no sound verdict for Assertion (guess: ok).
@@ -1107,7 +1107,7 @@ partial.i: In function 'main'
 partial.i:17: Warning: no sound verdict for Assertion (guess: FAIL).
         the considered predicate is:
         \initialized(&t[2])
-\end{shell}
+\end{logs}
 
 First, there is no message for the first assertion about the initialization of
 \texttt{\&t[0]}, meaning that this assertion is silently checked as valid by
@@ -1151,18 +1151,18 @@ Consider the following program.
 To check at runtime that this program does not perform any runtime error (which
 are potential overflows in this case), just do:
 
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -rte combine.i -then -e-acsl -then-last -print
   -ocode monitored_combine.c
 \$ e-acsl-gcc.sh -C -Ocombine monitored_combine.c
 \$ ./combine.e-acsl
-\end{shell}
+\end{frama-c-commands}
 
 Automatic assertion generation can also be enabled via \eacslgcc directly via
 the following command:
-\begin{shell}
+\begin{frama-c-commands}
 \$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all combine.i
-\end{shell}
+\end{frama-c-commands}
 
 Note the use of \eacslgcc \longopt{rte} option which asks \framac to combine
 \eacsl with \rte plug-in. This plug-in automatically instruments the input
@@ -1182,15 +1182,15 @@ proven valid by another plug-in, except if you explicitly set the option
 prove that there is no potential overflow in the previous program, so the \eacsl
 plug-in does not generate additional code for checking them if you run the
 following command.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -rte combine.i -then -eva -then -e-acsl \
   -then-last -print -ocode monitored_combine.i
-\end{shell}
+\end{frama-c-commands}
 The additional code will be generated with the two following command.
-\begin{shell}
+\begin{frama-c-commands}
 \$ frama-c -rte combine.i -then -eva -then -e-acsl \
   -e-acsl-valid -then-last -print -ocode monitored_combine.i
-\end{shell}
+\end{frama-c-commands}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1208,13 +1208,13 @@ you can pass it using \shortopt{F} switch:
 \listingname{check.i}
 \cinput{examples/check.i}
 
-\begin{shell}
+\begin{logs}
 \$ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i
 [kernel] Parsing check.i (no preprocessing)
 [e-acsl] beginning translation.
 [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
 [e-acsl] translation done in project "foobar".
-\end{shell}
+\end{logs}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%