[Doc] User manual: minor changes in the documentation of analysis-scripts.

doc/userman/user-analysis-scripts.tex

@@ -37,9 +37,9 @@ themselves are installed in Frama-C's \texttt{share} directory, underneath
 
 \subsection{General Framework}
 
-{\em Note}: the analysis scripts are intended for usage in a wide variety
-of scenarios, with different plug-ins. However, currently the scripts focus
-on usage with the \Value plug-in.
+{\em Note}: while the analysis scripts are intended for usage in a wide variety
+of scenarios with different plug-ins, they currently focus
+on analyses with the \Value plug-in only.
 
 The main usage mode of \texttt{analysis-scripts} consists in creating a
 Makefile dedicated to the analysis of a C code base.
@@ -49,10 +49,10 @@ This Makefile has three main purposes:
 \begin{enumerate}
 \item To separate the main analysis steps, saving partial results and logging
   output messages;
-\item To avoid recomputing unnecessary data (e.g. the AST) when modifying
+\item To avoid recomputing unnecessary data when modifying
   analysis-specific options;
 \item To document analysis options and improve replayability, e.g. when
-  iteratively fine-tuning results.
+  iteratively fine-tuning the analysis in order to improve its results.
 \end{enumerate}
 
 The intended usage is as follows:
@@ -73,7 +73,7 @@ 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{Alternative Workflows in the Absence of Build Information}
+\subsection{Possible Workflows in the Absence of Build Information}
 \label{alternative-workflows}
 
 It is sometimes the case that the \FramaC user is not the developer of the
@@ -127,7 +127,7 @@ in section~\ref{sec:preprocessing}). This leads to a different workflow:
 
 \begin{enumerate}
 \item Run CMake with the flag \texttt{-DCMAKE\_EXPORT\_COMPILE\_COMMANDS=1},
-  or install Build EAR (\url{https://github.com/rizsotto/Bear} and run
+  or install Build EAR (\url{https://github.com/rizsotto/Bear}) and run
   \texttt{bear make <targets>} instead of \texttt{make <targets>}. This will
   create a \texttt{compile\_commands.json} file.
 \item Run \texttt{frama-c-script list-files}. A list of the compiled files,
@@ -248,7 +248,7 @@ The most useful commands are described below.
 Run \texttt{frama-c-script help} for more details and optional arguments.
 
 \begin{description}
-\item[make-template]: used to create the initial Makefile, based on a template.
+\item[make-template]: creates the initial Makefile, based on a template.
   This command creates a file named \texttt{GNUmakefile} with some hardcoded
   sections, some filled in interactively by the user, and comments indicating
   which parts may need change. Once created, it enables the general workflow
@@ -270,7 +270,7 @@ Run \texttt{frama-c-script help} for more details and optional arguments.
 Other commands, only useful in a few cases, are described below.
 
 \begin{description}
-\item[configure <machdep>]: used to run a \texttt{configure}
+\item[configure <machdep>]: runs a \texttt{configure}
   script (based on Autoconf) with some settings to emulate a more portable
   system, removing optional code features that could prevent \FramaC from
   parsing the sources. Currently still depends partially on the host system,
@@ -280,7 +280,7 @@ Other commands, only useful in a few cases, are described below.
   by the Makefile generated by \texttt{make-template}.
 \item[flamegraph]: opens a {\em flamegraph}\footnote{%
   See \url{https://github.com/brendangregg/FlameGraph} for details about
-  flamegraphs.} to help visualize which functions take most of the time
+  flamegraphs.} to visualize which functions take most of the time
   during analysis with \Value.
 \item[summary]: for monitoring the progression of multiple analyses defined
   in a single Makefile. Presents a summary of the analyses when done. Mostly
@@ -305,7 +305,7 @@ different. It is available at\\
 
 \begin{description}
 \item[creduce.sh]: A script to help running the C-Reduce\footnote{%
-  See https://embed.cs.utah.edu/creduce for more details.} tool to minify
+  See \url{https://embed.cs.utah.edu/creduce} for more details.} tool to minify
   C programs causing crashes in \FramaC; useful e.g. when submitting a bug
   report to \FramaC, without needing to submit potentially confidential data.
   The script contains extensive comments about its usage. It is also
@@ -327,8 +327,8 @@ Due to the variety of test cases, OSCS provide practical usage
 examples of the \texttt{GNUmakefile} described in this chapter.
 They are periodically synchronized w.r.t. the public \FramaC repository
 (daily snapshots), so they may contain features not yet available in the
-major \FramaC releases. A few may also contain legacy features which
-are no longer used; but overall, they provide useful examples and allow
+major \FramaC releases. A few case studies may also contain legacy features
+which are no longer used; but overall, they provide useful examples and allow
 the user to tweak analysis parameters to test their effects.
 
 \section{Technical Notes}