Added documentation for the e-acsl wrapper script

src/plugins/e-acsl/doc/userman/macros.tex

@@ -7,6 +7,7 @@
 \newcommand{\framac}{\textsc{Frama-C}\xspace}
 \newcommand{\acsl}{\textsc{ACSL}\xspace}
 \newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
+\newcommand{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
 \newcommand{\rte}{\textsc{RTE}\xspace}
 \newcommand{\C}{\textsc{C}\xspace}
 \newcommand{\jml}{\textsc{JML}\xspace}

src/plugins/e-acsl/doc/userman/provides.tex

@@ -773,3 +773,183 @@ typing & minimization of the instrumentation for integers
 \hline
 \end{tabular}
 \end{center}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{\eacslgcc:  Wrapper Script for Easy Instrumentation}
+\label{sec:eacsl-gcc}
+
+Due to numerous instrumentation and compile-time options generating monitored
+executables using the \eacsl plugin can be tedious. To simplify this task we
+developed \eacslgcc\ -- a convenience wrapper around \framac and \gcc allowing
+to instrument programs with \eacsl and compile the instrumented code using a
+single command and a very few parameters.
+
+In this section we describe \eacslgcc and provide several examples of its use.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Basic Use}
+
+\eacslgcc instruments C files provided at input using the \eacsl plugin, and
+optionally compiles the generated code and the original sources using the \gcc
+compiler.
+
+The default behaviour of \eacslgcc is to instrument an annotated C program
+with runtime assertions via a run of \framac.
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -ogen.c foo.c
+\end{shell}
+
+The above command instruments \texttt{foo.c} with runtime assertions and
+outputs the generated code to \texttt{gen.c}. Unless the name of the output
+file is specified via the \texttt{-o} option (i.e., \texttt{-ogen.c} in the
+above example), the generated code is placed to a file named
+\texttt{a.out.frama.c}.
+
+Compilation of the original and the instrumented sources
+is enabled using the \texttt{-c} option.  For instance, the command
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -ogen.c foo.c
+\end{shell}
+
+instruments the code in \texttt{foo.c}, outputs it to \texttt{gen.c} and
+produces 2 executables: \texttt{a.out} and \texttt{a.out.e-acsl}, where
+\texttt{a.out} is an executable compiled from
+\texttt{foo.c}, while \texttt{a.out.e-acsl} is an executable compiled from
+\texttt{gen.c} generated by \eacsl.
+
+Named executables can be created using the \texttt{-O} option.  This is such
+that a value supplied to the \texttt{-O} option is used to name the executable
+generated from the original program and the executable generateted from the
+\eacsl-instrumented code is suffixed \texttt{.e-acsl}.
+
+For example, command
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -ogen.c -Ogen foo.c
+\end{shell}
+will name the executables generated from \texttt{foo.c} and \texttt{gen.c}:
+\texttt{gen} and \texttt{gen.e-acsl} respectively.
+
+The \eacslgcc \texttt{-C} option allows to skip instrumentation step and
+compile a given program as if it were already instrumented by the \eacsl
+plugin.  This option is useful if one makes some changes to an already
+instrumented source file by hand and only wants to recompile it.
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -C -Ogen gen.c
+\end{shell}
+
+In the above example the run of \eacslgcc produces a single executable named
+\texttt{gen.e-acsl}. This is because \texttt{gen.c} is considered to be
+instrumented code and thus no original program is provided.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Documentation}
+
+A list of \eacslgcc options can be retrieved using the following command:
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -h
+ Usage: e-acsl-gcc.sh [options] files
+ Options:
+   -h         show this help page
+   -c         compile instrumented code
+   -l         pass additional options to the linker
+   -e         pass additional options to the pre-preprocessor
+   -E         pass additional arguments to the Frama-C pre-processor
+   -p         output the generated code with rich formatting to STDOUT
+   -o <file>  output the generated code to <file> [a.out.frama.c]
+   -O <file>  output the generated executables to <file> [a.out, a.out.e-acsl]
+   -M         maximise memory-related instrumentation
+   -g         always use GMP integers instead of C integral types
+   -q         suppress any output except for errors and warnings
+   -s <file>  redirect all output to <file>
+   -P         compile executatle without debug features
+   -I <file>  specify Frama-C executable [frama-c]
+   -G <file>  specify GCC executable [gcc]
+\end{shell}
+
+Note that the \texttt{-h} option lists only the most basic options.
+For full up-to-date documentation of \eacslgcc see its man page:
+
+\begin{shell}
+    \$ man e-acsl-gcc.sh
+\end{shell}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Customising \framac and \gcc Invocations}
+
+Runs of \framac and \gcc issued by \eacslgcc can be customized by
+using additional flags passed the tools' invocations.
+
+Additional \framac flags can be passed using the \texttt{-F} option, while
+\texttt{-l} and \texttt{-e} options allow for passing additional pre-processor
+and linker flags during \gcc invocations.
+For example, command
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
+\end{shell}
+
+will yield an instrumented program \texttt{a.out.frama.c} where ACSL formulas
+are output using the UTF-8 character set. Further, during the compilation of
+\texttt{a.out.frama.c} \gcc will add directories \texttt{/bar} and
+\texttt{/baz} to the list of directories to be searched for header files.
+
+It is worth mentioning that \eacslgcc implements several convenience flags for
+setting some of the \framac options. For instance, \texttt{-E} can be used to
+pass additional arguments to the \framac pre-processor and \texttt{-M} maximizes
+memory-related instrumentation.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Verbosity Levels and Output Redirection}
+
+By default \eacslgcc prints the executed \framac and \gcc commands and pipes
+their output to the terminal. The verbosity of \framac output can be changed
+using \texttt{-v} and \texttt{-d} options used to pass values to
+\texttt{-verbose} and \texttt{-debug} flags of \framac respectively.  For
+instance, to increase the verbosity of plugins but suppress the verbosity of
+the \framac kernel while instrumenting \texttt{foo.c} one can use the following
+command:
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
+\end{shell}
+
+Verbosity of the output of \eacslgcc script can also be reduced using the
+\texttt{-q} option that suppresses any output except errors or warnings issued
+by \gcc, \framac or \eacslgcc itself.
+
+The output of \eacslgcc can also be redirected to a specified log file
+using the \texttt{-s} option.  For example, the following command will redirect
+all output during instrumentation and compillation of \texttt{foo.c} to the
+\texttt{/tmp/log} file.
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
+\end{shell}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Executables}
+
+By default \eacslgcc uses the first \texttt{frama-c} executable found in a
+system's path to instrument input programs. The name of the \framac executable
+can be changed using the \texttt{-I} option. For instance, to instrument a file
+named \texttt{foo.c} using the \texttt{/usr/local/bin/frama-c.byte} executable
+one can issue the following command:
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c.byte foo.c
+\end{shell}
+
+The name of a \gcc executable can be similarly changed using the \texttt{-G}
+option.
\ No newline at end of file