From b6f51172683fb11ed31c24e1d3f0fdbddb444428 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 5 Jun 2020 13:58:20 +0200
Subject: [PATCH] [Doc] User manual: minor changes in the documentation of
analysis-scripts.
---
doc/userman/user-analysis-scripts.tex | 26 +++++++++++++-------------
1 file changed, 13 insertions(+), 13 deletions(-)
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index 72dd39385cd..e542a564cd6 100644
--- a/doc/userman/user-analysis-scripts.tex
+++ b/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}
--
GitLab