diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index 451811966051eb65be4325ff23b9b1ce532a021a..e3d1ee5fab5002537d0747de3adebee6d99bed83 100644
--- a/doc/userman/user-analysis-scripts.tex
+++ b/doc/userman/user-analysis-scripts.tex
@@ -162,7 +162,7 @@ such as when multiple test files define a \texttt{main} function.
 \end{itemize}
 
 \subsection{Using a JSON Compilation Database (JCDB)}
-
+\label{sec:using-json-comp}
 Independently of the chosen workflow, some partial information can be retrieved
 when CMake or Makefile scripts are available for compiling the sources.
 They allow the production of a JSON Compilation Database
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 51604605640e95544f498f6a89a7a37dd2944533..078f492468acd70eaa495d8f1ea50e61e0aa70ad 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,8 @@ release. First we list changes of the last release.
 
 \section*{Frama-C+dev}
 \begin{itemize}
+\item \textbf{Normalizing the Source Code:} document the possibility of
+  undefining builtins macros from the chosen \texttt{-machdep}
 \item \textbf{Preparing the Sources:} add subsection on standard library about
   portability considerations.
 \end{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index a30490e6448385e21fea8046bf6589a8cb0e8479..8409cc2d684da99d29e91c22cb70b5f0bb43eac7 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -287,7 +287,14 @@ Apart from these default platforms, it is possible to give as argument
 to \texttt{-machdep} option the path of a YAML file containing the information
 needed by \FramaC. The Plug-in Development Guide~\cite{plugin-dev-guide} describes
 this format in more detail, as well as the use of the \texttt{make\_machdep.py}
-script to automatically generate it.
+script to automatically generate it. The YAML schema contains a list of builtins
+macros with their values. However, any such \texttt{MACRO} can be undefined by passing
+\texttt{-UMACRO} in the preprocessor arguments
+(using \texttt{-cpp-extra-args} or its per-file counterpart as in Sect.~\ref{sec:preprocessing},
+or a compilation database as in Sect.~\ref{sec:using-json-comp}). In addition,
+since compilers tend to define builtin macros with a varying number of
+underscores as prefix and suffix, \texttt{-UMACRO} will also undefine
+\texttt{\_MACRO}, \texttt{\_\_MACRO}, \texttt{\_\_MACRO\_\_}, etc.
 
 \item \optiondef{-}{simplify-cfg} allows \FramaC to remove break, continue and
   switch statements. This option is automatically set by some plug-ins that