From 21a760b2b3fff835ea64058ab74b875485a8d34a Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 10 Feb 2016 18:51:35 +0100
Subject: [PATCH] Section describing e-acsl-gcc.sh wrapper script added as a
separate section of the user manual
Minor spelling/stylistic changes (see merge request #26)
---
src/plugins/e-acsl/doc/userman/Makefile | 3 +-
src/plugins/e-acsl/doc/userman/eacslgcc.tex | 183 ++++++++++++++++++++
src/plugins/e-acsl/doc/userman/main.tex | 1 +
src/plugins/e-acsl/doc/userman/provides.tex | 177 -------------------
4 files changed, 186 insertions(+), 178 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/userman/eacslgcc.tex
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 25aafc00b0e..33d00dbf8c6 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -8,6 +8,7 @@ DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
provides.tex \
limitations.tex \
changes.tex \
+ eacslgcc.tex \
$(C_CODE) \
$(VERSION_FILE)
@@ -20,7 +21,7 @@ FC_VERSION= Sodium
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
-install:
+install:
cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
# cp -f main.pdf \
$(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
diff --git a/src/plugins/e-acsl/doc/userman/eacslgcc.tex b/src/plugins/e-acsl/doc/userman/eacslgcc.tex
new file mode 100644
index 00000000000..63c7fa7c482
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/eacslgcc.tex
@@ -0,0 +1,183 @@
+\chapter{Easy Instrumentation with \eacsl}
+
+Due to numerous instrumentation and compile-time options generating monitored
+executables using the \eacsl plug-in 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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Basic Use}
+
+\eacslgcc instruments C files provided at input using the \eacsl plug-in, and
+optionally compiles the generated code and the original sources using a \C
+compiler (\gcc by default).
+
+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 generated 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}
+names 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 the instrumentation step and
+compile a given program as if it were already instrumented by the \eacsl
+plug-in. This option is useful if one makes 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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{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 maximize 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 executable 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}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Customising \framac and \gcc Invocations}
+
+Runs of \framac and \gcc issued by \eacslgcc can be customized by using
+additional flags.
+
+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}
+
+yields 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 adds 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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{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 plug-ins 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 \eacslgcc output 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 file using the
+\texttt{-s} option. For example, the following command will redirect all
+output during instrumentation and compilation of \texttt{foo.c} to the
+file named \texttt{/tmp/log}.
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
+\end{shell}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{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 use 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 changed similarly using the \texttt{-G}
+option.
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 29010d84d70..4d713e7d3e2 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -56,6 +56,7 @@ Guillaume Petiot.
\include{introduction}
\include{provides}
+\include{eacslgcc}
\include{limitations}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index cf27296c588..da6ca9a13c3 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -774,181 +774,4 @@ typing & minimization of the instrumentation for integers
\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 plug-in 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 plug-in, 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 generated 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 the instrumentation step and
-compile a given program as if it were already instrumented by the \eacsl
-plug-in. This option is useful if one makes 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 executable 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 plug-ins 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 \eacslgcc output 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 file using the
-\texttt{-s} option. For example, the following command will redirect all
-output during instrumentation and compilation of \texttt{foo.c} to the
-file named \texttt{/tmp/log}.
-
-\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 use 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 changed similarly using the \texttt{-G}
-option.
--
GitLab