From 7fd007d6d643be6a06e6c895d54040116ee149c6 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 16 Nov 2020 15:37:46 +0100
Subject: [PATCH] [eacsl:doc] Update user manual with latest E-ACSL outputs and
URL
---
src/plugins/e-acsl/doc/userman/biblio.bib | 22 +-
src/plugins/e-acsl/doc/userman/changes.tex | 3 +-
.../e-acsl/doc/userman/examples/assert_sign.c | 4 +-
.../doc/userman/examples/instrumented_first.c | 68 +++--
.../e-acsl/doc/userman/examples/my_assert.c | 9 +-
.../e-acsl/doc/userman/introduction.tex | 12 +-
.../e-acsl/doc/userman/limitations.tex | 41 +--
src/plugins/e-acsl/doc/userman/main.tex | 11 +-
src/plugins/e-acsl/doc/userman/provides.tex | 277 +++++++++---------
9 files changed, 240 insertions(+), 207 deletions(-)
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index ebf119a6438..dc9980cd64f 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -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} },
}
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 034766eaca3..1dcc066fe7c 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -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}
diff --git a/src/plugins/e-acsl/doc/userman/examples/assert_sign.c b/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
index ce2e56c6fb9..7d2fb1842f2 100644
--- a/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
+++ b/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
@@ -1,2 +1,2 @@
-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);
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
index a940f8c891f..54948acabb3 100644
--- a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
+++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
@@ -1,13 +1,14 @@
\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;
}
diff --git a/src/plugins/e-acsl/doc/userman/examples/my_assert.c b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
index c006779bc5b..d6f42e6db32 100644
--- a/src/plugins/e-acsl/doc/userman/examples/my_assert.c
+++ b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
@@ -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);
}
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 08956a9c61a..dd28d602b28 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -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.
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 45caa5d91dc..1a20cd3d97c 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -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.
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index f2f73c8229c..3e3ce0bed39 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -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.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index f9dedfdf868..f393932c92f 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -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
-provided by \eacsl is not trustable anymore (see
+provided by \eacsl is not trustworthy anymore (see
Section~\ref{sec:partial-instrumentation}).
Below is an example which prints the validity status of each property but never
@@ -675,9 +673,9 @@ with the customized one specified in \texttt{my\_assert.c}
\begin{shell}
\$ e-acsl-gcc.sh -c -X first.i -Ofirst --external-assert=my_assert.c
\$ ./first.e-acsl
-Assertion at line 3 in function main is valid (trustable).
+Assertion in file first.i at line 3 in function main is valid (trustworthy).
The verified predicate was: `x == 0'.
-Assertion at line 4 in function main is invalid (trustable).
+Assertion in file first.i at line 4 in function main is invalid (trustworthy).
The verified predicate was: `x == 1'.
\end{shell}
@@ -716,16 +714,16 @@ Abort
Whenever option \longopt{libc-replacements} of \eacslgcc is set, \eacsl is
able to detect incorrect usage of the following libc functions:
\begin{itemize}
-\item \texttt{memcmp}
-\item \texttt{memcpy}
-\item \texttt{memmove}
-\item \texttt{memset}
-\item \texttt{strcat}
-\item \texttt{strncat}
-\item \texttt{strcmp}
-\item \texttt{strcpy}
-\item \texttt{strncpy}
-\item \texttt{strlen}
+ \item \texttt{memcmp}
+ \item \texttt{memcpy}
+ \item \texttt{memmove}
+ \item \texttt{memset}
+ \item \texttt{strcat}
+ \item \texttt{strncat}
+ \item \texttt{strcmp}
+ \item \texttt{strcpy}
+ \item \texttt{strncpy}
+ \item \texttt{strlen}
\end{itemize}
For instance, the program below incorrectly uses \texttt{strcpy} because the
@@ -774,12 +772,13 @@ The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
-<skip preprocessing command line>
+[kernel] Parsing no_main.i (no preprocessing)
[e-acsl] beginning translation.
-[e-acsl] warning: cannot find entry point `main'.
- Please use option `-main' for specifying a valid entry point.
- The generated program may miss memory instrumentation.
- if there are memory-related annotations.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[e-acsl] Warning: cannot find entry point `main'.
+ Please use option `-main' for specifying a valid entry point.
+ The generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
\end{shell}
@@ -817,12 +816,12 @@ The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ e-acsl-gcc.sh -omonitored_no_code.i no_code.c
+[kernel] Parsing no_code.c (with preprocessing)
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `my_pow':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-no_code.c:9:[kernel] warning: No code nor implicit assigns clause for function my_pow,
-generating default assigns from the prototype
+[e-acsl] Warning: annotating undefined function `my_pow':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
\end{shell}
@@ -840,10 +839,11 @@ executable by providing definition of \T{my\_pow}.
\begin{shell}
\$ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i
\$ ./no_code.e-acsl
-Postcondition failed at line 5 in function my_pow.
-The failing predicate is:
-\old(n % 2 == 0) ==> \result >= 1.
-Aborted
+no_code.c: In function 'my_pow'
+no_code.c:5: Error: Postcondition failed:
+ The failing predicate is:
+ even: \result >= 1.
+Aborted (core dumped)
\end{shell}
The execution of the corresponding binary fails at runtime: actually, our
@@ -896,21 +896,23 @@ One can ask to not instrument function \texttt{g} (\emph{i.e.} to instrument
only functions \texttt{f} and \texttt{main}) through the following command.
\begin{shell}
\$ e-acsl-gcc.sh \
- -c --oexec-e-acsl partial.out \
- --e-acsl-extra="-e-acsl-instrument=+@all,-g"' \
- partial.i
+ -c --oexec-e-acsl partial.out \
+ --e-acsl-extra="-e-acsl-instrument=+@all,-g" \
+ partial.i
\end{shell}
Therefore, running the generated executable \texttt{partial.out} leads to the
following verdicts.
\begin{shell}
\$ ./partial.out
-warning: no sound verdict (guess: ok) at line 16 (function main).
-The considered predicate is:
-\initialized(&t[1]).
-warning: no sound verdict (guess: FAIL) at line 17 (function main).
-The considered predicate is:
-\initialized(&t[2]).
+partial.i: In function 'main'
+partial.i:16: Warning: no sound verdict for Assertion (guess: ok).
+ the considered predicate is:
+ \initialized(&t[1])
+partial.i: In function 'main'
+partial.i:17: Warning: no sound verdict for Assertion (guess: FAIL).
+ the considered predicate is:
+ \initialized(&t[2])
\end{shell}
First, there is no message for the first assertion about the initialization of
@@ -919,7 +921,7 @@ First, there is no message for the first assertion about the initialization of
the complete instrumentation of functions \texttt{f} and \texttt{main}.
Second, since function \texttt{g} was not instrumented, no sound verdict may be
-provided after executing it. It leads to the printed warnings for the two last
+provided after executing it. It leads to the printed warnings for the last two
assertions. The indicated guesses (\texttt{ok} for the first assertion and
\texttt{FAIL} for the second one) are the verdicts computed by \eacsl. They can
be trusted if and only if the \eacsl instrumentation is not necessary for
@@ -957,15 +959,15 @@ are potential overflows in this case), just do:
\begin{shell}
\$ frama-c -rte combine.i -then -e-acsl -then-last -print
- -ocode monitored_combine.i
-\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.i
-\$ ./combine.
+ -ocode monitored_combine.c
+\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.c
+\$ ./combine.e-acsl
\end{shell}
Automatic assertion generation can also be enabled via \eacslgcc directly via
the following command:
\begin{shell}
-\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all
+\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all combine.i
\end{shell}
Note the use of \eacslgcc \longopt{rte} option which asks \framac to combine
@@ -987,13 +989,13 @@ prove that there is no potential overflow in the previous program, so the \eacsl
plug-in does not generate additional code for checking them if you run the
following command.
\begin{shell}
-\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -then-last -print -ocode monitored_combine.i
+\$ frama-c -rte combine.i -then -eva -then -e-acsl \
+ -then-last -print -ocode monitored_combine.i
\end{shell}
The additional code will be generated with the two following command.
\begin{shell}
-\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -e-acsl-valid -then-last -print -ocode monitored_combine.i
+\$ frama-c -rte combine.i -then -eva -then -e-acsl \
+ -e-acsl-valid -then-last -print -ocode monitored_combine.i
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1014,10 +1016,9 @@ you can pass it using \shortopt{F} switch:
\begin{shell}
\$ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i
-<skip preprocessing commands>
+[kernel] Parsing check.i (no preprocessing)
[e-acsl] beginning translation.
-check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
- Ignoring annotation.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "foobar".
\end{shell}
@@ -1047,21 +1048,21 @@ which information is displayed according to the verbosing level. The level $n$
also displays the information of all the lower levels.
\begin{center}
-\begin{tabular}{|l|l|}
-\hline
-\shortopt{e-acsl-verbose 0}& only warnings and errors\\
-\hline
-\shortopt{e-acsl-verbose 1}& beginning and ending of the translation\\
-\hline
-\shortopt{e-acsl-verbose 2}& different parts of the translation and
- functions-related information\\
-\hline
-\shortopt{e-acsl-verbose 3}& predicates- and statements-related information\\
-\hline
-\shortopt{e-acsl-verbose 4}& terms- and expressions-related information
-\\
-\hline
-\end{tabular}
+ \begin{tabular}{|l|l|}
+ \hline
+ \shortopt{e-acsl-verbose 0} & only warnings and errors \\
+ \hline
+ \shortopt{e-acsl-verbose 1} & beginning and ending of the translation \\
+ \hline
+ \shortopt{e-acsl-verbose 2} & different parts of the translation and
+ functions-related information \\
+ \hline
+ \shortopt{e-acsl-verbose 3} & predicates- and statements-related information \\
+ \hline
+ \shortopt{e-acsl-verbose 4} & terms- and expressions-related information
+ \\
+ \hline
+ \end{tabular}
\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1074,19 +1075,19 @@ The kind of information to display is settable by the option
parts of the translation, as detailed below.
\begin{center}
-\begin{tabular}{|l|l|}
-\hline
-analysis & minimization of the instrumentation for memory-related annotation
-(section~\ref{sec:memory}) \\
-\hline
-duplication & duplication of functions with contracts
-(section~\ref{sec:no-code}) \\
-\hline
-translation & translation of an annotation into \C code\\
-\hline
-typing & minimization of the instrumentation for integers
-(section~\ref{sec:integers}) \\
-\hline
-\end{tabular}
+ \begin{tabular}{|l|l|}
+ \hline
+ analysis & minimization of the instrumentation for memory-related annotation
+ (section~\ref{sec:memory}) \\
+ \hline
+ preparation & duplication of functions with contracts
+ (section~\ref{sec:no-code}) \\
+ \hline
+ translation & translation of an annotation into \C code \\
+ \hline
+ typing & minimization of the instrumentation for integers
+ (section~\ref{sec:integers}) \\
+ \hline
+ \end{tabular}
\end{center}
% >>>
--
GitLab