diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex index 39dbfe2c72d2d6b9dbe73b92d5b64295a87251b0..901130870c3b664df60a2d85b7b089d4078f9d38 100644 --- a/doc/userman/user-analysis-scripts.tex +++ b/doc/userman/user-analysis-scripts.tex @@ -76,8 +76,9 @@ 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: +The command \texttt{frama-c-script make-template} can be used to generate the +Makefile from a template. The user must fill in the following information, +required for running an \Value analysis: \begin{description} \item[machdep]: architectural information about system where the code will run: @@ -93,8 +94,8 @@ of information are necessary: 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 +A project without this information is incomplete; an alternative +workflow is then necessary. The next section presents some possibilities to retrieve such information. \subsection{Possible Workflows in the Absence of Build Information}