Skip to content
Snippets Groups Projects
Commit ae1b5fc5 authored by Julien Signoles's avatar Julien Signoles
Browse files

[E-ACSL] manual: Florent's comments

parent 78354f41
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/doc/userman/introduction.tex
+ 10
− 10
View file @ ae1b5fc5
......@@ -5,23 +5,23 @@ which supports the ACSL specification language~\cite{acsl}. This manual
documents the \eacsl plug-in of \framac, version \eacslversion. Which \eacsl
version you are using is indicated by running \texttt{frama-c
-e-acsl-version}\optionidx{-}{e-acsl-version}. This plug-in automatically
translates an annotated C code into another one which fails at runtime if an
annotation is violated. If no annotation is violated, the behavior of the new
translates an annotated C program into another program that fails at runtime if
an annotation is violated. If no annotation is violated, the behavior of the new
program is exactly the same than the one of the original program.
Such a translation brings several benefits. First it allows the user to monitor
a \C code, in particular to perform what is usually called ``runtime assertion
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
annotation checking'' would be a better more-general expression.}. That is the
primary goal of \eacsl. Second it allows to combine \framac and its existing
analyzers, with other analyzer tools for \C like
\pathcrawler~\cite{pathcrawler}, even those who do not understand the \acsl
annotation checking'' would be a better more-general expression.}. This is the
primary goal of \eacsl. Second it allows the combination of \framac and its
existing analyzers, with other analyzer tools for \C like
\pathcrawler~\cite{pathcrawler} that do not natively understand the \acsl
specification language. Third, the possibility to detect invalid annotations
during a concrete execution may be very helpful while writing a correct
specification of a given program, \emph{e.g.} for later program proving.
Finally, an executable specification makes it possible to check at runtime
assertions that cannot be verified statically and thus to establish a link
between monitoring tools and static analysis tools like
Finally, an executable specification makes it possible to check assertions that
cannot be verified statically at runtime and thus to establish a link between
monitoring tools and static analysis tools like
\valueplugin~\cite{value}\index{Value} or \wpplugin~\cite{wp}\index{Wp}.
Annotations must be written in the \eacsl specification
......@@ -30,6 +30,6 @@ a preliminary state: some parts of E-ACSL are not yet supported. Which \eacsl
annotations are currently handled by the \eacsl plug-in is documented in a
separated document~\cite{eacsl-implem}.
This manual does \emph{\textbf{not}} explain how to install the plug-in. Please
This manual does \emph{not} explain how to install the plug-in. Please
have a look at file \texttt{INSTALL} of the \eacsl tarball for this
purpose.\index{Installation}
src/plugins/e-acsl/doc/userman/limitations.tex
+ 24
− 24
View file @ ae1b5fc5
......@@ -3,29 +3,29 @@
The development of the \eacsl plug-in is still ongoing. First, the whole \eacsl
reference manual~\cite{eacsl} is not yet supported. Which annotations are
already translated into \C code and which are not is defined in a separated
document~\cite{eacsl-implem}. Second, even if we do our best, bugs may exist. If
you find a new one, please report it on the bug tracking system (see Chapter 10
of the \framac User Manual~\cite{userman}). Third, there are some additional
known limitations, which could be annoying for the user in some cases, but are
hard to lift. Thus they could be there for a while. Lifting them could be part
of commercial supports\footnote{Contact us or read
\url{http://frama-c.com/support.html} for additional details.}.
\section{Uninitialized Value}
document~\cite{eacsl-implem}. Second, even though we do our best, bugs may
exist. If you find a new one, please report it on the bug tracking system (see
Chapter 10 of the \framac User Manual~\cite{userman}). Third, there are some
additional known limitations, which could be annoying for the user in some
cases, but are hard to lift. Please contact us if you are interested in lifting
these limitations\footnote{Read \url{http://frama-c.com/support.html} for
additional details.}.
\section{Uninitialized Values}
\index{Uninitialized value}
As explained in Section~\ref{sec:runtime-error}, the \eacsl plug-in should never
translate an annotation into a \C code which can lead to a runtime error. That
is the case, except for uninitialized values which are values read before having
been written like in the following example.
translate an annotation into \C code which can lead to a runtime error. This is
enforced, except for uninitialized values which are values read before having
been written.
\listingname{uninitialized.i}
\cinput{examples/uninitialized.i}
If you generate the instrumented code, compile it, and finally execute it, you
may get no runtime error depending on your \C compiler, but the behavior is
actually uninitialized and should be trap by the \eacsl plug-in. That is not the
case yet.
actually uninitialized and should be caught by the \eacsl plug-in. That is not
the case yet.
\begin{shell}
\$ frama-c -e-acsl uninitialized.i -then-on e-acsl -print \
-ocode monitored_uninitialized.i
......@@ -37,9 +37,9 @@ monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this func
\$ ./monitored_uninitialized
\end{shell}
Actually that is more a design choice that a limitation: if the \eacsl plug-in
would generate additional instrumentation to prevent such values to be executed,
the generated code would be much more verbose and much slower.
This is more a design choice that a limitation: should the \eacsl plug-in
generate additional instrumentation to prevent such values to be executed, the
generated code would be much more verbose and much slower.
If you really want to track such uninitializations in your annotation, you have
to manually add calls to the \eacsl predicate
......@@ -56,7 +56,7 @@ may be incorrect. That is made explicit by a warning displayed when the \eacsl
plug-in is running (see examples of Sections~\ref{sec:no-main} and
\ref{sec:no-code}).
\subsection{Program without Main}
\subsection{Programs without Main}
\index{Program!Without main}
\label{sec:limits:no-main}
......@@ -106,7 +106,7 @@ The failing predicate is:
freed: \valid(x).
\end{shell}
\subsection{Function without Code}
\subsection{Functions without Code}
\label{sec:limits:no-code}
\index{Function!Without code}
......@@ -120,7 +120,7 @@ memory-related annotation $a$ and a function $f$ without code if and only if:
There is no workaround yet.
Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
function without code. There is also no workaround yet.
functions without code. There is also no workaround yet.
\section{Recursive Function}
\index{Function!Recursive}
......@@ -129,17 +129,17 @@ Programs containing recursive functions have the same limitations than the ones
containing function without code (Section~\ref{sec:limits:no-code}) and
memory-related annotations.
Also, even if there is no such annotations, the generated code may call a
Also, even though there is no such annotations, the generated code may call a
function before it is declared. This behavior appears in a non-specified
way. The generated code is however easy to fix by hand.
\section{Variadic Function}
\section{Variadic Functions}
\index{Function!Variadic}
Programs containing variadic functions without code but with a function contract
are not yet supported. There is no workaround.
are not yet supported. There is no workaround yet.
\section{Function Pointer}
\section{Function Pointers}
\index{Function!Pointer}
Programs containing function pointers have the same limitations as about
......
src/plugins/e-acsl/doc/userman/main.pdf
-800 B (0%)
View file @ ae1b5fc5
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
src/plugins/e-acsl/doc/userman/main.tex
+ 5
− 5
View file @ ae1b5fc5
......@@ -40,16 +40,16 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
\addcontentsline{toc}{chapter}{Foreword}
This is the user manual of the \framac plug-in
\eacsl\footnote{\url{http://frama-c.com/eacsl}}. The content of this document
corresponds to its version \eacslversion (\today) compatible with the version
\eacsl\footnote{\url{http://frama-c.com/eacsl}}. The contents of this document
correspond to its version \eacslversion (\today) compatible with the version
\fcversion of \framac~\cite{userman,sefm12}. However the development of the
\eacsl plug-in is still ongoing: features described here may still evolve in the
future.
%% \section*{Acknowledgements}
\section*{Acknowledgements}
%% We gratefully thank all the people who contributed to this document: Patrick
%% Baudin, Mickal Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente.
We gratefully thank all the people who contributed to this document: Florent
Kirchner, Nikola Kosmatov and Guillaume Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
src/plugins/e-acsl/doc/userman/provides.tex
+ 72
− 70
View file @ ae1b5fc5
......@@ -3,15 +3,15 @@
This chapter is the core of this manual and describes how to use the
plug-in. You can still call the option \optiondef{-}{e-acsl-help} to get the
list of available options with few lines of documentation. First,
Section~\ref{sec:simple} shows how to run the plug-in on a trivial example and
how to execute the generated code with a standard \C compiler to detect invalid
Section~\ref{sec:simple} shows how to run the plug-in on a toy example and how
to execute the generated code with a standard \C compiler to detect invalid
annotations at runtime. Then, Section~\ref{sec:exec-env} provides additional
details on the execution of the generated code. Next,
Section~\ref{sec:incomplete} focuses on how to deal with incomplete programs,
\emph{i.e.} in which some functions have no body or in which there are no main
function. After, Section~\ref{sec:combine} explains how to combine the plug-in
function. Section~\ref{sec:combine} explains how to combine the \eacsl plug-in
with others \framac plug-ins. Finally, Section~\ref{sec:custom} introduces how
to customize the plug-in, while Section~\ref{sec:verbose} details the verbosing
to customize the plug-in, and Section~\ref{sec:verbose} details the verbosing
policy of the plug-in.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -59,7 +59,7 @@ translates it into a new \framac project named \texttt{e-acsl}\footnote{The
notion of \emph{project} is explained in Section 8.1 of the \framac user
manual~\cite{userman}.}. By default, the option \optionuse{-}{e-acsl} does
nothing more. It is however possible to have a look at the generated code in the
\framac GUI. It is also possible through the command line thanks to the kernel
\framac GUI. This is also possible through the command line thanks to the kernel
options \optionuse{-}{then-on} and \optionuse{-}{print} which respectively
switches to another project and pretty prints the \C code~\cite{userman}:
......@@ -173,7 +173,7 @@ against the file \texttt{`frama-c -print-share-path`/e-acsl/e\_acsl.c}. This
last file is part of the \eacsl library installed with the plug-in. It contains
an implementation of the function
\texttt{e\_acsl\_assert}\codeidx{e\_acsl\_assert}, which is required to generate
an executable binary from an \eacsl-generated code.
an executable binary from the \eacsl-instrumented code.
The warnings can be safely ignored. They refer to an attribute
\texttt{FC\_BUILTIN} internally used by \framac. You can also add the option
......@@ -204,8 +204,8 @@ this execution.
The environment in which the code is executed is not necessarily the same than
the one assumed by \framac. You must take care of that when running the \eacsl
plug-in and when compiling the generated code with \gcc. Also, the plug-in
offers you few possibilities of customization.
plug-in and when compiling the generated code with \gcc. In this aspect, the
plug-in offers a few possibilities of customization.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -223,9 +223,9 @@ evaluate $t$ (resp. $p$). The \eacsl Reference Manual also states that
\emph{``it is the responsibility of the tools which interprets \eacsl to ensure
that an undefined term is never evaluated''}~\cite{eacsl}.
Accordingly, the \eacsl plug-in prevents undefined term to be evaluated. If it
should be because an annotation contains such a term, it will report a proper
error at runtime instead.
Accordingly, the \eacsl plug-in prevents undefined terms from being
evaluated. Should it be because an annotation contains such a term, it will
report a proper error at runtime instead.
Consider for instance the following annotated program.
......@@ -259,14 +259,14 @@ division_by_zero: y != 0.
\subsection{Architecture Dependent Annotations}
In many cases, the execution of a \C program depends on the underlying machine
architecture which it is executed on. Also the program must be compiled in the
very same architecture (or cross-compiled) for the compiler being able to
generate a correct binary.
\framac mades assumptions about this machine when analyzed such a file. By
default, it assumes a x86 32 bits platform, but it may be changed thanks to the
option \optionuse{-}{machdep}~\cite{userman}. This option is of primary
importance when using the \eacsl plug-in: it must be set to the value
architecture which it is executed on. The program must be compiled in the very
same architecture (or cross-compiled) for the compiler being able to generate a
correct binary.
\framac makes assumptions about the machine architecture when analyzing such a
file. By default, it assumes a x86 32 bits platform, but it may be changed
thanks to the option \optionuse{-}{machdep}~\cite{userman}. This option is of
primary importance when using the \eacsl plug-in: it must be set to the value
corresponding to the machine which the generated code will be executed on if the
code \emph{or the annotation} is machine dependent.
......@@ -336,12 +336,12 @@ To compile it however, you need to have \gmp installed and to add the option
\optionuse{-}{lgmp} to \gcc as follows:
\begin{shell}
\$ gcc -o gmp `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_gmp.i -lgmp
\$ gcc -o pow_gmp `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_gmp.i -lgmp
\end{shell}
We can now execute it as usual.
\begin{shell}
\$ ./gmp
\$ ./pow_gmp
\end{shell}
Since the assertion is valid, there is no output in this case.
......@@ -349,16 +349,16 @@ Since the assertion is valid, there is no output in this case.
The option \optiondef{-}{e-acsl-gmp-only} (unset by default) may be set to
always generate \gmp integers, even when it is not required. If it is set, the
generated program must be linked against \gmp as soon as there is an integer or
any integral \C type in an annotation.
any integral \C type in an \eacsl annotation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Memory-related Annotations}
\label{sec:memory}
The \eacsl plug-in handles memory-related annotations like
The \eacsl plug-in handles memory-related annotations such as
\lstinline|\valid|. When using such an annotation, the generated code must be
linked against a dedicated library installed with the plug-in to be
linked against a specific library installed with the plug-in to be
executed. This library includes two \C files which are installed in the \eacsl'
share directory:
\begin{itemize}
......@@ -399,16 +399,17 @@ The failing predicate is:
freed: \valid(x).
\end{shell}
Like for integers, we do our best to use the dedicated library only when
required~\cite{rv13}. So, if your program does not contain memory-related
annotations, the generated one does not require to be linked against the
dedicated memory library, like the examples of the previous sections.
Like for integers, the \eacsl plug-in does its best to use the dedicated library
only when required~\cite{rv13}. So, if your program does not contain
memory-related annotations, the generated one does not require to be linked
against the dedicated memory library, like the examples of the previous
sections.
However, if your program has annotations with pointer dereferencing (for
instance), then the generated code \emph{does} require to be linked against the
dedicated library at compile time. Why? Because pointer dereferencing may lead
to runtime errors, so the \eacsl plug-in inserts runtime checks to prevent them
according to Section~\ref{sec:runtime-error} as shown by the following example.
according to Section~\ref{sec:runtime-error}, witness the following example.
\listingname{pointer.c}
\cinput{examples/pointer.c}
......@@ -433,7 +434,7 @@ linked against the memory library.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Execution Behavior Environment}
\subsection{Runtime Monitor Behavior}
When a predicate is checked at runtime, the function
\texttt{e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} is called. Its body is
......@@ -449,8 +450,8 @@ example which prints the validity status of each property but never exits.
\listingname{my\_assert.c}
\cinput{examples/my_assert.c}
Then you can generate the program as usual, but use your own file to compile it
instead \texttt{e\_acsl.c} as shown below (we reuse the initial example
Then you can generate the program as usual, but use your own file to compile it,
instead of \texttt{e\_acsl.c}, as shown below (we reuse the initial example
\texttt{first.i} of this manual).
\begin{shell}
......@@ -467,7 +468,7 @@ The verified predicate was: `x == 1'.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Incomplete Program}
\section{Incomplete Programs}
\label{sec:incomplete}
Executing a \C program requires to have a complete application. However, the
......@@ -476,7 +477,7 @@ instrumented code.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Program without Main}
\subsection{Programs without Main}
\label{sec:no-main}
\index{Program!Without main}
......@@ -487,7 +488,7 @@ Consider for instance the following annotated program without such a
\listingname{no\_main.i}
\cinput{examples/no_main.i}
The instrumented code is generated as usual, even if you get an additional
The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ frama-c -e-acsl no_main.i -then-on e-acsl -print -ocode monitored_no_main.i
......@@ -512,15 +513,15 @@ explained in Section~\ref{sec:integers}.
\cinput{examples/main.c}
\begin{shell}
\$ gcc -o no_main `frama-c -print-share-path`/e-acsl/e_acsl.c \
\$ gcc -o with_main `frama-c -print-share-path`/e-acsl/e_acsl.c \
monitored_no_main.i main.c -lgmp
\$ ./no_main
\$ ./with_main
x = 65536
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Function without Code}
\subsection{Functions without Code}
\label{sec:no-code}
\index{Function!Without code}
......@@ -531,7 +532,7 @@ implementation of the function \texttt{my\_pow} is not provided.
\listingname{no\_code.c}
\cinput{examples/no_code.c}
The instrumented code is generated as usual, even if you get an additional
The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
[e-acsl] beginning translation.
......@@ -545,11 +546,11 @@ generating default assigns from the prototype
Like in the previous Section, this warning indicates that the instrumentation
would be incorrect if the program contains memory-related annotations (see
Section~\ref{sec:limits:no-code}). That is still not the case here, so you
can safely ignore it. Now, it is possible to compile the generated code with a
\C compiler in a standard way, and even to link it against additional files that
provided an implementation for the missing functions like the following one. In
this particular case, we also need to link against \gmp as explained in
Section~\ref{sec:limits:no-code}). That is still not the case here, so you can
safely ignore it. Now, it is possible to compile the generated code with a \C
compiler in a standard way, and even to link it against additional files that
provide an implementation for the missing functions such as the following
one. In this particular case, we also need to link against \gmp as explained in
Section~\ref{sec:integers}.
\listingname{pow.i}
......@@ -566,7 +567,7 @@ The failing predicate is:
The execution of the corresponding binary fails at runtime: actually, our
implementation of the function \texttt{my\_pow} that we use several times since
the beginning of this manual may overflow in case of big exponentiations.
the beginning of this manual may overflow in case of large exponentiations.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -579,12 +580,12 @@ As the \eacsl plug-in generates a new \framac project, it is easy to run any
plug-in on the generated program, either in the same \framac session (thanks to
the option \optionuse{-}{then} or through the GUI), or in another one. The only
issue might be that, depending on the plug-in, the analysis may be imperfect if
the generated program uses \gmp or the dedicated memory library: both
intensively use dynamic structures which are usually difficult to handle by
the generated program uses \gmp or the dedicated memory library: both make
intensive use of dynamic structures which are usually difficult to handle by
analysis tools.
Another way to combine \eacsl with others plug-ins is to run \eacsl afterward.
For instance, the \rte plug-in~\cite{rte} may be used to generate annotations
Another way to combine \eacsl with others plug-ins is to run \eacsl last. For
instance, the \rte plug-in~\cite{rte} may be used to generate annotations
corresponding to runtime errors. Then the \eacsl plug-in may generate an
instrumented program to verify that there is no such runtime errors during the
execution of the program.
......@@ -607,9 +608,9 @@ a new temporary project in which it links the analyzed program against its own
library in order to generate the \framac internal representation of the \C
program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
even if the \eacsl plug-in keeps the maximum amount of information, results of
already executed analyzer (like the validity status of the annotations) are not
known in this new project. If you want to keep them, you have to set the option
\optiondef{-}{e-acsl-prepare} when the first analysis is asked for.
already executed analyzers (such as the validity status of the annotations) are
not known in this new project. If you want to keep them, you have to set the
option \optiondef{-}{e-acsl-prepare} when the first analysis is asked for.
In this context, the \eacsl plug-in does not generate code for annotations
proven valid by another plug-in, except if you explicitly set the option
......@@ -643,16 +644,16 @@ plug-in is running.
There are few ways to customize the \eacsl plug-in.
First, the name of the generated project ---which is \texttt{e-acsl} by
default--- may be changed by setting the option \optiondef{-}{e-acsl-project}.
First, the name of the generated project -- which is \texttt{e-acsl} by
default -- may be changed by setting the option \optiondef{-}{e-acsl-project}.
Second, the directory which the \eacsl library files are searched in ---which is
\texttt{`frama-c -print-share-path`/e-acsl} by default--- may be changed by
Second, the directory which the \eacsl library files are searched in -- which is
\texttt{`frama-c -print-share-path`/e-acsl} by default -- may be changed by
setting the option \optiondef{-}{e-acsl-share}.
Third, the option \optiondef{-}{e-acsl-check} does not generate any new project
but it only verifies that each annotation is translatable. Then it produces a
summary as shown in the following example (left shift in annotation is not
summary as shown in the following example (left shifts in annotation are not
yet supported by the \eacsl plug-in).
\listingname{check.i}
......@@ -671,22 +672,22 @@ check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet suppo
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Verbosing Policy}
\section{Verbosity Policy}
\label{sec:verbose}
By default, \eacsl does not provide many information when it is running. Mainly,
By default, \eacsl does not provide much information when it is running. Mainly,
it prints a message when it begins the translation, and one other when the
translation is done. It may also displays warnings when something usually
requires the attention of the user, for instance if it is not able to translate
an annotation. Such information is usually enough but, in some cases, you might
want to get additional controls on what is displayed. As quite usual in \framac,
the \eacsl plug-in offers two different ways to do this: the verbosing level
which indicates the \emph{amount} of information to display, and the message
categories which indicates the \emph{kind} of information to display.
translation is done. It may also display warnings when something requires the
attention of the user, for instance if it is not able to translate an
annotation. Such information is usually enough but, in some cases, you might
want to get additional controls on what is displayed. As quite usual with
\framac plug-ins, \eacsl offers two different ways to do this: the verbosity
level which indicates the \emph{amount} of information to display, and the
message categories which indicates the \emph{kind} of information to display.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Verbosing Level}
\subsection{Verbosity Level}
The amount of information displayed by the \eacsl plug-in is settable by the
option \optiondef{-}{e-acsl-verbose}. It is 1 by default. Below is indicated
......@@ -701,11 +702,12 @@ also displays the information of the level $n-1$.
\texttt{-e-acsl-verbose 1}& beginning and ending of the translation\\
\hline
\texttt{-e-acsl-verbose 2}& different parts of the translation and
about functions\\
functions-related information\\
\hline
\texttt{-e-acsl-verbose 3}& about predicates and statements\\
\texttt{-e-acsl-verbose 3}& predicates- and statements-related information\\
\hline
\texttt{-e-acsl-verbose 4 and above}& about terms and expressions\\
\texttt{-e-acsl-verbose 4 and above}& terms- and expressions-related information
\\
\hline
\end{tabular}
\end{center}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment