diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index a688b58cb2e19ef05641b190138dbc5aea7024ff..de091b1c3a4e0a844d974433da8547e89beefa67 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,11 @@ release. First we list changes of the last release.
 
 \section*{\nextframacversion}
 
+\begin{itemize}
+\item \textbf{Preparing the Sources:} added option
+  \texttt{-print-cpp-commands}.
+\end{itemize}
+
 \section*{21.0 (Scandium)}
 
 \begin{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 030d362f6f863016ab4cc3de58ce887afb9b8f61..0bb8b4360ed20e101419d6464d87e3603f151742 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -29,34 +29,38 @@ in the figure. Note that some plug-ins, such as \textsf{Variadic}
 (described in chapter~\ref{user-variadic}), perform further AST
 transformations before most analyses are run.
 
-\section{Pre-processing the Source Files}\label{sec:preprocessing}
+\section{Preprocessing the Source Files}\label{sec:preprocessing}
 
 The list of files to analyze must be provided on the command line, or
 chosen interactively in the GUI. Files with the suffix
-{\tt .i} are assumed to be already pre-processed \C files. \FramaC
-pre-processes the other files with the following command.
+{\tt .i} are assumed to be already preprocessed \C files. \FramaC
+preprocesses {\tt .c} and {\tt .h} files with the following basic command:
 \begin{shell}
 \$ gcc -C -E -I .
 \end{shell}
+Plus some architecture-dependent flags. The {\em exact} preprocessing command
+line can be obtained via options \texttt{-kernel-msg-key pp} and
+\optiondef{-}{print-cpp-commands} (the latter exits \FramaC after printing).
 
 Option \optiondef{-}{cpp-extra-args} can be used to add arguments to the
-default pre-processing command, typically via the inclusion of defines
+default preprocessing command, typically via the inclusion of defines
 (\texttt{-D} switches) and header directories (\texttt{-I} switches), as in
 \texttt{-cpp-extra-args="-DDEBUG -DARCH=ia32 -I./headers"}.
 You can also add arguments on a per-file basis, using option
 \optiondef{-}{cpp-extra-args-per-file}.
 
-If you need to, you can also {\em replace} the pre-processing command
+If you need to, you can also {\em replace} the preprocessing command
 entirely with option \optiondef{-}{cpp-command}. Placeholders (see below)
 can be used for advanced commands.
-If no placeholders are used, the pre-processor is invoked in the
+If no placeholders are used, the preprocessor is invoked in the
 following way.
 \begin{commands}
-\texttt{<cmd> <args> -o <output file> <input file>}
+\texttt{<cmd> <args> <input file> -o <output file>}
 \end{commands}
 
-In this command, \texttt{<output file>} is chosen by \FramaC while
-\texttt{<input file>} is one of the filenames provided by the user.
+In this command, \texttt{<output file>} is a temporary filename chosen by
+\FramaC while \texttt{<input file>} is one of the filenames provided by the
+user.
 
 For commands which do not follow this pattern, it is also possible to use
 the following placeholders:
@@ -103,29 +107,29 @@ are ignored. Also note that the use of the database simply adds flags
 be specified by the user.
 
 In all of the above cases,
-\acsl annotations are pre-processed by default (option \optiondef{-}{pp-annot}
-is set by default). Unless a custom pre-processor is specified
+\acsl annotations are preprocessed by default (option \optiondef{-}{pp-annot}
+is set by default). Unless a custom preprocessor is specified
 (via \optionuse{-}{cpp-frama-c-compliant}), \FramaC considers that \gcc is
-installed and uses it as pre-processor.
-If you do \emph{not} want annotations to be pre-processed, you need to pass
+installed and uses it as preprocessor.
+If you do \emph{not} want annotations to be preprocessed, you need to pass
 option \texttt{-no-pp-annot} to \FramaC. Note that some headers in the
 standard C library provided with \FramaC (described below) use such annotations,
 therefore it might be necessary to disable inclusion of such headers.
 
-Also note that ACSL annotations are pre-processed separately from the C
+Also note that ACSL annotations are preprocessed separately from the C
 code in a second pass, and that arguments given as \texttt{-cpp-extra-args} are
-\emph{not} given to the second pass of pre-processing. Instead,
+\emph{not} given to the second pass of preprocessing. Instead,
 \texttt{-pp-annot} relies on the ability of \gcc to output all
 macro definitions (including those given with \texttt{-D}) in the
-pre-processed file. In particular, \texttt{-cpp-extra-args} must be
+preprocessed file. In particular, \texttt{-cpp-extra-args} must be
 used if you are including header files who behave differently
 depending on the number of times they are included.
 
 In addition, files having the suffix \texttt{.ci} will be considered as needing
 preprocessing for ACSL annotations only. Those files may contain
-\texttt{\#define} directives and annotations are pre-processed as explained in
+\texttt{\#define} directives and annotations are preprocessed as explained in
 the previous paragraph. This allows to have macros in ACSL annotations while
-using a non-GNU-like pre-processor.
+using a non-GNU-like preprocessor.
 
 \begin{important}
   An experimental, incomplete, C standard library is bundled with \FramaC and installed
@@ -143,7 +147,7 @@ using a non-GNU-like pre-processor.
 
 \section{Merging the Source Code files}
 
-After pre-processing, \FramaC parses, type-checks and links the source
+After preprocessing, \FramaC parses, type-checks and links the source
 code.  It also performs these operations for the \acsl annotations
 optionally present in the program. Together, these steps form the
 \emph{merging} phase of the creation of an analysis project.
@@ -347,7 +351,7 @@ supported are typedefs redefinition.
 a certain number of C macros. They are summarized below.
 
 \begin{description}
-\item \textttdef{\_\_FRAMAC\_\_}: defined to 1 during pre-processing by \FramaC,
+\item \textttdef{\_\_FRAMAC\_\_}: defined to 1 during preprocessing by \FramaC,
 as if the user had added \texttt{-D\_\_FRAMAC\_\_} to the command line. Useful
 for conditional compilation and detection of an execution by \FramaC.
 
@@ -465,7 +469,7 @@ preparation itself succeeds, by running \FramaC without any option.
 \$ frama-c <input files>
 \end{shell}
 
-If you need to use other options for pre-processing or normalizing the source
+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}
diff --git a/man/frama-c.1 b/man/frama-c.1
index 66cfcd0fea3cb54912b7077fc834d76899be92e8..6eb485315a7f5a8ecc0f79e11f8489f9691269d9 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -25,45 +25,45 @@
 .\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
 .\" and run `make man/frama-c.1`.
 
-.TH FRAMA-C 1 2020-04-02
+.TH FRAMA-C 1 2020-09-01
 .SH NAME
 .PP
-frama\-c[.byte] \- a static analyzer for C programs
+frama-c[.byte] - a static analyzer for C programs
 .PP
-frama\-c\-gui[.byte] \- the graphical interface of frama\-c
+frama-c-gui[.byte] - the graphical interface of frama-c
 .SH SYNOPSIS
 .PP
-\f[B]frama\-c\f[] [ \f[I]options\f[] ] \f[I]files\f[]
+\f[B]frama-c\f[R] [ \f[I]options\f[R] ] \f[I]files\f[R]
 .SH DESCRIPTION
 .PP
-\f[B]frama\-c\f[] is a suite of tools dedicated to the analysis of
+\f[B]frama-c\f[R] is a suite of tools dedicated to the analysis of
 source code written in C.
 It gathers several analysis techniques in a single collaborative
 framework.
 This framework can be extended by additional plugins placed in the
-\f[B]$FRAMAC_PLUGIN\f[] directory.
+\f[B]$FRAMAC_PLUGIN\f[R] directory.
 The command
 .RS
 .PP
-frama\-c \-\-plugins
+frama-c --plugins
 .RE
 .PP
 will provide the full list of the plugins that are currently installed.
 .PP
-\f[B]frama\-c\-gui\f[] is the graphical user interface of
-\f[B]frama\-c\f[].
-It features the same options as the command\-line version.
+\f[B]frama-c-gui\f[R] is the graphical user interface of
+\f[B]frama-c\f[R].
+It features the same options as the command-line version.
 .PP
-\f[B]frama\-c.byte\f[] and \f[B]frama\-c\-gui.byte\f[] are the OCaml
-bytecode versions of the command\-line and graphical user interface
+\f[B]frama-c.byte\f[R] and \f[B]frama-c-gui.byte\f[R] are the OCaml
+bytecode versions of the command-line and graphical user interface
 respectively.
 .PP
-By default, Frama\-C recognizes \f[I].c\f[] files as C files needing
-pre\-processing and \f[I].i\f[] files as C files having been already
-pre\-processed.
+By default, Frama-C recognizes \f[I].c\f[R] files as C files needing
+pre-processing and \f[I].i\f[R] files as C files having been already
+pre-processed.
 Some plugins may extend the list of recognized files.
-Pre\-processing can be customized through the \f[B]\-cpp\-command\f[]
-and \f[B]\-cpp\-extra\-args\f[] options.
+Pre-processing can be customized through the \f[B]-cpp-command\f[R] and
+\f[B]-cpp-extra-args\f[R] options.
 .SH OPTIONS
 .SS Syntax
 .PP
@@ -71,738 +71,553 @@ Options taking an additional parameter can also be written under the
 form
 .RS
 .PP
-\-\f[I]option\f[]=\f[I]param\f[]
+-\f[I]option\f[R]=\f[I]param\f[R]
 .RE
 .PP
-This form is mandatory when \f[I]param\f[] starts with a dash (`\-').
+This form is mandatory when \f[I]param\f[R] starts with a dash (`-').
 .PP
 Most options that take no parameter have a corresponding
 .RS
 .PP
-\-no\-\f[I]option\f[]
+-no-\f[I]option\f[R]
 .RE
 .PP
 option which has the opposite effect.
 .SS Help options
 .TP
-.B \-help
+.B -help
 gives a short usage notice.
-.RS
-.RE
 .TP
-.B \-kernel\-help
-prints the list of options recognized by Frama\-C's kernel
-.RS
-.RE
+.B -kernel-help
+prints the list of options recognized by Frama-C\[cq]s kernel
 .TP
-.B \-explain
+.B -explain
 prints a help message for each other option given on the command line
-.RS
-.RE
 .TP
-.B \-verbose \f[I]n\f[]
+.B -verbose \f[I]n\f[R]
 sets verbosity level.
 Defaults to 1.
 Setting it to 0 will output less progress messages.
-This level can also be set on a per\-\f[I]plugin\f[] basis, with option
-\-\f[I]plugin\f[]\-\f[B]verbose\f[] \f[I]n\f[].
+This level can also be set on a per-\f[I]plugin\f[R] basis, with option
+-\f[I]plugin\f[R]-\f[B]verbose\f[R] \f[I]n\f[R].
 Verbosity level of the kernel can be controlled with option
-\f[B]\-kernel\-verbose\f[] \f[I]n\f[].
-.RS
-.RE
+\f[B]-kernel-verbose\f[R] \f[I]n\f[R].
 .TP
-.B \-debug \f[I]n\f[]
+.B -debug \f[I]n\f[R]
 sets debugging level.
 Defaults to 0, meaning no debugging messages.
-This option has the same per\-plugin (and kernel) specializations as
-\f[B]\-verbose\f[].
-.RS
-.RE
+This option has the same per-plugin (and kernel) specializations as
+\f[B]-verbose\f[R].
 .TP
-.B \-quiet
+.B -quiet
 sets verbosity and debugging level to 0.
-.RS
-.RE
-.SS Options controlling Frama\-C's kernel
+.SS Options controlling Frama-C\[cq]s kernel
 .TP
-.B \-absolute\-valid\-range \f[I]min\-max\f[]
-considers that all numerical addresses in the range \f[I]min\-max\f[]
+.B -absolute-valid-range \f[I]min-max\f[R]
+considers that all numerical addresses in the range \f[I]min-max\f[R]
 are valid.
 Bounds are parsed as OCaml integer constants.
 By default, all numerical addresses are considered invalid.
-.RS
-.RE
 .TP
-.B \-add\-path \f[I]p1[,p2[\&...,pn]]\f[]
-adds directories \f[I]p1\f[] through \f[I]pn\f[] to the list of
+.B -add-path \f[I]p1[,p2[\&...,pn]]\f[R]
+adds directories \f[I]p1\f[R] through \f[I]pn\f[R] to the list of
 directories in which plugins are searched.
-.RS
-.RE
 .TP
-.B [\-no]\-aggressive\-merging
+.B [-no]-aggressive-merging
 merges function definitions modulo renaming.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-allow\-duplication
+.B [-no]-allow-duplication
 allows duplication of small blocks during normalization of tests and
 loops.
 Otherwise, normalization uses labels and gotos.
-Bigger blocks and blocks with non\-trivial control flow are never
+Bigger blocks and blocks with non-trivial control flow are never
 duplicated.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B [\-no]\-annot
+.B [-no]-annot
 reads ACSL annotations.
 This is the default.
-Annotations are pre\-processed by default.
-Use \-no\-pp\-annot if you don't want to expand macros in annotations.
-.RS
-.RE
+Annotations are pre-processed by default.
+Use -no-pp-annot if you don\[cq]t want to expand macros in annotations.
 .TP
-.B \-big\-ints\-hex \f[I]max\f[]
-integers larger than \f[I]max\f[] are displayed in hexadecimal (by
+.B -big-ints-hex \f[I]max\f[R]
+integers larger than \f[I]max\f[R] are displayed in hexadecimal (by
 default, all integers are displayed in decimal).
-.RS
-.RE
 .TP
-.B \-check
+.B -check
 performs integrity checks on the internal AST (for developers only).
-.RS
-.RE
 .TP
-.B [\-no]\-asm\-contracts
-generates contracts for assembly code written according to gcc's
+.B [-no]-asm-contracts
+generates contracts for assembly code written according to gcc\[cq]s
 extended syntax.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B [\-no]\-asm\-contracts\-auto\-validate
+.B [-no]-asm-contracts-auto-validate
 automatically marks contracts generated from asm as valid.
 Defaults to no.
-.RS
-.RE
 .TP
-.B \-c11
+.B -c11
 enables (partial) C11 compatibility, e.g.\ typedef redefinitions.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-collapse\-call\-cast
+.B [-no]-collapse-call-cast
 allows implicit cast between the value returned by a function and the
 lvalue it is assigned to.
 Otherwise, a temporary variable is used and the cast is made explicit.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B [\-no]\-constfold
+.B [-no]-constfold
 folds all syntactically constant expressions in the code before
 analyses.
 Defaults to no.
-.RS
-.RE
 .TP
-.B \-const\-readonly
+.B -const-readonly
 variables with const qualifier must be actually constant.
 Defaults to yes.
-The opposite option is \f[B]\-unsafe\-writable\f[].
-.RS
-.RE
+The opposite option is \f[B]-unsafe-writable\f[R].
 .TP
-.B [\-no]\-continue\-annot\-error
-when analyzing an annotation, the default behavior (the \f[B]\-no\f[]
+.B [-no]-continue-annot-error
+when analyzing an annotation, the default behavior (the \f[B]-no\f[R]
 version of this option) when a typechecking error occurs is to reject
 the source file as is the case for typechecking errors within the C
 code.
 With this option on, the typechecker will only output a warning and
-discard the annotation but type‐checking will continue (errors in C code
-are still fatal, though).
+discard the annotation but type\[hy]checking will continue (errors in C
+code are still fatal, though).
 .PD 0
 .P
 .PD
-\f[B]Deprecated\f[]: use \f[B]\-kernel\-warn\-key annot\-error\f[]
+\f[B]Deprecated\f[R]: use \f[B]-kernel-warn-key annot-error\f[R]
 instead.
-.RS
-.RE
 .TP
-.B \-cpp\-command \f[I]cmd\f[]
-uses \f[I]cmd\f[] as the command to pre\-process C files.
-Defaults to the \f[B]CPP\f[] environment variable or to
-.RS
-.RE
+.B -cpp-command \f[I]cmd\f[R]
+uses \f[I]cmd\f[R] as the command to pre-process C files.
+Defaults to the \f[B]CPP\f[R] environment variable or to
 .RS
 .PP
-gcc \-C \-E \-I.
+gcc -C -E -I.
 .RE
 .PP
 if it is not set.
 If unset, the command is built as follows:
 .RS
 .PP
-CPP \-o
+CPP -o
 .RE
 .PP
-\f[I]%1\f[] and \f[I]%2\f[] can be used into the \f[B]CPP\f[] string to
-mark the position of \f[I]\f[] and \f[I]\f[] respectively.
+\f[I]%1\f[R] and \f[I]%2\f[R] can be used into the \f[B]CPP\f[R] string
+to mark the position of \f[I]\f[R] and \f[I]\f[R] respectively.
 Note that this option is often better replaced by
-\f[B]\-cpp\-extra\-args\f[].
+\f[B]-cpp-extra-args\f[R].
 .TP
-.B \-cpp\-extra\-args \f[I]args\f[]
-gives additional arguments to the pre\-processor.
-Pre\-processing annotations is done in two separate pre\-processing
+.B -cpp-extra-args \f[I]args\f[R]
+gives additional arguments to the pre-processor.
+Pre-processing annotations is done in two separate pre-processing
 stages.
 The first one is a normal pass on the C code which retains macro
 definitions.
 These are then used in the second pass during which annotations are
-pre\-processed.
-\f[I]args\f[] are used only for the first pass, so that arguments that
+pre-processed.
+\f[I]args\f[R] are used only for the first pass, so that arguments that
 should not be used twice (such as additional include directives or macro
-definitions) must thus go there instead of \f[B]\-cpp\-command\f[].
-.RS
-.RE
+definitions) must thus go there instead of \f[B]-cpp-command\f[R].
 .TP
-.B \-cpp\-extra\-args\-per\-file \f[I]file1:args1,\&...,filen:argsn\f[]
-like \f[B]\-cpp\-extra\-args\f[], but the arguments only apply to the
+.B -cpp-extra-args-per-file \f[I]file1:args1,\&...,filen:argsn\f[R]
+like \f[B]-cpp-extra-args\f[R], but the arguments only apply to the
 specified files.
-.RS
-.RE
 .TP
-.B [\-no]\-cpp\-frama\-c\-compliant
-indicates that the chosen preprocessor complies to some Frama\-C
+.B [-no]-cpp-frama-c-compliant
+indicates that the chosen preprocessor complies to some Frama-C
 requirements, such as accepting the same set of options as GNU cpp, and
-accepting architecture\-specific options such as \-m32/\-m64.
+accepting architecture-specific options such as -m32/-m64.
 Default values depend on the installed preprocessor at configure time.
-See also \f[B]\-pp\-annot\f[].
-.RS
-.RE
+See also \f[B]-pp-annot\f[R].
 .TP
-.B [\-no]\-autoload\-plugins
+.B [-no]-autoload-plugins
 when on, load all the dynamic plugins found in the search path (see
-\f[B]\-print\-plugin\-path\f[] for more information on the default
-search path).
-Otherwise, only plugins requested by \f[B]\-load\-module\f[] will be
+\f[B]-print-plugin-path\f[R] for more information on the default search
+path).
+Otherwise, only plugins requested by \f[B]-load-module\f[R] will be
 loaded.
 Defaults to on.
-.RS
-.RE
 .TP
-.B \-enums \f[I]repr\f[]
+.B -enums \f[I]repr\f[R]
 choose the way the representation of enumerated types is determined.
-\f[B]frama\-c \-enums help\f[] gives the list of available options.
-Default is \f[B]gcc\-enums\f[].
-.RS
-.RE
+\f[B]frama-c -enums help\f[R] gives the list of available options.
+Default is \f[B]gcc-enums\f[R].
 .TP
-.B \-float\-digits \f[I]n\f[]
-when outputting floating\-point numbers, display \f[I]n\f[] digits.
+.B -float-digits \f[I]n\f[R]
+when outputting floating-point numbers, display \f[I]n\f[R] digits.
 Defaults to 12.
-.RS
-.RE
 .TP
-.B \-float\-flush\-to\-zero
+.B -float-flush-to-zero
 floating point operations flush to zero.
-.RS
-.RE
 .TP
-.B \-float\-hex
+.B -float-hex
 display floats as hexadecimal.
-.RS
-.RE
 .TP
-.B \-float\-normal
+.B -float-normal
 display floats with the standard OCaml routine.
-.RS
-.RE
 .TP
-.B \-float\-relative
-display float intervals as [ \f[I]lower_bound\f[]++\f[I]width\f[] ].
-.RS
-.RE
+.B -float-relative
+display float intervals as [ \f[I]lower_bound\f[R]++\f[I]width\f[R] ].
 .TP
-.B [\-no]\-frama\-c\-stdlib
-adds \f[B]\-I$FRAMAC_SHARE/libc\f[] to the options given to the cpp
+.B [-no]-frama-c-stdlib
+adds \f[B]-I$FRAMAC_SHARE/libc\f[R] to the options given to the cpp
 command.
-If \f[B]\-cpp\-frama\-c\-compliant\f[] is not false, also adds
-\f[B]\-nostdinc\f[] to prevent an inconsistent mix of system and
-Frama\-C header files.
+If \f[B]-cpp-frama-c-compliant\f[R] is not false, also adds
+\f[B]-nostdinc\f[R] to prevent an inconsistent mix of system and Frama-C
+header files.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B \-implicit\-function\-declaration \f[I]action\f[]
+.B -implicit-function-declaration \f[I]action\f[R]
 warns or aborts when a function is called before it has been declared.
-\f[I]action\f[] can be one of \f[B]ignore\f[], \f[B]warn\f[], or
-\f[B]error\f[].
-Defaults to \f[B]warn\f[].
+\f[I]action\f[R] can be one of \f[B]ignore\f[R], \f[B]warn\f[R], or
+\f[B]error\f[R].
+Defaults to \f[B]warn\f[R].
 .PD 0
 .P
 .PD
-\f[B]Deprecated\f[]: use \f[B]\-kernel\-warn\-key
-typing:implicit\-function\-declaration\f[] instead.
-.RS
-.RE
+\f[B]Deprecated\f[R]: use \f[B]-kernel-warn-key
+typing:implicit-function-declaration\f[R] instead.
 .TP
-.B \-initialized\-padding\-locals
+.B -initialized-padding-locals
 implicit initialization of locals sets padding bits to 0.
 If false, padding bits are left uninitialized.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B \-inline\-calls \f[I]f1,\&...,fn\f[]
-syntactically inlines calls to functions \f[I]f1,\&...,fn\f[].
-Use \f[B]\@inline\f[] to select all functions with attribute
-\f[I]inline\f[].
+.B -inline-calls \f[I]f1,\&...,fn\f[R]
+syntactically inlines calls to functions \f[I]f1,\&...,fn\f[R].
+Use \f[B]\[at]inline\f[R] to select all functions with attribute
+\f[I]inline\f[R].
 Recursive functions are inlined only at the first level.
 Calls via function pointers are not inlined.
-.RS
-.RE
 .TP
-.B \-journal\-disable
+.B -journal-disable
 do not output a journal of the current session.
-See \f[B]\-journal\-enable\f[].
-.RS
-.RE
+See \f[B]-journal-enable\f[R].
 .TP
-.B \-journal\-enable
+.B -journal-enable
 on by default, dumps a journal of all the actions performed during the
-current Frama\-C session in the form of an OCaml script that can be
-replayed with \f[B]\-load\-script\f[].
-The name of the script can be set with the \f[B]\-journal\-name\f[]
+current Frama-C session in the form of an OCaml script that can be
+replayed with \f[B]-load-script\f[R].
+The name of the script can be set with the \f[B]-journal-name\f[R]
 option.
-.RS
-.RE
 .TP
-.B \-journal\-name \f[I]name\f[]
-sets the name of the journal file (without the \f[I].ml\f[] extension).
-Defaults to \f[B]frama_c_journal\f[].
-.RS
-.RE
+.B -journal-name \f[I]name\f[R]
+sets the name of the journal file (without the \f[I].ml\f[R] extension).
+Defaults to \f[B]frama_c_journal\f[R].
 .TP
-.B \-json\-compilation\-database \f[I]path\f[]
-use \f[I]path\f[] as a JSON compilation database (see
+.B -json-compilation-database \f[I]path\f[R]
+use \f[I]path\f[R] as a JSON compilation database (see
 <https://clang.llvm.org/docs/JSONCompilationDatabase.html> for more
-information): each file preprocessed by Frama\-C will include
-corresponding \f[B]\-I\f[] and \f[B]\-D\f[] flags according to the
-specifications in \f[I]path\f[].
-If \f[I]path\f[] is a directory, use
-\f[B]<path>/compile_commands.json\f[].
+information): each file preprocessed by Frama-C will include
+corresponding \f[B]-I\f[R] and \f[B]-D\f[R] flags according to the
+specifications in \f[I]path\f[R].
+If \f[I]path\f[R] is a directory, use
+\f[B]<path>/compile_commands.json\f[R].
 Disabled by default.
-.RS
-.RE
 .TP
-.B [\-no]\-keep\-comments
-tries to preserve comments when pretty\-printing the source code.
+.B [-no]-keep-comments
+tries to preserve comments when pretty-printing the source code.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-keep\-switch
-when \f[B]\-simplify\-cfg\f[] is set, keeps switch statements.
+.B [-no]-keep-switch
+when \f[B]-simplify-cfg\f[R] is set, keeps switch statements.
 Defaults to no.
-.RS
-.RE
 .TP
-.B \-keep\-unused\-specified\-functions
-see \f[B]\-remove\-unused\-specified\-functions\f[].
-.RS
-.RE
+.B -keep-unused-specified-functions
+see \f[B]-remove-unused-specified-functions\f[R].
 .TP
-.B \-keep\-unused\-types
-see \f[B]\-remove\-unused\-types\f[].
-.RS
-.RE
+.B -keep-unused-types
+see \f[B]-remove-unused-types\f[R].
 .TP
-.B \-kernel\-log \f[I]kind:file\f[]
-copies log messages from the Frama\-C's kernel to file.
-\f[I]kind\f[] specifies which kinds of messages to be copied (e.g.
-\f[B]w\f[] for warnings, \f[B]e\f[] for errors, etc.).
-See \f[B]\-kernel\-help\f[] for more details.
-Can also be set on a per\-plugin basis, with option
-\-\f[I]<plugin>\f[]\-\f[B]log\f[].
-.RS
-.RE
+.B -kernel-log \f[I]kind:file\f[R]
+copies log messages from the Frama-C\[cq]s kernel to file.
+\f[I]kind\f[R] specifies which kinds of messages to be copied
+(e.g.\ \f[B]w\f[R] for warnings, \f[B]e\f[R] for errors, etc.).
+See \f[B]-kernel-help\f[R] for more details.
+Can also be set on a per-plugin basis, with option
+-\f[I]<plugin>\f[R]-\f[B]log\f[R].
 .TP
-.B \-kernel\-msg\-key \f[I]k1,\&...,kn\f[]
+.B -kernel-msg-key \f[I]k1,\&...,kn\f[R]
 controls the emission of messages based on categories.
-Use \f[B]\-kernel\-msg\-key help\f[] to get a list of available
-categories, and \f[B]\-kernel\-msg\-key=\[lq]*\[rq]\f[] to control all
+Use \f[B]-kernel-msg-key help\f[R] to get a list of available
+categories, and \f[B]-kernel-msg-key=\[lq]*\[rq]\f[R] to control all
 categories.
-To disable a category, add a \f[B]\-\f[] before its name; to enable a
-category, simply add its name, with an optional \f[B]+\f[] before it.
-For instance, \f[B]\-kernel\-msg\-key=\-k1,k2\f[] will disable messages
-from category \f[B]k1\f[] and enable those from category \f[B]k2\f[].
-Can also be set on a per\-plugin basis, with option
-\-\f[I]<plugin>\f[]\-\f[B]msg\-key\f[].
+To disable a category, add a \f[B]-\f[R] before its name; to enable a
+category, simply add its name, with an optional \f[B]+\f[R] before it.
+For instance, \f[B]-kernel-msg-key=-k1,k2\f[R] will disable messages
+from category \f[B]k1\f[R] and enable those from category \f[B]k2\f[R].
+Can also be set on a per-plugin basis, with option
+-\f[I]<plugin>\f[R]-\f[B]msg-key\f[R].
 Note that each plugin has its own set of categories.
-.RS
-.RE
 .TP
-.B \-kernel\-warn\-key \f[I]k1=a1,\&...,kn=an\f[]
+.B -kernel-warn-key \f[I]k1=a1,\&...,kn=an\f[R]
 controls the emission of warnings based on categories: for each warning
-category \f[I]k\f[], associate action \f[I]a\f[].
-Use \f[B]\-kernel\-warn\-key help\f[] to get a list of available warning
+category \f[I]k\f[R], associate action \f[I]a\f[R].
+Use \f[B]-kernel-warn-key help\f[R] to get a list of available warning
 categories and their currently associated actions.
-The following actions can be set per category: \f[B]active\f[] (warn),
-\f[B]feedback\f[], \f[B]error\f[], \f[B]abort\f[], \f[B]once\f[],
-\f[B]feedback\-once\f[], \f[B]err\-once\f[].
-Omitting the action is equivalent to setting it to \f[B]active\f[].
-Warning categories can also be set on a per\-plugin basis, with option
-\-\f[I]<plugin>\f[]\f[B]\-warn\-key\f[].
-.RS
-.RE
-.TP
-.B [\-no]\-lib\-entry
+The following actions can be set per category: \f[B]active\f[R] (warn),
+\f[B]feedback\f[R], \f[B]error\f[R], \f[B]abort\f[R], \f[B]once\f[R],
+\f[B]feedback-once\f[R], \f[B]err-once\f[R].
+Omitting the action is equivalent to setting it to \f[B]active\f[R].
+Warning categories can also be set on a per-plugin basis, with option
+-\f[I]<plugin>\f[R]\f[B]-warn-key\f[R].
+.TP
+.B [-no]-lib-entry
 indicates that the entry point is called during program execution.
 This implies in particular that global variables cannot be assumed to
 have their initial values.
-The default is \f[B]\-no\-lib\-entry\f[]: the entry point is also the
+The default is \f[B]-no-lib-entry\f[R]: the entry point is also the
 starting point of the program and globals have their initial value.
-.RS
-.RE
 .TP
-.B \-load \f[I]file\f[]
-loads the (previously saved) state contained in \f[I]file\f[].
-.RS
-.RE
+.B -load \f[I]file\f[R]
+loads the (previously saved) state contained in \f[I]file\f[R].
 .TP
-.B \-load\-module \f[I]SPEC\f[]
-dynamically load OCaml plug\-ins, modules and scripts.
-Each \f[I]SPEC\f[] can be an OCaml source or object file, with or
+.B -load-module \f[I]SPEC\f[R]
+dynamically load OCaml plug-ins, modules and scripts.
+Each \f[I]SPEC\f[R] can be an OCaml source or object file, with or
 without extension, or a Findlib package.
 Loading order is preserved and additional dependencies can be listed in
-*\f[B].depend\f[] files.
-.RS
-.RE
+*\f[B].depend\f[R] files.
 .TP
-.B \-load\-script \f[I]SPEC\f[]
-alias for option \f[B]\-load\-module\f[].
-.RS
-.RE
+.B -load-script \f[I]SPEC\f[R]
+alias for option \f[B]-load-module\f[R].
 .TP
-.B \-machdep \f[I]machine\f[]
-uses \f[I]machine\f[] as the current machine\-dependent configuration
+.B -machdep \f[I]machine\f[R]
+uses \f[I]machine\f[R] as the current machine-dependent configuration
 (size of the various integer types, endiandness, \&...).
 The list of currently supported machines is available through option
-\f[I]\-machdep help\f[].
-Default is \f[B]x86_32\f[].
-.RS
-.RE
+\f[I]-machdep help\f[R].
+Default is \f[B]x86_32\f[R].
 .TP
-.B \-main \f[I]f\f[]
-sets \f[I]f\f[] as the entry point of the analysis.
-Defaults to \f[B]main\f[].
+.B -main \f[I]f\f[R]
+sets \f[I]f\f[R] as the entry point of the analysis.
+Defaults to \f[B]main\f[R].
 By default, it is considered as the starting point of the program under
 analysis.
-Use \f[B]\-lib\-entry\f[] if \f[I]f\f[] is supposed to be called in the
+Use \f[B]-lib-entry\f[R] if \f[I]f\f[R] is supposed to be called in the
 middle of an execution.
-.RS
-.RE
 .TP
-.B \-obfuscate
+.B -obfuscate
 prints an obfuscated version of the code (where original identifiers are
 replaced by meaningless ones) and exits.
 The correspondence table between original and new symbols is kept at the
 beginning of the result.
-.RS
-.RE
 .TP
-.B \-ocode \f[I]file\f[]
-redirects pretty\-printed code to \f[I]file\f[] instead of standard
+.B -ocode \f[I]file\f[R]
+redirects pretty-printed code to \f[I]file\f[R] instead of standard
 output.
-.RS
-.RE
 .TP
-.B [\-no]\-orig\-name
+.B [-no]-orig-name
 During the normalization phase, some variables may get renamed when
-different variables with the same name can co\-exist (e.g.\ a global
+different variables with the same name can co-exist (e.g.\ a global
 variable and a formal parameter).
 When this option is on, a message is printed each time this occurs.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-pp\-annot
-pre\-processes annotations.
+.B [-no]-pp-annot
+pre-processes annotations.
 This is currently only possible when using gcc (or GNU cpp)
-pre\-processor.
-The default is to pre\-process annotations when the default
-pre\-processor is identified as GNU or GNU\-like.
-See also \f[B]\-cpp\-frama\-c\-compliant\f[].
-.RS
-.RE
+pre-processor.
+The default is to pre-process annotations when the default pre-processor
+is identified as GNU or GNU-like.
+See also \f[B]-cpp-frama-c-compliant\f[R].
 .TP
-.B [\-no]\-print
-pretty\-prints the source code as normalized by CIL.
+.B [-no]-print
+pretty-prints the source code as normalized by CIL.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-print\-libc
-expands \f[B]#include\f[] directives in the pretty\-printed CIL code for
-files in the Frama\-C standard library.
+.B -print-cpp-commands
+outputs the preprocessing commands for all input files.
+.TP
+.B [-no]-print-libc
+expands \f[B]#include\f[R] directives in the pretty-printed CIL code for
+files in the Frama-C standard library.
 Defaults to no.
-.RS
-.RE
 .TP
-.B \-print\-libpath
-outputs the directory where the Frama\-C kernel library is installed.
-.RS
-.RE
+.B -print-libpath
+outputs the directory where the Frama-C kernel library is installed.
 .TP
-.B \-print\-path
-alias of \f[B]\-print\-share\-path\f[].
-.RS
-.RE
+.B -print-path
+alias of \f[B]-print-share-path\f[R].
 .TP
-.B \-print\-plugin\-path
-outputs the directory where Frama\-C searches its plugins (can be
-overridden by the \f[B]FRAMAC_PLUGIN\f[] variable and the
-\f[B]\-add\-path\f[] option).
-.RS
-.RE
+.B -print-plugin-path
+outputs the directory where Frama-C searches its plugins (can be
+overridden by the \f[B]FRAMAC_PLUGIN\f[R] variable and the
+\f[B]-add-path\f[R] option).
 .TP
-.B \-print\-share\-path
-outputs the directory where Frama\-C stores its data (can be overridden
-by the \f[B]FRAMAC_SHARE\f[] variable).
-.RS
-.RE
+.B -print-share-path
+outputs the directory where Frama-C stores its data (can be overridden
+by the \f[B]FRAMAC_SHARE\f[R] variable).
 .TP
-.B [\-no]\-remove\-exn
+.B [-no]-remove-exn
 transforms throw and try/catch statements into normal C functions.
 Defaults to no, unless the input source language has an exception
 mechanism.
-.RS
-.RE
 .TP
-.B \-remove\-inlined \f[I]f1,\&...,fn\f[]
-removes inlined functions \f[I]f1,\&...,fn\f[] from the AST, which must
-have been given to \f[B]\-inline\-calls\f[].
+.B -remove-inlined \f[I]f1,\&...,fn\f[R]
+removes inlined functions \f[I]f1,\&...,fn\f[R] from the AST, which must
+have been given to \f[B]-inline-calls\f[R].
 Note: this option does not check if the given functions were fully
 inlined.
-.RS
-.RE
 .TP
-.B \-remove\-projects \f[I]p1,\&...,pn\f[]
-removes the given projects \f[I]p1,\&...,pn\f[].
-\f[B]\@all_but_current\f[] removes all projects but the current one.
-.RS
-.RE
+.B -remove-projects \f[I]p1,\&...,pn\f[R]
+removes the given projects \f[I]p1,\&...,pn\f[R].
+\f[B]\[at]all_but_current\f[R] removes all projects but the current one.
 .TP
-.B \-remove\-unused\-specified\-functions
+.B -remove-unused-specified-functions
 keeps function prototypes that have an ACSL specification but are not
 used in the code.
 This is the default.
-Functions having the attribute \f[B]FRAMAC_BUILTIN\f[] are always kept.
-.RS
-.RE
+Functions having the attribute \f[B]FRAMAC_BUILTIN\f[R] are always kept.
 .TP
-.B \-remove\-unused\-types
+.B -remove-unused-types
 remove types and struct/union/enum declarations that are not referenced
 anywhere else in the code.
 This is the default.
-Use \f[B]\-keep\-unused\-types\f[] to keep these definitions.
-.RS
-.RE
+Use \f[B]-keep-unused-types\f[R] to keep these definitions.
 .TP
-.B \-safe\-arrays
+.B -safe-arrays
 for multidimensional arrays or arrays that are fields inside structs,
 assumes that all accesses must be in bound (set by default).
-The opposite option is \f[B]\-unsafe\-arrays\f[].
-.RS
-.RE
+The opposite option is \f[B]-unsafe-arrays\f[R].
 .TP
-.B \-save \f[I]file\f[]
-saves Frama\-C's state into \f[I]file\f[] after analyses have taken
+.B -save \f[I]file\f[R]
+saves Frama-C\[cq]s state into \f[I]file\f[R] after analyses have taken
 place.
-.RS
-.RE
 .TP
-.B \-session \f[I]s\f[]
-sets \f[I]s\f[] as the directory in which session files are searched.
-.RS
-.RE
+.B -session \f[I]s\f[R]
+sets \f[I]s\f[R] as the directory in which session files are searched.
 .TP
-.B [\-no]\-set\-project\-as\-default
+.B [-no]-set-project-as-default
 the current project becomes the default one (and so future
-\f[B]\-then\f[] sequences are applied on it).
+\f[B]-then\f[R] sequences are applied on it).
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-simplify\-cfg
-removes \f[B]break\f[], \f[B]continue\f[] and \f[B]switch\f[] statements
-before analyses.
+.B [-no]-simplify-cfg
+removes \f[B]break\f[R], \f[B]continue\f[R] and \f[B]switch\f[R]
+statements before analyses.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-simplify\-trivial\-loops
-simplifies trivial loops such as \f[B]do \&... while (0)\f[] loops.
+.B [-no]-simplify-trivial-loops
+simplifies trivial loops such as \f[B]do \&... while (0)\f[R] loops.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B \-then
-allows one to compose analyses: a first run of Frama\-C will occur with
-the options before \f[B]\-then\f[] and a second run will be done with
-the options after \f[B]\-then\f[] on the current project from the first
+.B -then
+allows one to compose analyses: a first run of Frama-C will occur with
+the options before \f[B]-then\f[R] and a second run will be done with
+the options after \f[B]-then\f[R] on the current project from the first
 run.
-.RS
-.RE
 .TP
-.B \-then\-last
-like \f[B]\-then\f[], but the second group of actions is executed on the
+.B -then-last
+like \f[B]-then\f[R], but the second group of actions is executed on the
 last project created by a program transformer.
-.RS
-.RE
 .TP
-.B \-then\-on \f[I]prj\f[]
-similar to \f[B]\-then\f[] except that the second run is performed in
-project \f[I]prj\f[].
-If no such project exists, Frama\-C exits with an error.
-.RS
-.RE
+.B -then-on \f[I]prj\f[R]
+similar to \f[B]-then\f[R] except that the second run is performed in
+project \f[I]prj\f[R].
+If no such project exists, Frama-C exits with an error.
 .TP
-.B \-then\-replace
-like \f[B]\-then\-last\f[], but also removes the previous current
+.B -then-replace
+like \f[B]-then-last\f[R], but also removes the previous current
 project.
-.RS
-.RE
 .TP
-.B \-time \f[I]file\f[]
-appends user time and date in the given file when Frama\-C exits.
-.RS
-.RE
+.B -time \f[I]file\f[R]
+appends user time and date in the given file when Frama-C exits.
 .TP
-.B \-typecheck
+.B -typecheck
 forces typechecking of the source files.
 This option is only relevant if no further analysis is requested (as
 typechecking will implicitly occur before the analysis is launched).
-.RS
-.RE
 .TP
-.B \-ulevel \f[I]n\f[]
-syntactically unroll loops \f[I]n\f[] times before the analysis.
+.B -ulevel \f[I]n\f[R]
+syntactically unroll loops \f[I]n\f[R] times before the analysis.
 This can be quite costly and some plugins (e.g.\ Eva) provide more
 efficient ways to perform the same thing.
 See their respective manuals for more information.
-This can also be activated on a per\-loop basis via the \f[B]loop pragma
-unroll \f[] directive.
-A negative value for \f[I]n\f[] will inhibit such pragmas.
-.RS
-.RE
+This can also be activated on a per-loop basis via the \f[B]loop pragma
+unroll \f[R] directive.
+A negative value for \f[I]n\f[R] will inhibit such pragmas.
 .TP
-.B [\-no]\-ulevel\-force
-ignores \f[B]UNROLL\f[] loop pragmas disabling unrolling.
-.RS
-.RE
+.B [-no]-ulevel-force
+ignores \f[B]UNROLL\f[R] loop pragmas disabling unrolling.
 .PP
-[\-no]\-unicode outputs ACSL formulas with UTF\-8 characters.
+[-no]-unicode outputs ACSL formulas with UTF-8 characters.
 This is the default.
-When given the \f[B]\-no\-unicode\f[] option, Frama\-C will use the
-ASCII version instead.
+When given the \f[B]-no-unicode\f[R] option, Frama-C will use the ASCII
+version instead.
 See the ACSL manual for the correspondence.
 .TP
-.B \-unsafe\-arrays
-see \f[B]\-safe\-arrays\f[].
-.RS
-.RE
+.B -unsafe-arrays
+see \f[B]-safe-arrays\f[R].
 .TP
-.B [\-no]\-unspecified\-access
+.B [-no]-unspecified-access
 checks that read/write accesses occurring in an unspecified order
-(according to the C standard's notion of sequence points) are performed
-on separate locations.
-With \f[B]\-no\-unspecified\-access\f[], assumes that it is always the
+(according to the C standard\[cq]s notion of sequence points) are
+performed on separate locations.
+With \f[B]-no-unspecified-access\f[R], assumes that it is always the
 case (this is the default).
-.RS
-.RE
 .TP
-.B \-version
-outputs the version string of Frama\-C.
-.RS
-.RE
+.B -version
+outputs the version string of Frama-C.
 .TP
-.B \-warn\-decimal\-float \f[I]freq\f[]
-warns when a floating\-point constant cannot be exactly represented
+.B -warn-decimal-float \f[I]freq\f[R]
+warns when a floating-point constant cannot be exactly represented
 (e.g.\ 0.1).
-\f[I]freq\f[] can be one of \f[B]none\f[], \f[B]once\f[], or
-\f[B]all\f[].
+\f[I]freq\f[R] can be one of \f[B]none\f[R], \f[B]once\f[R], or
+\f[B]all\f[R].
 .PD 0
 .P
 .PD
-\f[B]Deprecated\f[]: use \f[B]\-kernel\-warn\-key
-parser:decimal\-float=once\f[] (and variants) instead.
-.RS
-.RE
+\f[B]Deprecated\f[R]: use \f[B]-kernel-warn-key
+parser:decimal-float=once\f[R] (and variants) instead.
 .TP
-.B [\-no]\-warn\-invalid\-pointer
+.B [-no]-warn-invalid-pointer
 generate alarms for invalid pointer arithmetic.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-left\-shift\-negative
+.B [-no]-warn-left-shift-negative
 generate alarms for signed left shifts on negative values.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-right\-shift\-negative
+.B [-no]-warn-right-shift-negative
 generate alarms for signed right shifts on negative values.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-pointer\-downcast
+.B [-no]-warn-pointer-downcast
 generates alarms when the downcast of a pointer may exceed the
 destination range.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-signed\-downcast
+.B [-no]-warn-signed-downcast
 generates alarms when signed downcasts may exceed the destination range.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-signed\-overflow
+.B [-no]-warn-signed-overflow
 generates alarms for signed operations that overflow.
 Defaults to yes.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-unsigned\-downcast
+.B [-no]-warn-unsigned-downcast
 generates alarms when unsigned downcasts may exceed the destination
 range.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-unsigned\-overflow
+.B [-no]-warn-unsigned-overflow
 generates alarms for unsigned operations that overflow.
 Defaults to no.
-.RS
-.RE
 .TP
-.B [\-no]\-warn\-invalid\-bool
+.B [-no]-warn-invalid-bool
 generates alarms for reads of trap representations of _Bool lvalues.
 Defaults to yes.
-.RS
-.RE
-.SS Plugin\-specific options
+.SS Plugin-specific options
 .PP
 For each plugin, the command
 .RS
 .PP
-frama\-c \-plugin\-help
+frama-c -plugin-help
 .RE
 .PP
 will give the list of options that are specific to the plugin.
@@ -810,64 +625,45 @@ will give the list of options that are specific to the plugin.
 .TP
 .B 0
 Successful execution
-.RS
-.RE
 .TP
 .B 1
 Invalid user input
-.RS
-.RE
 .TP
 .B 2
 User interruption (kill or equivalent)
-.RS
-.RE
 .TP
 .B 3
 Unimplemented feature
-.RS
-.RE
 .TP
 .B 4 5 6
 Internal error
-.RS
-.RE
 .TP
 .B 125
 Unknown error
-.RS
-.RE
 .PP
 Exit statuses greater than 2 can be considered as a bug (or a feature
-request for the case of exit status 3) and may be reported on Frama\-C's
-BTS (see below).
+request for the case of exit status 3) and may be reported on
+Frama-C\[cq]s BTS (see below).
 .SH ENVIRONMENT VARIABLES
 .PP
-It is possible to control the places where Frama\-C looks for its files
+It is possible to control the places where Frama-C looks for its files
 through the following variables.
 .TP
 .B FRAMAC_LIB
-The directory where kernel's compiled interfaces are installed.
-.RS
-.RE
+The directory where kernel\[cq]s compiled interfaces are installed.
 .TP
 .B FRAMAC_PLUGIN
-The directory where Frama\-C can find standard plugins.
-If you wish to have plugins in several places, use \f[B]\-add\-path\f[]
+The directory where Frama-C can find standard plugins.
+If you wish to have plugins in several places, use \f[B]-add-path\f[R]
 instead.
-.RS
-.RE
 .TP
 .B FRAMAC_SHARE
-The directory where Frama\-C data (e.g.\ its version of the standard
+The directory where Frama-C data (e.g.\ its version of the standard
 library) is installed.
-.RS
-.RE
 .SH SEE ALSO
 .PP
-Frama\-C user manual:
-http://frama\-c.com/download/frama\-c\-user\-manual.pdf
+Frama-C user manual: http://frama-c.com/download/frama-c-user-manual.pdf
 .PP
-Frama\-C homepage: http://frama\-c.com
+Frama-C homepage: http://frama-c.com
 .PP
-Frama\-C BTS: http://bts.frama\-c.com
+Frama-C BTS: http://bts.frama-c.com
diff --git a/man/frama-c.1.header b/man/frama-c.1.header
index 2bc62cfc5176c9274f4dad74c7c7d4894dd84a7c..0f53666d7fe149a1b104dd8bc8fccf774f4b9726 100644
--- a/man/frama-c.1.header
+++ b/man/frama-c.1.header
@@ -25,4 +25,4 @@
 .\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
 .\" and run `make man/frama-c.1`.
 
-.TH FRAMA-C 1 2020-05-26
+.TH FRAMA-C 1 2020-09-01
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 396cf3138d6b15f78d2354d2b41a5767104c8bc8..35111cfa6e87e5064a33e9a72e6661004692de18 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -333,6 +333,9 @@ See also **-cpp-frama-c-compliant**.
 [-no]-print
 : pretty-prints the source code as normalized by CIL. Defaults to no.
 
+-print-cpp-commands
+: outputs the preprocessing commands for all input files.
+
 [-no]-print-libc
 : expands **#include** directives in the pretty-printed CIL code for files in
 the Frama-C standard library. Defaults to no.