From 5fca2cd750a647fa7e62659b89643c2663fe8ea0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 23 Mar 2023 14:03:36 +0100
Subject: [PATCH] [userman] document new machdep usage
---
doc/userman/user-changes.tex | 1 +
doc/userman/user-sources.tex | 7 +++++--
2 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 2c9097889fe..c2a61d60d94 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,7 @@ release. First we list changes of the last release.
\section*{Frama-C+dev}
\begin{itemize}
+\item \textbf{Normalizing the Source Code:} new usage of \texttt{-machdep}
\item \textbf{Normalizing the Source Code:} deprecated option \texttt{-c11}
(enabled by default).
\end{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index b748156775d..b2256fa875b 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -296,8 +296,11 @@ The list of supported platforms can be obtained by typing:
\$ frama-c -machdep help
\end{frama-c-commands}
-The process for adding a new platform is described in the Plug-in
-Development Guide~\cite{plugin-dev-guide}.
+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.
\item \optiondef{-}{simplify-cfg} allows \FramaC to remove break, continue and
switch statements. This option is automatically set by some plug-ins that
--
GitLab