Commit 7fd007d6 authored by Basile Desloges 's avatar Basile Desloges

[eacsl:doc] Update user manual with latest E-ACSL outputs and URL

parent 65caae73
......@@ -4,14 +4,14 @@
André Maroneze and Virgile Prevosto and
Armand Puccetti and Julien Signoles and
Boris Yakobowski},
note = {\url{http://frama-c.cea.fr/download/user-manual.pdf}}
note = {\url{https://frama-c.com/download/frama-c-user-manual.pdf}},
}
@manual{plugin-dev-guide,
author = {Julien Signoles and Loïc Correnson and Matthieu Lemerre and
Virgile Prevosto},
title = {{Frama-C Plug-in Development Guide}},
note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
note = {\newline \url{https://frama-c.com/download/frama-c-plugin-development-guide.pdf}},
}
@manual{eva,
......@@ -19,7 +19,7 @@
Matthieu Lemerre and André Maroneze and Valentin Perelle and
Virgile Prevosto},
title = {{EVA} -- The Evolved Value Analysis plug-in},
note = {\mbox{\url{http://frama-c.cea.fr/download/value-analysis.pdf}}},
note = {\mbox{\url{https://frama-c.com/download/frama-c-value-analysis.pdf}}},
}
@manual{acsl,
......@@ -185,9 +185,15 @@ for C}},
month = oct,
}
@article{pldi16,
title = {{Shadow State Encoding for Efficient Monitoring of Block-level
Properties}},
author = {Kostyantyn Vorobyov and Julien Signoles and Nikolai Kosmatov},
note = {Submitted for publication},
@inproceedings{vorobyov17ismm,
author = { Vorobyov, Kostyantyn and Signoles, Julien and Kosmatov, Nikolai },
booktitle = { International Symposium on Memory Management (ISMM) },
title = { Shadow State Encoding for Efficient Monitoring of Block-level Properties },
year = { 2017 },
month = jun,
pages = {47--58},
location = { Barcelona, Spain },
doi = { 10.1145/3092255 },
pdf = {publis/2017_ismm.pdf},
publisher = { {ACM} },
}
......@@ -6,6 +6,7 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslpluginversion}
\begin{itemize}
\item Update every section with changes to \framac and \eacslgcc output
\item \textbf{Simple Example}: Remove option \texttt{-e-acsl-check}
\item \textbf{Combining E-ACSL with Other PLug-ins}: \texttt{-e-acsl-prepare} is
no more necessary.
......@@ -30,7 +31,7 @@ release. First we list changes of the last release.
\textbf{-e-acsl-prepare}.
\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
Monitoring Libraries'' by the new section ``Supported Systems''.
\item \textbf{Known Limitations}: Add limitation about monitoring of variables
\item \textbf{Known Limitations}: Add limitation about monitoring of variables
with incomplete types.
\end{itemize}
......
void __e_acsl_assert(int pred, char *kind,
char *func_name, char *pred_text, int line);
void __e_acsl_assert(int pred, const char *kind, const char *func_name,
const char *pred_txt, const char * file, int line);
\begin{shell}
\$ frama-c -e-acsl first.i -then-last -print
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
struct __e_acsl_contract_t;
typedef struct __e_acsl_contract_t __attribute__((__FC_BUILTIN__)) __e_acsl_contract_t;
struct __e_acsl_mpz_struct {
int _mp_alloc ;
int _mp_size ;
......@@ -15,39 +16,56 @@ struct __e_acsl_mpz_struct {
};
typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
/*@ ghost extern int __e_acsl_init; */
struct __e_acsl_mpq_struct {
__e_acsl_mpz_struct _mp_num ;
__e_acsl_mpz_struct _mp_den ;
};
typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
typedef unsigned long __e_acsl_mp_bitcnt_t;
/*@ requires pred != 0;
assigns \nothing; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred, char *kind,
char *fct,
char *pred_txt,
__attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred,
char const *kind,
char const *fct,
char const *pred_txt,
char const *file,
int line);
/*@ assigns \nothing; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_memory_init(int *argc_ref,
char ***argv,
size_t ptr_size);
extern size_t __e_acsl_heap_allocation_size;
/*@
predicate diffSize{L1, L2}(integer i) =
\at(__e_acsl_heap_allocation_size,L1) -
\at(__e_acsl_heap_allocation_size,L2) == i;
extern size_t __e_acsl_heap_allocated_blocks;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@ ghost extern int __e_acsl_init; */
long valid_nstring(char *s, long n, int wrtbl);
long valid_nwstring(wchar_t *s, long n, int wrtbl);
__inline static long valid_string__fc_inline(char *s, int wrtbl)
{
long tmp;
tmp = valid_nstring(s,(long)(-1),wrtbl);
return tmp;
}
__inline static long valid_wstring__fc_inline(wchar_t *s, int wrtbl)
{
long tmp;
tmp = valid_nwstring(s,(long)(-1),wrtbl);
return tmp;
}
*/
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
int x = 0;
/*@ assert x == 0; */
__e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
3);
/*@ assert x == 1; */
__e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",
4);
__e_acsl_assert(x == 0,"Assertion","main","x == 0","first.i",3);
/*@ assert x == 0; */ ;
__e_acsl_assert(x == 1,"Assertion","main","x == 1","first.i",4);
/*@ assert x == 1; */ ;
__retres = 0;
return __retres;
}
......
......@@ -2,14 +2,15 @@
extern int __e_acsl_sound_verdict;
void __e_acsl_assert(int pred, char *kind,
char *func_name, char *pred_text, int line) {
printf("%s at line %d in function %s is %s (%s).\n\
void __e_acsl_assert(int pred, const char *kind, const char *func_name,
const char *pred_text, const char *file, int line) {
printf("%s in file %s at line %d in function %s is %s (%s).\n\
The verified predicate was: `%s'.\n",
kind,
file,
line,
func_name,
pred ? "valid" : "invalid",
__e_acsl_sound_verdict ? "trustable" : "UNTRUSTABLE",
__e_acsl_sound_verdict ? "trustworthy" : "UNTRUSTWORTHY",
pred_text);
}
......@@ -15,7 +15,7 @@ program.
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
annotation checking'' would be more precise.}. This is the primary goal of
\eacsl. Indirectly, in combination with the \rte plug-in~\cite{rte} of \framac,
this
this
usage allows the user to detect undefined behaviors in its \C code. Second, it
allows to combine \framac and its existing analyzers with other \C analyzers
that do not natively understand the \acsl specification language. Third, the
......@@ -38,10 +38,12 @@ previous paragraph. Using \eacsl this way is therefore a fully automatic
process. Many usages, including automatic usages, are described in companion
research papers~\cite{rv13tutorial,rvcubes17tool,signoles18hdr}.
This manual does \emph{not} explain how to install the \eacsl plug-in. For
installation instructions please refer to the \texttt{INSTALL} file in the
\eacsl distribution. \index{Installation} Furthermore, even though this manual
provides examples, it is \emph{not} a full comprehensive tutorial on
The \eacsl plug-in is installed with \framac, but this manual does \emph{not}
explain how to install \framac. For installation instructions please refer to
the \texttt{INSTALL}\footnote{
\url{https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md}}
file in the \framac distribution. \index{Installation} Furthermore, even though
this manual provides examples, it is \emph{not} a full comprehensive tutorial on
\framac or \eacsl.
% You can still refer to any external
% tutorial~\cite{rv13tutorial} for additional examples.
......@@ -5,12 +5,13 @@ reference manual~\cite{eacsl} is not yet fully supported. Which annotations can
already be translated into \C code and which cannot is defined in a separate
document~\cite{eacsl-implem}. Second, even though we do our best to avoid them,
bugs may exist. If you find a new one, please report it on the bug tracking
system\footnote{\url{http://bts.frama-c.com}} (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 tedious 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.}.
system\footnote{\url{https://git.frama-c.com/pub/frama-c/-/issues}} (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
tedious to lift. Please contact us if you are interested in lifting these
limitations\footnote{Read
\url{https://git.frama-c.com/pub/frama-c/blob/master/CONTRIBUTING.md} for
additional details.}.
\section{Supported Systems}
......@@ -53,8 +54,8 @@ may get no runtime error depending on your \C compiler, but the behavior is
actually undefined because the assertion reads the uninitialized variable
\lstinline|x|. You should be caught by the \eacsl plug-in, but that is not
the case yet.
\begin{shell}
\begin{shell}
\$ e-acsl-gcc.sh uninitialized.i -c -Omonitored_uninitialized
monitored_uninitialized.i: In function 'main':
monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function
......@@ -98,22 +99,26 @@ Consider the following example.
You can generate the instrumented program as follows.
\begin{shell}
\$ e-acsl-gcc.sh -ML -omonitored_valid_no_main.i valid_no_main.c
<skip preprocessing commands>
\$ e-acsl-gcc.sh -M -omonitored_valid_no_main.i valid_no_main.c
[kernel] Parsing valid_no_main.c (with preprocessing)
[e-acsl] beginning translation.
<skip warnings about annotations from the Frama-C libc
which cannot be translated>
[kernel] warning: no entry point specified:
you must call function `__e_acsl_memory_init' by yourself.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Warning: no entry point specified:
you must call functions `__e_acsl_globals_init', `__e_acsl_globals_clean',
`__e_acsl_memory_init' and `__e_acsl_memory_clean' by yourself.
[e-acsl] translation done in project "e-acsl".
\end{shell}
The last warning states an important point: if this program is linked against
another file containing \texttt{main} function, then this main function must
be modified to insert a call to the function \texttt{\_\_e\_acsl\_memory\_init}
be modified to insert a calls to the functions
\texttt{\_\_e\_acsl\_globals\_init}
\index{e\_acsl\_globals\_init@\texttt{\_\_e\_acsl\_globals\_init}} and
\texttt{\_\_e\_acsl\_memory\_init}
\index{e\_acsl\_memory\_init@\texttt{\_\_e\_acsl\_memory\_init}} at the very
beginning. This function plays a very important role: it initializes metadata
storage used for tracking of memory blocks. Unless this call is inserted the
beginning. These functions play a very important role: the latter initializes
metadata storage used for tracking of memory blocks while the former initializes
tracking of global variables and constants. Unless these calls are inserted the
run of a modified program is likely to fail.
While it is possible to add such intrumentation manually we recommend using
......@@ -125,7 +130,7 @@ While it is possible to add such intrumentation manually we recommend using
Then just compile and run it as explained in Section~\ref{sec:memory}.
\begin{shell}
\$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
\$ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c
\$ e-acsl-gcc.sh -C -Ovalid_no_main monitored_modified_main.i monitored_valid_no_main.i
\$ ./valid_no_main.e-acsl
Assertion failed at line 11 in function f.
......@@ -192,7 +197,7 @@ functions.
\subsection{\eacsl Namespace}
While \eacsl uses source-to-source transformations and not binary
instrumentations it is important that the source code provided at input does
instrumentations it is important that the source code provided as input does
not contain any variables or functions prefixed \T{\_\_e\_acsl\_}. \eacsl
reserves this namespace for its transformations, and therefore an input program
containing such symbols beforehand may fail to be instrumented or compiled.
......
......@@ -20,7 +20,7 @@
\title{\eacsl Plug-in}{Release \eacslpluginversion
\ifthenelse{\equal{\eacslpluginversion}{\fcversion}}{}{%
\\[1em] compatible with \framac \fcversion}}
\author{Julien Signoles and Kostyantyn Vorobyov}
\author{Julien Signoles, Basile Desloges and Kostyantyn Vorobyov}
\begin{center}
CEA LIST\\ Software Reliability \& Security Laboratory
\end{center}
......@@ -41,8 +41,8 @@ CEA LIST\\ Software Reliability \& Security Laboratory
\addcontentsline{toc}{chapter}{Foreword}
This is the user manual of the \framac plug-in
\eacsl\footnote{\url{https://frama-c.com/eacsl.html}}. The contents of this
document correspond to its version \eacslpluginversion compatible with
\eacsl\footnote{\url{https://frama-c.com/fc-plugins/e-acsl.html}}. The contents
of this document correspond to its version \eacslpluginversion compatible with
\fcversion version of \framac~\cite{userman,fac15}. The development of
the \eacsl plug-in is still ongoing. Features described by this document may
evolve in the future.
......@@ -50,9 +50,8 @@ evolve in the future.
\section*{Acknowledgements}
We gratefully thank the people who contributed to this document:
Basile Desloges, Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner,
Nikola\"i Kosmatov, Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and
Guillaume Petiot.
Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola\"i Kosmatov,
Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -44,13 +44,9 @@ Running \eacsl on \texttt{first.i} consists of adding \shortopt{e-acsl} option
to the \framac command line:
\begin{shell}
\$ frama-c -e-acsl first.i
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
<skip a warning when translating the Frama-C libc>
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
\end{shell}
......@@ -58,8 +54,8 @@ Even though \texttt{first.i} has already been pre-processed, \eacsl first asks
the \framac kernel to process and combine it against several header files
provided by the \eacsl plug-in. Further \eacsl translates the annotated code
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 \shortopt{e-acsl} does nothing
\emph{project} is explained in Section 8.1 of the \framac user
manual~\cite{userman}.}. By default, the option \shortopt{e-acsl} does nothing
more. It is however possible to have a look at the generated code in the
\framac GUI. This is also possible through the command line thanks to the
kernel options \shortopt{then-last} and \shortopt{print}. The former
......@@ -72,15 +68,15 @@ As you can see, the generated code contains additional type declarations,
constant declarations and global \acsl annotations not present in the initial
file \texttt{first.i}. They are part of the \eacsl monitoring library. You can
safely ignore them for now. The translated \texttt{main} function of
\texttt{first.i} is displayed at the end. After each \eacsl annotation,
\texttt{first.i} is displayed at the end. Before each \eacsl annotation,
a call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert} has been added.
\begin{minipage}{\linewidth}
\begin{ccode}
/*@ assert x == 0; */
__e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
/*@ assert x == 1; */
__e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
__e_acsl_assert(x == 0,"Assertion","main","x == 0","first.i",3);
/*@ assert x == 0; */ ;
__e_acsl_assert(x == 1,"Assertion","main","x == 1","first.i",4);
/*@ assert x == 1; */ ;
\end{ccode}
\end{minipage}
......@@ -117,15 +113,15 @@ corresponding to your compiler and your system. For instance, in a 64-bit
machine you should also pass
\shortopt{machdep} \texttt{x86\_64} option as follows:
\begin{shell}
\$ frama-c -machdep x86_64 -e-acsl first.i -then-last \
-print -ocode monitored_first.c
\$ frama-c -machdep x86_64 -e-acsl first.i -then-last \
-print -ocode monitored_first.c
\end{shell}
This file can be compile with a \C compiler (for instance \gcc), as follows:
\lstset{escapechar=£}
\begin{shell}
\$ gcc -c -Wno-attributes monitored_first.c
\$ gcc -c -Wno-attributes monitored_first.c
\end{shell}
However, creating an executable through a proper invokation to \gcc is painful
......@@ -154,7 +150,7 @@ 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 -omonitored_first.i first.i
\$ e-acsl-gcc.sh -omonitored_first.i first.i
\end{shell}
The above command instruments \texttt{first.i} with runtime assertions and
......@@ -167,7 +163,7 @@ Compilation and Linking of the original and the instrumented sources
is enabled using the \shortopt{c} option. For instance, command
\begin{shell}
\$ e-acsl-gcc.sh -c -omonitored_first.i first.i
\$ e-acsl-gcc.sh -c -omonitored_first.i first.i
\end{shell}
instruments the code in \texttt{first.i}, outputs it to
......@@ -180,18 +176,19 @@ You can execute the generate binaries, in particular \texttt{a.out.e-acsl} which
detects at runtime the incorrect annotation.
\begin{shell}
\$ ./a.out.e-acsl
Assertion failed at line 4 in function main.
The failing predicate is:
x == 1.
Aborted
first.i: In function 'main'
first.i:4: Error: Assertion failed:
The failing predicate is:
x == 1.
Aborted (core dumped)
\$ echo \$?
134
\end{shell}
The execution aborts with a non-zero exit code (134) and an error message
indicating \eacsl annotation that has been violated. There is no output for the
valid \eacsl annotation. That is, the run of an executable generated from the
instrumented source file (i.e., \texttt{monitored\_first.i}) detects that the
second annotation in the initial program is invalid, whereas the first
indicating an \eacsl annotation that has been violated. There is no output for
the valid \eacsl annotation. That is, the run of an executable generated from
the instrumented source file (i.e., \texttt{monitored\_first.i}) detects that
the second annotation in the initial program is invalid, whereas the first
annotation holds for this execution.
Named executables can be created using the \shortopt{O} option. This is such
......@@ -201,7 +198,7 @@ generated from the original program and the executable generated from the
For example, command
\begin{shell}
\$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
\$ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i
\end{shell}
names the executables generated from \texttt{first.i} and
\texttt{monitored\_first.i}: \texttt{monitored\_first} and
......@@ -213,7 +210,7 @@ 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 -Omonitored_first monitored_first.i
\$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
\end{shell}
The above command generates a single executable named
......@@ -230,16 +227,16 @@ also be passed using \shortopt{I} and \shortopt{G} options
respectively, for instance as follows:
\begin{shell}
\$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
\$ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c
\end{shell}
Runs of \framac and \gcc issued by \eacslgcc can further be customized by using
additional flags. \framac flags can be passed using the \shortopt{F} option,
while \shortopt{l} and \shortopt{e} options allow for passing additional
while \shortopt{e} and \shortopt{l} 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
\$ 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
......@@ -264,7 +261,7 @@ 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
\$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
\end{shell}
Verbosity of the \eacslgcc output can also be reduced using the \shortopt{q}
......@@ -277,7 +274,7 @@ 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
\$ e-acsl-gcc.sh -c -s/tmp/log foo.c
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -304,6 +301,7 @@ One of the benefits of using the wrapper script is that it makes sure that
further passed \shortopt{m64} or \shortopt{m32} options to generate code using
64-bit or 32-bit ABI respectively.
At the present stage of implementation \eacsl does not support generating
executables with ABI different to the default one.
......@@ -313,13 +311,13 @@ executables with ABI different to the default one.
For full up-to-date documentation of \eacslgcc see its man page:
\begin{shell}
\$ man e-acsl-gcc.sh
\$ man e-acsl-gcc.sh
\end{shell}
Alternatively, you can also use the \shortopt{h} option of \eacslgcc:
\begin{shell}
\$ man e-acsl-gcc.sh -h
\$ e-acsl-gcc.sh -h
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -347,8 +345,8 @@ is undefined if $e$ leads to a runtime error and, consequently, the semantics of
any term $t$ (resp. predicate $p$) containing such a construct $c$ is
undefined as soon as $e$ has to be evaluated in order to evaluate $t$
(resp. $p$). The \eacsl Reference Manual also states that \emph{``it is the
responsibility of each tool which interprets \eacsl to ensure that an
undefined term is never evaluated''}~\cite{eacsl}.
responsibility of each tool which interprets \eacsl to ensure that an
undefined term is never evaluated''}~\cite{eacsl}.
Accordingly, the \eacsl plug-in prevents an undefined term from being
evaluated. If an annotation contains such a term, \eacsl will report a proper
......@@ -390,20 +388,20 @@ line.
It might be particularly useful in one of the following contexts:
\begin{itemize}
\item several libc functions used by the analyzed program are still not defined
in the \framac libc; or
\item your system libc and the \framac libc mismatch about several function
types (for instance, your system libc is not 100\% POSIX compliant); or
\item several \framac lib functions get a contract and you are not interested in
verifying them (for instance, only checking undefine behaviors matters).
\item several libc functions used by the analyzed program are still not defined
in the \framac libc; or
\item your system libc and the \framac libc mismatch about several function
types (for instance, your system libc is not 100\% POSIX compliant); or
\item several \framac lib functions get a contract and you are not interested in
verifying them (for instance, only checking undefine behaviors matters).
\end{itemize}
\begin{important}
Notably, \eacslgcc disables \framac libc by default. This is because most of
its functions are annotated with \eacsl contracts and generating code for
these contracts results in additional runtime overheads. To enforce default
\framac contracts with \eacslgcc you can pass \shortopt{L} option to the wrapper
script.
Notably, \eacslgcc disables \framac libc by default. This is because most of
its functions are annotated with \eacsl contracts and generating code for
these contracts results in additional runtime overheads. To enforce default
\framac contracts with \eacslgcc you can pass \shortopt{L} option to the wrapper
script.
\end{important}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -464,10 +462,11 @@ reports the violation of the second annotation:
\begin{shell}
\$ e-acsl-gcc.sh -c -Ovalid valid.c
\$ ./valid.e-acsl
Assertion failed at line 11 in function main.
The failing predicate is:
freed: \valid(x).
Aborted
valid.c: In function 'main'
valid.c:11: Error: Assertion failed:
The failing predicate is:
freed: \valid(x).
Aborted (core dumped)
\end{shell}
To check memory-related predicates (such as \lstinline|\valid|) \eacsl tracks
......@@ -494,11 +493,10 @@ location \T{x} as belonging unallocated memory space.
Memory tracking implemented by the \eacsl library comes in two flavours dubbed
\I{bittree-based} and \I{segment-based} memory models. With the bittree-based
model meta-storage is implemented as a compact prefix trie called Patricia
trie~\cite{rv13}, whereas segment-based memory model
\footnote{Segment-based model of \eacsl has not yet appeared in the literature.}
is based on shadow memory~\cite{pldi16}. The functionality of the provided
memory models is equivalent, however they differ in performance. We further
discuss performance considerations.
trie~\cite{rv13}, whereas segment-based memory model is based on shadow
memory~\cite{vorobyov17ismm}. The functionality of the provided memory models is
equivalent, however they differ in performance. We further discuss performance
considerations.
The \eacsl models allocate heap memory using a customized version of the
\dlmalloc\footnote{\url{http://dlmalloc.net/}} memory allocator replacing
......@@ -537,7 +535,7 @@ performance. The bittree-based model uses compact memory representation of
metadata. The segment-based model on the other hand uses significantly more
memory. You can expect over 2x times memory overheads when using it. However It
is often an order of magnitude faster than the bittree-based
model~\cite{pldi16}.
model~\cite{vorobyov17ismm}.
%[Need ref here with comparison of the performance. Ideally a reference to the PLDI paper].
......@@ -553,9 +551,9 @@ feature can be enabled using the \shortopt{M} switch of \eacslgcc or
\shortopt{e-acsl-full-mtracking} option of the \eacsl plug-in.
\begin{important}
The above-mentioned static analysis is probably the less robust part of \eacsl
for the time being. When handling a large piece of code, it might be necessary
to deactivate it and systematically instrument the code as explained above.
The above-mentioned static analysis is probably the less robust part of \eacsl
for the time being. When handling a large piece of code, it might be necessary
to deactivate it and systematically instrument the code as explained above.
\end{important}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -636,7 +634,7 @@ that uses \texttt{exit(CODE)} instead of \texttt{abort}.
For instance, the program generated using the following command
exits with code \texttt{5} on a predicate violation.
\begin{shell}
\$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
\$ e-acsl-gcc.sh -c --fail-with-code=5 foo.c
\end{shell}
Forceful termination of a monitored program can be disabled using
......@@ -657,7 +655,7 @@ following signature:
Additionally, it may depends on the global variable
\texttt{\_\_e\_acsl\_sound\_verdict}\codeidxdef{e\_acsl\_sound\_verdict}. This
variable of type \texttt{int} is set to \texttt{0} as soon as the verdict