From d962647b4ebe4177ee8abcf02b32080364d9ded7 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 5 Jun 2020 16:10:42 +0200
Subject: [PATCH] [Doc] add section about required build information
---
doc/userman/user-analysis-scripts.tex | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index e542a564cd6..ba6e590c56b 100644
--- a/doc/userman/user-analysis-scripts.tex
+++ b/doc/userman/user-analysis-scripts.tex
@@ -73,6 +73,30 @@ re-running \texttt{make} should be enough to obtain a new result.
Section~\ref{sec:using-generated-makefile} details usage of the Makefile
and presents an illustrative diagram.
+\subsection{Necessary Build Information}
+\label{sec:necessary-build-information}
+
+For an analysis with \FramaC, besides the source code, the following pieces
+of information are necessary:
+
+\begin{description}
+\item[machdep]: architectural information about system where the code will run:
+ integer type sizes, compiler, OS, etc. See section~\ref{sec:normalize} for
+ more details.
+\item[preprocessing flags]: options given to the C preprocessor, mainly
+ macros (\texttt{-D}) and include directories (\texttt{-I}).
+\item[list of sources]: the actual list of source files that make a logical
+ unit (e.g. a test case or a whole program), without duplicate function
+ definitions.
+\item[main function]: the function where the analysis will start; it is often
+ \texttt{main}, but not always. ({\em Note: \FramaC itself thes not require
+ a \texttt{main} function, but plug-ins such as \texttt{Eva} do}.)
+\end{description}
+
+A project without such information is incomplete. In such cases, an alternative
+workflow is necessary. The next section presents some possibilities to
+retrieve such information.
+
\subsection{Possible Workflows in the Absence of Build Information}
\label{alternative-workflows}
--
GitLab