From af90bdaafebdaeda334cbb61a63d2a2e7fc2b380 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 5 Apr 2024 17:46:08 +0200
Subject: [PATCH] [userman] document undefinition of builtin macros in -machdep
---
doc/userman/user-analysis-scripts.tex | 2 +-
doc/userman/user-changes.tex | 2 ++
doc/userman/user-sources.tex | 9 ++++++++-
3 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index 45181196605..e3d1ee5fab5 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 51604605640..078f492468a 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 a30490e6448..8409cc2d684 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
--
GitLab