Skip to content
Snippets Groups Projects
Commit 5bfbc197 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Merge branch 'kostyantyn/feature/manual-0.7' into 'master' 

Updates to E-ACSL user manual prior to 0.7 release

See merge request !99
parents 5940d7f0 0559aec1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 871 additions and 740 deletions
src/plugins/e-acsl/VERSION
+ 1
− 1
View file @ 5bfbc197
0.6+dev
0.7+dev
src/plugins/e-acsl/doc/userman/Makefile
+ 3
− 5
View file @ 5bfbc197
......@@ -2,8 +2,7 @@ MAIN=main
C_CODE=$(wildcard examples/*.[ci])
VERSION_FILE=../../VERSION
FC_VERSION= Magnesium
FC_VERSION= Silicon
EACSL_VERSION= $(shell cat $(VERSION_FILE))
DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
......@@ -11,7 +10,6 @@ DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
provides.tex \
limitations.tex \
changes.tex \
eacslgcc.tex \
$(C_CODE) \
$(VERSION_FILE)
......@@ -30,8 +28,8 @@ include $(EACSL_DIR)/doc/support/MakeLaTeXModern
eacslversion.tex: Makefile
rm -f $@
echo '\\newcommand{\\eacslversion}{$(EACSL_VERSION)\\xspace}' > $@
echo '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}' >> $@
printf '\\newcommand{\\eacslversion}{$(EACSL_VERSION)\\xspace}\n' > $@
printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
chmod a-w $@
%.1: %.mp
......
src/plugins/e-acsl/doc/userman/biblio.bib
+ 45
− 71
View file @ 5bfbc197
@manual{userman,
title = {Frama-C User Manual},
author = {Loc Correnson and Pascal Cuoq and Florent Kirchner and
Armand Puccetti and Virgile Prevosto and Julien Signoles and
author = {Loc Correnson and Pascal Cuoq and Florent Kirchner and
Andr Maroneze and Virgile Prevosto and
Armand Puccetti and Julien Signoles and
Boris Yakobowski},
year = apr,
month = may,
note = {\url{http://frama-c.cea.fr/download/user-manual.pdf}}
}
......@@ -12,16 +11,14 @@
author = {Julien Signoles and Loc Correnson and Matthieu Lemerre and
Virgile Prevosto},
title = {{Frama-C Plug-in Development Guide}},
year = 2013,
month = apr,
note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
}
@manual{value,
author = {Pascal Cuoq and Boris Yakobowski and Virgile Prevosto},
title = {{Frama-C}'s value analysis plug-in},
year = 2013,
month = apr,
author = {David B\"uhler and Pascal Cuoq and Boris Yakobowski and
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}}},
}
......@@ -29,35 +26,26 @@
author = {Baudin, Patrick and Filli\^{a}tre, Jean-Christophe and
March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
month = apr,
title = {{ACSL: ANSI/ISO C Specification Language. Version 1.8}},
year = {2014}
title = {{ACSL: ANSI/ISO C Specification Language.}},
}
@manual{acsl-implem,
author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe
and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
month = mar,
title = {ACSL: ANSI/ISO C Specification Language. Version 1.9 ---
Frama-C Neon implementation.},
year = {2015}
title = {ACSL: ANSI/ISO C Specification Language. ---
Frama-C Silicon implementation.},
}
@manual{eacsl,
author = {Julien Signoles},
title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.9},
year = 2015,
month = jun,
title = {E-ACSL: Executable ANSI/ISO C Specification Language.},
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
}
@manual{eacsl-implem,
author = {Julien Signoles},
title = {E-ACSL Version 1.9.
Implementation in Frama-C Plug-in E-ACSL version 0.5},
year = 2015,
month = jun,
title = {E-ACSL. Implementation in Frama-C Plug-in E-ACSL},
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
}
......@@ -85,56 +73,29 @@
month = sep,
}
@misc{slicing,
author = {Patrick Baudin and Anne Pacalet},
title = {Slicing plug-in},
note = {\mbox{\url{http://frama-c.com/slicing.html}}},
}
@manual{wp,
author = {Loc Correnson and Zaynah Dargaye and Anne Pacalet},
author = {Patrick Baudin and Franois Bobot and Loc Correnson
and Zaynah Dargaye},
title = {{Frama-C}'s {WP} plug-in},
year = 2013,
month = apr,
note = {\mbox{\url{http://frama-c.com/download/frama-c-wp-manual.pdf}}},
}
@manual{rte,
author = {Philippe Herrmann and Julien Signoles},
title = {Annotation Generation: {Frama-C}'s {RTE} plug-in},
year = 2013,
month = apr,
note = {\mbox{\url{http://frama-c.com/download/frama-c-rte-manual.pdf}}},
}
@inproceedings{fmics12,
author = {Loc Correnson and Julien Signoles},
title = {{Combining Analysis for C Program Verification}},
booktitle = {{Formal Methods for Industrial Critical Systems (FMICS)}},
year = 2012,
month = August,
}
@inproceedings{sefm12,
author = {Pascal Cuoq and Florent Kirchner and Nikolai Kosmatov and Virgile
Prevosto and Julien Signoles and Boris Yakobowski},
title = {{Frama-C, A software Analysis Perspective}},
booktitle = {{Software Engineering and Formal Methods (SEFM)}},
year = 2012,
month = oct,
}
@article{fac15,
year={2015},
month={jan},
journal={Formal Aspects of Computing},
title={{Frama-C: A Software Analysis Perspective}},
publisher={Springer London},
publisher={Springer},
keywords={Formal verification; Static analysis; Dynamic analysis; C},
author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and
Signoles, Julien and Yakobowski, Boris},
pages={1-37},
note={Extended version of \cite{sefm12}},
}
@article{runtime-assertion-checking,
......@@ -149,24 +110,18 @@ note={Extended version of \cite{sefm12}},
pages = {25-37},
}
@article{rv13,
@inproceedings{rv13,
author = {Nikola Kosmatov and Guillaume Petiot and Julien Signoles},
title = {{Optimized Memory Monitoring for Runtime Assertion Checking of C
Programs}},
note = {Submitted for publication},
}
@inproceedings{pathcrawler,
author = {Bernard Botella and Mickal Delahaye and Stphane
Hong-Tuan-Ha and Nikolai Kosmatov and Patricia Mouy
and Muriel Roger and Nicky Williams},
title = {Automating Structural Testing of {C} Programs:
Experience with {PathCrawler}},
booktitle = {the 4th Int. Workshop on Automation
of Software Test {(AST 2009)}},
pages = {70--78},
year = 2009,
publisher = {{IEEE} Computer Society},
title = {An Optimized Memory Monitoring for Runtime Assertion Checking of
{C} Programs},
booktitle = {International Conference on
Runtime Verification ({RV 2013})},
publisher = {Springer},
series = {LNCS},
volume = {8174},
pages = {167--182},
year = 2013,
month = sep,
}
@inproceedings{jfla15,
......@@ -178,3 +133,22 @@ note={Extended version of \cite{sefm12}},
month = jan,
note = {In French},
}
@article{scp16,
title = {{Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring
for C}},
author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
journal = {Science of Computer Programming},
publisher = {Elsevier},
pages = {226-246},
language = {English},
year = {2016},
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},
}
src/plugins/e-acsl/doc/userman/changes.tex
+ 16
− 0
View file @ 5bfbc197
......@@ -5,6 +5,22 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslversion}
\begin{itemize}
\item Removed chapter \textbf{Easy Instrumentation with E-ACSL}.
\item \textbf{What the Plug-in Provides}: added section \textbf{E-ACSL Wrapper
Script}.
\item \textbf{What the Plug-in Provides}: added description of \eacsl runtime
libraries.
\item \textbf{Known Limitations}: added section \textbf{Requirements to Input
Programs}.
\item \textbf{Known Limitations}: added section \textbf{Limitations of E-ACSL Monitoring Libraries}.
\item \textbf{Recursive Functions}: remove limitation about possible uses before
being declared.
\item \textbf{Variadic Functions}: mention the \variadic plug-in.
\end{itemize}
\section*{E-ACSL 0.6}
\begin{itemize}
\item \textbf{Easy Instrumentation with E-ACSL}: new chapter.
\end{itemize}
......
src/plugins/e-acsl/doc/userman/eacslgcc.tex deleted 100644 → 0
+ 0
− 183
View file @ 5940d7f0
\chapter{Easy Instrumentation with \eacsl}
Due to numerous instrumentation and compile-time options generating monitored
executables using the \eacsl plug-in can be tedious. To simplify this task we
developed \eacslgcc\ -- a convenience wrapper around \framac and \gcc allowing
to instrument programs with \eacsl and compile the instrumented code using a
single command and a very few parameters.
In this section we describe \eacslgcc and provide several examples of its use.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Basic Use}
\eacslgcc instruments C files provided at input using the \eacsl plug-in, and
optionally compiles the generated code and the original sources using a \C
compiler (\gcc by default).
The default behaviour of \eacslgcc is to instrument an annotated C program
with runtime assertions via a run of \framac.
\begin{shell}
\$ e-acsl-gcc.sh -ogen.c foo.c
\end{shell}
The above command instruments \texttt{foo.c} with runtime assertions and
outputs the generated code to \texttt{gen.c}. Unless the name of the output
file is specified via the \texttt{-o} option (i.e., \texttt{-ogen.c} in the
above example), the generated code is placed to a file named
\texttt{a.out.frama.c}.
Compilation of the original and the instrumented sources
is enabled using the \texttt{-c} option. For instance, the command
\begin{shell}
\$ e-acsl-gcc.sh -c -ogen.c foo.c
\end{shell}
instruments the code in \texttt{foo.c}, outputs it to \texttt{gen.c} and
produces 2 executables: \texttt{a.out} and \texttt{a.out.e-acsl}, where
\texttt{a.out} is an executable compiled from \texttt{foo.c}, while
\texttt{a.out.e-acsl} is an executable compiled from \texttt{gen.c} generated
by \eacsl.
Named executables can be created using the \texttt{-O} option. This is such
that a value supplied to the \texttt{-O} option is used to name the executable
generated from the original program and the executable generated from the
\eacsl-instrumented code is suffixed \texttt{.e-acsl}.
For example, command
\begin{shell}
\$ e-acsl-gcc.sh -c -ogen.c -Ogen foo.c
\end{shell}
names the executables generated from \texttt{foo.c} and \texttt{gen.c}:
\texttt{gen} and \texttt{gen.e-acsl} respectively.
The \eacslgcc \texttt{-C} option allows to skip the instrumentation step and
compile a given program as if it were already instrumented by the \eacsl
plug-in. This option is useful if one makes changes to an already
instrumented source file by hand and only wants to recompile it.
\begin{shell}
\$ e-acsl-gcc.sh -C -Ogen gen.c
\end{shell}
In the above example the run of \eacslgcc produces a single executable named
\texttt{gen.e-acsl}. This is because \texttt{gen.c} is considered to be
instrumented code and thus no original program is provided.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Documentation}
A list of \eacslgcc options can be retrieved using the following command:
\begin{shell}
\$ e-acsl-gcc.sh -h
Usage: e-acsl-gcc.sh [options] files
Options:
-h show this help page
-c compile instrumented code
-l pass additional options to the linker
-e pass additional options to the pre-preprocessor
-E pass additional arguments to the Frama-C pre-processor
-p output the generated code with rich formatting to STDOUT
-o <file> output the generated code to <file> [a.out.frama.c]
-O <file> output the generated executables to <file> [a.out, a.out.e-acsl]
-M maximize memory-related instrumentation
-g always use GMP integers instead of C integral types
-q suppress any output except for errors and warnings
-s <file> redirect all output to <file>
-P compile executable without debug features
-I <file> specify Frama-C executable [frama-c]
-G <file> specify GCC executable [gcc]
\end{shell}
Note that the \texttt{-h} option lists only the most basic options.
For full up-to-date documentation of \eacslgcc see its man page:
\begin{shell}
\$ man e-acsl-gcc.sh
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Customising \framac and \gcc Invocations}
Runs of \framac and \gcc issued by \eacslgcc can be customized by using
additional flags.
Additional \framac flags can be passed using the \texttt{-F} option, while
\texttt{-l} and \texttt{-e} options allow for passing additional pre-processor
and linker flags during \gcc invocations. For example, command
\begin{shell}
\$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
\end{shell}
yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
are output using the UTF-8 character set. Further, during the compilation of
\texttt{a.out.frama.c} \gcc adds directories \texttt{/bar} and
\texttt{/baz} to the list of directories to be searched for header files.
It is worth mentioning that \eacslgcc implements several convenience flags for
setting some of the \framac options. For instance, \texttt{-E} can be used to
pass additional arguments to the \framac pre-processor and \texttt{-M}
maximizes memory-related instrumentation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Verbosity Levels and Output Redirection}
By default \eacslgcc prints the executed \framac and \gcc commands and pipes
their output to the terminal. The verbosity of \framac output can be changed
using \texttt{-v} and \texttt{-d} options used to pass values to
\texttt{-verbose} and \texttt{-debug} flags of \framac respectively. For
instance, to increase the verbosity of plug-ins but suppress the verbosity of
the \framac kernel while instrumenting \texttt{foo.c} one can use the following
command:
\begin{shell}
\$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
\end{shell}
Verbosity of the \eacslgcc output can also be reduced using the \texttt{-q}
option that suppresses any output except errors or warnings issued by \gcc,
\framac or \eacslgcc itself.
The output of \eacslgcc can also be redirected to a specified file using the
\texttt{-s} option. For example, the following command redirects all
output during instrumentation and compilation of \texttt{foo.c} to the
file named \texttt{/tmp/log}.
\begin{shell}
\$ e-acsl-gcc.sh -c -s/tmp/log foo.c
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Executables}
By default \eacslgcc uses the first \texttt{frama-c} executable found in a
system's path to instrument input programs. The name of the \framac executable
can be changed using the \texttt{-I} option. For instance, to instrument a file
named \texttt{foo.c} using the \texttt{/usr/local/bin/frama-c.byte} executable
one can use the following command:
\begin{shell}
\$ e-acsl-gcc.sh -I/usr/local/bin/frama-c.byte foo.c
\end{shell}
The name of a \gcc executable can be changed similarly using the \texttt{-G}
option.
src/plugins/e-acsl/doc/userman/examples/assert_sign.c 0 → 100644
+ 2
− 0
View file @ 5bfbc197
void __e_acsl_assert(int pred, char *kind,
char *func_name, char *pred_text, int line);
src/plugins/e-acsl/doc/userman/examples/instrumented_first.i 0 → 100644
+ 61
− 0
View file @ 5bfbc197
\begin{shell}
\$ frama-c -e-acsl first.i -then-last -print
[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.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
typedef unsigned int size_t;
struct __e_acsl_mpz_struct {
int _mp_alloc ;
int _mp_size ;
unsigned long *_mp_d ;
};
typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
/*@ requires pred != 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred,
char *kind,
char *fct,
char *pred_txt,
int line);
/*@ ghost extern int __e_acsl_init; */
/*@ ghost extern int __e_acsl_internal_heap; */
extern size_t __e_acsl_heap_allocation_size;
int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
}
*/
/*@
predicate diffSize{L1, L2}(integer i) =
\at(__e_acsl_heap_allocation_size,L1) -
\at(__e_acsl_heap_allocation_size,L2) == i;
*/
int main(void)
{
int __retres;
int x;
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);
__retres = 0;
return __retres;
}
\end{shell}
src/plugins/e-acsl/doc/userman/examples/modified_main.c
+ 1
− 7
View file @ 5bfbc197
extern void e_acsl_global_init(void);
extern void __clean(void);
extern void f(void);
int main(void) {
e_acsl_global_init();
int main(int argc, char **argv) {
f();
__clean();
return 0;
}
src/plugins/e-acsl/doc/userman/examples/my_assert.c
+ 3
− 7
View file @ 5bfbc197
#include "stdio.h"
void e_acsl_assert(int predicate,
char *kind,
char *fct,
char *pred_txt,
int line)
{
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.\n\
The verified predicate was: `%s'.\n",
kind, line, fct, predicate ? "valid" : "invalid", pred_txt);
kind, line, func_name, pred ? "valid" : "invalid", pred_text);
}
src/plugins/e-acsl/doc/userman/examples/no_main.i
+ 3
− 1
View file @ 5bfbc197
......@@ -3,7 +3,7 @@
@ ensures \result >= 1;
@ behavior odd:
@ assumes n % 2 != 0;
@ \result >= 1; */
@ ensures \result >= 1; */
unsigned long long my_pow(unsigned int x, unsigned int n) {
unsigned long long res = 1;
while (n) {
......@@ -13,3 +13,5 @@ unsigned long long my_pow(unsigned int x, unsigned int n) {
}
return res;
}
src/plugins/e-acsl/doc/userman/examples/rte_debug.i 0 → 100644
+ 16
− 0
View file @ 5bfbc197
void foo(int *p) {
/*@assert \valid(p); */
*p = 1;
}
void bar(int *p) {
foo(p);
}
int main(void) {
int i = 0;
int *p = &i;
bar(p+1);
return 0;
}
src/plugins/e-acsl/doc/userman/introduction.tex
+ 29
− 26
View file @ 5bfbc197
\chapter{Introduction}
\framac~\cite{userman,sefm12,fac15} is a modular analysis framework for the C
language which supports the ACSL specification language~\cite{acsl}. This manual
documents the \eacsl plug-in of \framac, version \eacslversion. The \eacsl
version you are using is indicated by the command \texttt{frama-c
-e-acsl-version}\optionidx{-}{e-acsl-version}. This plug-in automatically
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 as the one of the original program.
\framac~\cite{userman,fac15} is a modular analysis framework for the C
programming language which supports the ACSL specification
language~\cite{acsl}. This manual documents the \eacsl plug-in of \framac,
version \eacslversion. The \eacsl version you are using is indicated by the
command \texttt{frama-c -e-acsl-version}\optionidx{-}{e-acsl-version}. \eacsl
automatically 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 as 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
\eacsl translation brings several benefits. First, it allows a user to monitor
\C code and perform what is usually referred to as ``runtime assertion
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
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 analyzers for \C like
\pathcrawler~\cite{pathcrawler} that do not natively understand the \acsl
annotation checking'' would be more precise.}. This is the
primary goal of \eacsl. 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 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 assertions that
cannot be verified statically at runtime and thus to establish a link between
monitoring tools and static analysis tools like
cannot be verified statically and thus to establish a link between
runtime monitoring and static analysis tools such as
\valueplugin~\cite{value}\index{Value} or \wpplugin~\cite{wp}\index{Wp}.
Annotations must be written in the \eacsl specification
language~\cite{eacsl,sac13} which is a subset of \acsl. This plug-in is still in
a preliminary state: some parts of \eacsl are not yet supported. \eacsl
annotations currently handled by the \eacsl plug-in are documented in a
separated document~\cite{eacsl-implem}.
Annotations used by the plug-in must be written in the \eacsl specification
language~\cite{eacsl,sac13} -- a subset of \acsl. \eacsl plug-in is still in a
preliminary state: some parts of the \eacsl specification language are not yet
supported. Annotation supported by the plugin are described in a separate
document~\cite{eacsl-implem}.
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} Also this manual is \emph{not} a full tutorial
about \framac and \eacsl, even if it provides some examples. You can still refer
to any external tutorial~\cite{rv13tutorial} for additional examples.
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
\framac or \eacsl.
% You can still refer to any external
% tutorial~\cite{rv13tutorial} for additional examples.
src/plugins/e-acsl/doc/userman/limitations.tex
+ 69
− 35
View file @ 5bfbc197
\chapter{Known Limitations}
The development of the \eacsl plug-in is still ongoing. First, the \eacsl
reference manual~\cite{eacsl} is not yet fully supported. Which annotations are
already translated into \C code and which are not is defined in a separated
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 (see Chapter 10 of the \framac User Manual~\cite{userman}). Third, there
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}
......@@ -24,17 +25,16 @@ been written.
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 caught by the \eacsl plug-in. That is not
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}
\$ frama-c -e-acsl uninitialized.i -then-on e-acsl -print \
-ocode monitored_uninitialized.i
\$ gcc -Wuninitialized -o pointer `frama-c -print-share-path`/e-acsl/e_acsl.c` \
monitored_uninitialized.i
\$ 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\
monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function
[-Wuninitialized]
\$ ./monitored_uninitialized
\$ ./monitored_uninitialized.e-acsl
\end{shell}
This is more a design choice than a limitation: should the \eacsl plug-in
......@@ -61,9 +61,10 @@ plug-in is running (see examples of Sections~\ref{sec:no-main} and
\label{sec:limits:no-main}
The instrumentation in the generated program is partial for every program
without main containing a memory-related annotations, except if the option
\optionuse{-}{e-acsl-full-mmodel} is provided. In that case, violations of such
annotations are undetected.
without main containing memory-related annotations, except if the option
\optionuse{-}{e-acsl-full-mmodel} or the \eacsl plug-in (of \shortopt{M} option
of \eacslgcc) is provided. In that case, violations of such annotations are
undetected.
Consider the following example.
......@@ -72,24 +73,26 @@ Consider the following example.
You can generate the instrumented program as follows.
\begin{shell}
\$ frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl valid_no_main.c \
-then-on e-acsl -print -ocode monitored_valid_no_main.i
\$ e-acsl-gcc.sh -ML -omonitored_valid_no_main.i valid_no_main.c
<skip preprocessing commands>
[e-acsl] beginning translation.
<skip warnings about annotations from the Frama-C libc
which cannot be translated>
<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' and `__e_acsl_memeory_clean' by yourself.
you must call function `__e_acsl_memory_init' 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 a \texttt{main} function, then this main function must
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}
\index{e\_acsl\_memory\_init@\texttt{\_\_e\_acsl\_memory\_init}} at the very
beginning and a call to the function \texttt{\_\_e\_acsl\_memory\_clean}
\index{e\_acsl\_memory\_clean@\texttt{\_\_e\_acsl\_memory\_clean}} at the very
end like in the following example.
beginning. This function plays a very important role: it initializes metadata
storage used for tracking of memory blocks. Unless this call is inserted the
run of a modified program is likely to fail.
While it is possible to add such intrumentation manually we recommend using
\eacslgcc. Consider the following incomplete program containing \T{main}:
\listingname{modified\_main.c}
\cinput{examples/modified_main.c}
......@@ -97,14 +100,13 @@ end like in the following example.
Then just compile and run it as explained in Section~\ref{sec:memory}.
\begin{shell}
\$ DIR=`frama-c -print-share-path`/e-acsl
\$ MDIR=\$DIR/memory_model
\$ gcc -o valid_no_main \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \
\$MDIR/e_acsl_mmodel.c monitored_valid_no_main.i modified_main.c
\$ ./valid_no_main
\$ 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.
The failing predicate is:
freed: \valid(x).
Aborted
\end{shell}
Also, if the unprovided main initializes some variables, running the
......@@ -123,7 +125,7 @@ $f$ such that:
\item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
\item or $a$ is one of the post-conditions of $f$.
\end{itemize}
A Violation of such an annotation $a$ is undetected. There is no workaround yet.
A violation of such an annotation $a$ is undetected. There is no workaround yet.
Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
undefined functions. There is also no workaround yet.
......@@ -135,19 +137,51 @@ Programs containing recursive functions have the same limitations as the ones
containing undefined functions (Section~\ref{sec:limits:no-code}) and
memory-related annotations.
Also, even though there is no such annotations, the generated code may call a
function before it is declared. When this behavior appears remains
unspecifed. The generated code is however easy to fix by hand.
%% JS: this issue should have been fixed:
%% Also, even though there is no such annotations, the generated code may call a
%% function before it is declared. When this behavior appears remains
%% unspecifed. The generated code is however easy to fix by hand.
\section{Variadic Functions}
\index{Function!Variadic}
Programs containing variadic undefined functions but with a function contract
are not yet supported. There is no workaround yet.
Programs containing undefined variadic functions with contracts
are not yet supported. Using the \variadic plug-in of \framac could be a
solution in some cases, but its generated code cannot always be compiled.
\section{Function Pointers}
\index{Function!Pointer}
Programs containing function pointers have the same limitations on
memory-related annotations as the ones containing undefined function or
recursive functions.
memory-related annotations as the ones containing undefined or recursive
functions.
\section{Requirements to Input Programs}
\index{Function!Input}
\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
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.
\subsection{Memory Management Functions}
Programs providing custom definitions of \T{syscall}, \T{mmap} or
\T{sbrk} should be rejected. Also, an input programs should not modify
memory-management functions namely \T{malloc}, \T{calloc}, \T{realloc},
\T{free}, \T{cfree}, \T{posix\_memalign} and \T{aligned\_alloc}. \eacsl relies
on these functions in order to track heap memory. Further, correct heap memory
monitoring requires to limit allocation and deallocation of heap memory to
POSIX-compliant memory management functions
listed above. Monitoring of programs that allocate memory using non-standard or
obsolete functions (e.g., \T{valloc}, \T{memalign}, \T{pvalloc}) may not work
correctly.
\section{Limitations of E-ACSL Monitoring Libraries}
\index{Function!Libraries}
\eacsl monitoring library implementing segment-based memory model is fairly
recent and presently has very limited support for 32-bit architectures. When
using a 32-bit machine we recommend using the bittree-based memory model
instead.
src/plugins/e-acsl/doc/userman/macros.tex
+ 8
− 0
View file @ 5bfbc197
......@@ -12,10 +12,12 @@
\newcommand{\C}{\textsc{C}\xspace}
\newcommand{\jml}{\textsc{JML}\xspace}
\newcommand{\valueplugin}{\textsc{Value}\xspace}
\newcommand{\variadic}{\textsc{Variadic}\xspace}
\newcommand{\wpplugin}{\textsc{Wp}\xspace}
\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
\newcommand{\gcc}{\textsc{Gcc}\xspace}
\newcommand{\gmp}{\textsc{GMP}\xspace}
\newcommand{\jemalloc}{\textsc{Jemalloc}\xspace}
\newcommand{\nodiff}{\emph{No difference with \acsl.}}
\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
......@@ -276,6 +278,12 @@
\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
\newcommand{\shortopt}[1]{\optionuse{-}{#1}}
\newcommand{\longopt}[1]{\optionuse{{-}{-}}{#1}}
% Shortcuts for truetype, italic and bold
\newcommand{\T}[1]{\texttt{#1}}
\newcommand{\I}[1]{\textit{#1}}
\newcommand{\B}[1]{\textbf{#1}}
\definecolor{gris}{gray}{0.85}
\makeatletter
......
src/plugins/e-acsl/doc/userman/main.tex
+ 7
− 8
View file @ 5bfbc197
......@@ -17,7 +17,7 @@
\includegraphics[height=14mm]{cealistlogo.jpg}
\end{flushleft}
\vfill
\title{\eacsl Plug-in}{Release \eacslversion compatible
\title{\eacsl Plug-in}{Release \eacslversion compatible
with \framac \fcversion}
\author{Julien Signoles and Kostyantyn Vorobyov}
\begin{tabular}{l}
......@@ -40,15 +40,15 @@ 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 contents of this document
correspond to its version \eacslversion (\today) compatible with the version
\fcversion of \framac~\cite{userman,sefm12,fac15}. However the development of
the \eacsl plug-in is still ongoing: features described here may still evolve in
the future.
\eacsl\footnote{\url{https://frama-c.com/eacsl.html}}. The contents of this
document correspond to its version \eacslversion (January 2017) 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.
\section*{Acknowledgements}
We gratefully thank all the people who contributed to this document:
We gratefully thank the people who contributed to this document:
Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola Kosmatov and
Guillaume Petiot.
......@@ -56,7 +56,6 @@ Guillaume Petiot.
\include{introduction}
\include{provides}
\include{eacslgcc}
\include{limitations}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
src/plugins/e-acsl/doc/userman/provides.tex
+ 606
− 394
View file @ 5bfbc197
\chapter{What the Plug-in Provides}
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 toy example and how
to compile the generated code with a standard \C compiler and 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 are not defined or in which there are no
main function. Section~\ref{sec:combine} explains how to combine the \eacsl
plug-in with other \framac plug-ins. Finally, Section~\ref{sec:custom}
introduces how to customize the plug-in, and Section~\ref{sec:verbose} details
the verbosing policy of the plug-in.
This chapter is the core of this manual and describes how to use the \eacsl
plug-in.
% You can still call the option \shortopt{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 toy example,
compile the generated code with the \gcc compiler and detect invalid
annotations at runtime. Further, Section~\ref{sec:wrapper} describes \eacslgcc\
-- a convenience wrapper script around \framac and \gcc. The aim of this script
is to simplify instrumentation and compilation of the instrumented code.
Section~\ref{sec:exec-env} gives 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 are not defined or in
which there are no main function. Section~\ref{sec:combine} explains how to
combine the \eacsl plug-in with other \framac plug-ins. Finally,
Section~\ref{sec:custom} introduces how to customize the plug-in, and
Section~\ref{sec:verbose} details the verbosing policy of the plug-in.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Simple Example}
\section{Simple Example} % <<<
\label{sec:simple}
This Section is a mini-tutorial which explains from scratch how to use the
\eacsl plug-in to detect at runtime that an \eacsl annotation is violated.
This section is a mini-tutorial which explains from scratch how to use the
\eacsl plug-in to detect whether an \eacsl annotation is violated at runtime.
% All tool invocations and code listings shown in this section assume a Linux
% distribution with system-wide \framac installation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Running \eacsl}
\label{sec:run}
Consider the following simple program in which the first assertion is valid
while the second one is not.
Consider the following program containing two \eacsl assertions such that
the first assertion is valid, whereas the second one is not.
\listingname{first.i}
\cinput{examples/first.i}
Running \eacsl on this file just consists in adding the option
\optiondef{-}{e-acsl} to the \framac command line:
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_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.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>
[e-acsl] translation done in project "e-acsl".
\end{shell}
Even if \texttt{first.i} is already preprocessed, \eacsl first asks the \framac
kernel to preprocess and to link against \texttt{first.i} several files which
form the \eacsl library. Their usage will be explained later, mainly in
Section~\ref{sec:exec-env}.
Then \eacsl takes the annotated \C code as input and 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. This is also
possible through the command line thanks to the kernel options
\optionuse{-}{then-last} and \optionuse{-}{print} which respectively switch to
the last generated project and pretty prints the \C code~\cite{userman}:
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
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
switches to the last generated project, while the latter pretty prints the \C
code~\cite{userman}:
\begin{shell}
\$ frama-c -e-acsl first.i -then-last -print
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
int _mp_size ;
unsigned long *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
/*@ requires predicate != 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *kind,
char *fct,
char *pred_txt,
int line);
/*@
model __mpz_struct { integer n };
*/
int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__); */
/*@
axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
}
*/
/*@ ghost extern int __e_acsl_init; */
/*@ ghost extern int __e_acsl_internal_heap; */
extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(integer i) =
\at(__memory_size,L1)-\at(__memory_size,L2) == i;
*/
int main(void)
{
int __retres;
int x;
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);
__retres = 0;
return __retres;
}
\end{shell}
\input{examples/instrumented_first.i}
As you can see, the generated code contains additional type declarations,
constant declarations and global \acsl annotations that are not in the initial
file \texttt{first.i}. They are part of the included \eacsl monitoring
library. You can safely ignore it right now. The translated \texttt{main}
function of \texttt{first.i} is displayed at the end. After each \eacsl
annotation, a line has been added.
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,
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);
__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 == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
\end{ccode}
\end{minipage}
They are function calls to \texttt{e\_acsl\_assert}\codeidx{e\_acsl\_assert}
which is defined in the \eacsl library. Each call performs the dynamic
verification that the corresponding assertion is valid. More precisely, it
checks that its first argument (here \texttt{x == 0} or \texttt{x == 1}) is not
equal to 0 and fails otherwise. The extra arguments are only used to display
precise error reports as shown in Section~\ref{sec:exec}.
Each call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert}, function
defined by the \eacsl monitoring library, dynamically verifies the validity of
the corresponding assertion. In other words, it checks that its first argument
(here \texttt{x == 0} or \texttt{x == 1}) is not equal to 0 and fails
otherwise. The extra arguments are used to display error reports as shown in
Section~\ref{sec:exec}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Executing the generated code}
\label{sec:exec}
By using the option \optionuse{-}{ocode} of \framac~\cite{userman}, we can
redirect the generated code into a \C file as follow.
Using \shortopt{ocode} \framac~\cite{userman} option, the code generated by the
\eacsl plug-in can be redirected into a file as follows:
\begin{shell}
\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.i
\end{shell}
Then it may be executed by a standard \C compiler like \gcc in the following
way.
\framac uses architecture-dependent configuration which
affects sizes of integer types, endianness and potentially other features. It
can be seen that the code generated from \texttt{first.i} (shown in the
previous section) defines \C type \texttt{size\_t} as \texttt{unsigned int}, whereas
in 64-bit architectures \texttt{size\_t} is typically defined as
\texttt{unsigned long}. Architecture used during \framac translation is
controlled through \framac \shortopt{machdep} option that specifies the
architecture type to use during translation. The default value of
\shortopt{machdep} is \texttt{x86\_32} (a generic 32-bit x86 architecture).
Note that since code generated by \eacsl is aimed at being compiled it is
important that the architecture used by \framac matches the architecture
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.i
\end{shell}
An executable checking the validity of annotations in \texttt{first.i} at
runtime can be generated using a \C compiler (for instance \gcc), as follows:
\lstset{escapechar=£}
\begin{shell}
\$ gcc -o monitored_first `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_first.i
In file included from <file_path>/e_acsl.c:23:0:
<file_path>/e_acsl.h:41:3: warning: `FC_BUILTIN' attribute directive ignored [-Wattributes]
monitored_first.i:8:1: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
monitored_first.i:16:60: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
monitored_first.i:21:1: warning: `__FRAMA_C_MODEL__' attribute directive ignored [-Wattributes]
\end{shell}
You may notice that the generated file \texttt{monitored\_first.i} is linked
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 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
\optionuse{-}{Wno-attributes} to \gcc if you do not want to be polluted by these
warnings.
\$ gcc monitored_first.i -omonitored_first -leacsl-rtl-bittree -lpthread -lm
monitored_first.i:9:1: warning: '__FC_BUILTIN__' attribute directive ignored [-Wattributes]
typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
^
monitored_first.i:16:62: warning: '__FC_BUILTIN__' attribute directive ignored [-Wattributes]
int line);
^
monitored_first.i:24:1: warning: '__FRAMA_C_MODEL__' attribute directive ignored [-Wattributes]
int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
\end{shell}
The displayed warnings can be safely ignored as they refer to the attribute
\texttt{FC\_BUILTIN} used internally by \framac. The warnings can be suppressed
using \shortopt{Wno-attributes} \gcc option. You may also notice that the
generated executable (\texttt{monitored\_first}) is linked against the \eacsl
static library (i.e., via \texttt{-leacsl-rtl-bittree}) installed alongside the
\eacsl plug-in. This library provides definitions of the functions used by
\eacsl during its runtime analysis.
We describe libraries used by \eacsl later on in Section~\ref{sec:memory}.
Finally you can execute the generated binary.
\begin{shell}
......@@ -192,20 +152,217 @@ Finally you can execute the generated binary.
Assertion failed at line 4 in function main.
The failing predicate is:
x == 1.
Aborted
\$ echo \$?
1
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
annotation holds for this execution.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{\eacsl Wrapper Script} % <<<
\label{sec:wrapper}
You may have noticed that generating executables using a combination of
\framac, \eacsl and \gcc may be tedious. To simplify this process we developed
\eacslgcc\ -- a convenience wrapper around \framac and \gcc allowing to
instrument and compile instrumented code using a single command and a few
parameters.
\begin{important}\index{Gcc}
Presently, \eacslgcc is a recommended way of running the \eacsl plug-in.
This manual further describes features of the \eacsl plug-in using \eacslgcc
as its main driver for source code instrumentation and compilation of the
instrumented programs.
\end{important}
In this section we describe \eacslgcc and provide several examples of its use.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Standard Usage}
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
\end{shell}
The above command instruments \texttt{first.i} with runtime assertions and
outputs the generated code to \texttt{monitored\_first.i}. Unless the name of
the output file is specified via the \shortopt{o} option (i.e.,
\shortopt{-omonitored\_first.i} in the above example), the generated
code is placed to a file named \texttt{a.out.frama.c}.
Compilation of the original and the instrumented sources
is enabled using the \shortopt{c} option. For instance, command
\begin{shell}
\$ e-acsl-gcc.sh -c -omonitored_first.i first.i
\end{shell}
instruments the code in \texttt{first.i}, outputs it to
\texttt{monitored\_first.i} and produces 2 executables: \texttt{a.out} and
\texttt{a.out.e-acsl}, such that \texttt{a.out} is an executable compiled from
\texttt{first.i}, while \texttt{a.out.e-acsl} is an executable compiled from
\texttt{monitored\_first.i} generated by \eacsl.
Named executables can be created using the \shortopt{O} option. This is such
that a value supplied to the \shortopt{O} option is used to name the executable
generated from the original program and the executable generated from the
\eacsl-instrumented code is suffixed \texttt{.e-acsl}.
For example, command
\begin{shell}
\$ e-acsl-gcc.sh -c -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
\texttt{monitored\_first.e-acsl} respectively.
The \eacslgcc \shortopt{C} option allows to skip the instrumentation step and
compile a given program as if it was already instrumented by the \eacsl
plug-in. This option is useful if one makes changes to an already
instrumented source file by hand and only wants to recompile it.
\begin{shell}
\$ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i
\end{shell}
This execution stops with exit code 1 and an error message indicating which
invalid \eacsl annotation has been violated. There is no output for the valid
\eacsl annotation. So, thanks to the plug-in, we detect that the second
assertion in the initial program is wrong, while the first one is correct for
this execution.
The above command generates a single executable named
\texttt{monitored\_first.e-acsl}. This is because \texttt{monitored\_first.i} is
considered to be instrumented code and thus no original program is provided.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Customising \framac and \gcc Invocations}
By default \eacslgcc uses \T{frama-c} and \T{gcc} executables by looking them
up in a system's path. If either of the tools are not found the script fails
with an appropriate error message. Paths to \framac and \gcc executables can
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
\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
pre-processor and linker flags during \gcc invocations. For example, command
\begin{shell}
\$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
\end{shell}
yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
are output using the UTF-8 character set. Further, during the compilation of
\texttt{a.out.frama.c} \gcc adds directories \texttt{/bar} and
\texttt{/baz} to the list of directories to be searched for header files.
It is worth mentioning that \eacslgcc implements several convenience flags for
setting some of the \framac options. For instance, \shortopt{E} can be used to
pass additional arguments to the \framac pre-processor (see
Section~\ref{sec:eacsl-gcc:doc}).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Verbosity Levels and Output Redirection}
By default \eacslgcc prints the executed \framac and \gcc commands and pipes
their output to the terminal. The verbosity of \framac output can be changed
using \shortopt{v} and \shortopt{d} options used to pass values to
\shortopt{verbose} and \shortopt{debug} flags of \framac respectively. For
instance, to increase the verbosity of plug-ins but suppress the verbosity of
the \framac kernel while instrumenting \texttt{foo.c} one can use the following
command:
\begin{shell}
\$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
\end{shell}
Verbosity of the \eacslgcc output can also be reduced using the \shortopt{q}
option that suppresses any output except errors or warnings issued by \gcc,
\framac, and \eacslgcc itself.
The output of \eacslgcc can also be redirected to a specified file using the
\shortopt{s} option. For example, the following command redirects all
output during instrumentation and compilation of \texttt{foo.c} to the
file named \texttt{/tmp/log}.
\begin{shell}
\$ e-acsl-gcc.sh -c -s/tmp/log foo.c
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Architecture Dependency}
As pointed out in Section~\ref{sec:exec} the execution of a \C program depends
on the underlying machine architecture it is executed on. The program must be
compiled on the very same architecture (or cross-compiled for it) for the
compiler being able to generate a correct binary.
\framac makes assumptions about the machine architecture when analyzing source
code. By default, it assumes an X86 32-bit platform, but it can be customized
through \shortopt{machdep} switch~\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 architecture which the generated code will be
executed on, otherwise the generated program is likely to fail to link against
the \eacsl library. Note that the library is built using the default
machine architecture.
One of the benefits of using the wrapper script is that it makes sure that
\framac is invoked with the correct \shortopt{machdep} option. By default
\eacslgcc uses \shortopt{machdep gcc\_x86\_64} for 64-bit architectures and
\shortopt{machdep gcc\_x86\_32} for 32-bit ones. Compiler invocations are
further passed \shortopt{m64} or \shortopt{m32} options to generate code using
64-bit or 32-bit ABI respectively.
\section{Execution Environment of the Generated Code}
At the present stage of implementation \eacsl does not support generating
executables with ABI different to the default one.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Documentation}\label{sec:eacsl-gcc:doc}
For full up-to-date documentation of \eacslgcc see its man page:
\begin{shell}
\$ man e-acsl-gcc.sh
\end{shell}
A brief listing of the basic options of \eacslgcc
can be viewed using its \shortopt{h} option:
\begin{shell}
\$ e-acsl-gcc.sh -h
e-acsl-gcc.sh - instrument and compile C files with E-ACSL
Usage: e-acsl-gcc.sh [options] files
Options:
-h show this help page
-c compile instrumented code
-l pass additional options to the linker
-e pass additional options to the prepreprocessor
-E pass additional arguments to the Frama-C preprocessor
-p output the generated code to STDOUT
-o <file> output the generated code to <file> [a.out.frama.c]
-O <file> output the generated executables to <file> [a.out, a.out.e-acsl]
-M maximize memory-related instrumentation
-g always use GMP integers instead of C integral types
-q suppress any output except for errors and warnings
-s <file> redirect all output to <file>
-I <file> specify Frama-C executable [frama-c]
-G <file> specify C compiler executable [gcc]
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{Execution Environment of the Generated Code} %<<<
\label{sec:exec-env}
The environment in which the code is executed is not necessarily the same as
......@@ -221,13 +378,14 @@ plug-in offers a few possibilities of customization.
The major difference between \acsl~\cite{acsl} and \eacsl~\cite{eacsl}
specification languages is that the logic is total in the former while it is
partial in the latter one: the semantics of a term denoting a \C expression $e$
partial in the latter one: the semantics of a logic construct $c$ denoting a \C
expression $e$
is undefined if $e$ leads to a runtime error and, consequently, the semantics of
any term $t$ (resp. predicate $p$) containing such an expression $e$ is
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
......@@ -238,113 +396,66 @@ Consider for instance the following annotated program.
\listingname{rte.i}
\cinput{examples/rte.i}
The terms and predicates containing the modulo `\%' in the \texttt{assumes}
clause are undefined in the context of the \texttt{main} function call since
the second argument is equal to 0.
However we can generate an instrumented code and compile it through the
following command lines:
The terms and predicates containing the modulo `\%' in the \T{assumes} clause
are undefined in the context of the \T{main} function call since the second
argument is equal to 0. However, we can generate an instrumented code and
compile it using the following command:
\begin{shell}
\$ frama-c -e-acsl rte.i -then-last -print -ocode monitored_rte.i
\$ gcc -o rte `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_rte.i
\$ e-acsl-gcc.sh -c -omonitored_rte.i -Orte rte.i
\end{shell}
Now, when \texttt{rte} is executed, you get the following output indicating that
your function contract is invalid because it contains a division by zero.
Now, when \T{rte.e-acsl} is executed, you get the following output indicating
that your function contract is invalid because it contains a division by zero.
\begin{shell}
\$ ./rte
RTE failed at line 5 in function divide.
\$ ./rte.e-acsl
RTE failed at line 5 in function is_dividable.
The failing predicate is:
division_by_zero: y != 0.
Aborted
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Architecture Dependent Annotations}\label{sec:architecture}
In many cases, the execution of a \C program depends on the underlying machine
architecture it is executed on. The program must be compiled on the very same
architecture (or cross-compiled for it) 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 an X86 32-bit platform, but it may be customized
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 architecture which the generated code will be
executed on if the code \emph{or the annotation} is machine dependent.
Consider for instance the following program.
\listingname{archi.c}
\cinput{examples/archi.c}
We can generate an instrumented code and compile it through the
following command lines (the option \optionuse{-}{pp-annot} must be used to
preprocess the annotations~\cite{userman}):
\begin{shell}
\$ frama-c -pp-annot -e-acsl archi.c -then-last -print -ocode monitored_archi.i
\$ gcc -o archi `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_archi.i
\end{shell}
However, the generated code fails at runtime on an X86 64-bit computer because
a 32-bit architecture was assumed at generation time.
\begin{shell}
\$ ./archi
Assertion failed at line 10 in function main.
The failing predicate is:
sizeof(long) == 8.
\end{shell}
There is no assertion failure if you add the option \texttt{-machdep x86\_64}
when running the \eacsl plug-in.
\begin{shell}
\$ frama-c -machdep x86_64 -pp-annot -e-acsl archi.c \
-then-last -print -ocode monitored_archi.i
\end{shell}
\begin{important}\index{Gcc}
If you plan to compile the generated code with \gcc, it is even better to set
\texttt{-machdep} to \texttt{gcc\_x86\_64} (or \texttt{gcc\_x86\_32}), even if
it does not matter on this simple example.
\end{important}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Libc}\index{Libc}
By default, \framac uses its own standard library (\emph{aka} libc) instead of
the one of your system. If you do not want to use it, you have to add the option
\texttt{-no-framac-stdlib}\optionidx{-}{framac-stdlib} to the \framac command
line following options on the command line:
\shortopt{no-framac-stdlib}\optionidx{-}{framac-stdlib} to the \framac command
line.
It might be particularly useful in one of the following contexts:
\begin{itemize}
\item several libc functions are still not defined in the \framac libc; or
\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
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 runtime errors matter).
verifying them (for instance, only checking undefine behaviors matters).
\end{itemize}
\begin{important} \index{eacslgcc}
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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Integers}
\label{sec:integers}
\index{GMP}
\eacsl has got a type \texttt{integer}\codeidx{integer} which exactly
corresponds to mathematical integers. Such a type does not fit in any integral
\C type. To circumvent this issue, \eacsl uses the \gmp
library\footnote{\url{http://gmplib.org}}. Thus, even if \eacsl does its best to
use standard integral types instead of \gmp~\cite{sac13,jfla15}, it may generate
such integers from time to time. In such cases, the generated code must be
linked against \gmp to be executed.
\eacsl uses an \texttt{integer}\codeidx{integer} type corresponding to
mathematical integers which does not fit in any integral \C type. To circumvent
this issue, \eacsl uses the \gmp library\footnote{\url{http://gmplib.org}}.
Thus, even if \eacsl does its best to use standard integral types instead of
\gmp~\cite{sac13,jfla15}, it may generate such integers from time to time. It is
notably the case if your program contains \lstinline|long long|, either signed
or unsigned.
Consider for instance the following program.
......@@ -352,33 +463,23 @@ Consider for instance the following program.
\cinput{examples/gmp.i}
Even on a 64-bit machine, it is not possible to compute the assertion with a
standard \C type. In this case, the \eacsl plug-in generates \gmp code.
We can generate an instrumented code as usual through the following command
line:
\begin{shell}
\$ frama-c -e-acsl gmp.i -then-last -print -ocode monitored_gmp.i
\end{shell}
To compile it however, you need to have \gmp installed and to add the option
\optionuse{-}{lgmp} to \gcc as follow:
\begin{shell}
\$ gcc -o pow_gmp `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_gmp.i -lgmp
\end{shell}
standard \C type. In this case, the \eacsl plug-in generates \gmp code. Note
that E-ACSL library already includes \gmp, thus no additional arguments need to
be provided. We can generate and execute the instrumented code as usual via
the following command:
We can now execute it as usual.
\begin{shell}
\$ ./pow_gmp
\$ e-acsl-gcc.sh -omonitored_gmp.i -Ogmp gmp.i
\$ ./gmp.e-acsl
\end{shell}
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 \eacsl annotation.
Note that it is possible to use \gmp arithmetic in all cases (even if not
required). This option is controlled through \shortopt{g} switch of \eacslgcc
which passes the \shortopt{e-acsl-gmp-only} option to the \eacsl
plug-in. However it could slow down the execution of the instrumented program
significantly.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -386,112 +487,205 @@ any integral \C type in an \eacsl annotation.
\label{sec:memory}
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 specific memory library installed with the plug-in. This
library includes two \C files which are installed in the \eacsl' share
directory:
\begin{itemize}
\item \texttt{memory\_model/e\_acsl\_bittree.c}, and
\item \texttt{memory\_model/e\_acsl\_mmodel.c}.
\end{itemize}
Consider for instance the following program.
\lstinline|\valid|. Consider for instance the following program.
\listingname{valid.c}
\cinput{examples/valid.c}
Assuming that we want to execute the generated code on an X86 64-bit machine and
to compile it with \gcc, the generation of the instrumented code requires the
use of the option \optionuse{-}{machdep} since the code uses
\texttt{sizeof}. However, nothing is required here.
Even though the first annotation holds, the second annotation (labelled
\I{freed}) is invalid. This is because at the point of its execution memory
allocated via \texttt{malloc} has been deallocated and \T{x} is a stale pointer
referencing unallocated memory. The execution of the instrumented program thus
reports the violation of the second annotation:
\begin{shell}
\$ frama-c -machdep gcc_x86_64 -e-acsl valid.c -then-last -print -ocode monitored_valid.i
\$ 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
\end{shell}
Since the original code uses \lstinline|\valid|, the executable binary
must be generated from \texttt{monitored\_valid.i} as follow:
To check memory-related predicates (such as \lstinline|\valid|) \eacsl tracks
memory allocated by a program at runtime. \eacsl records memory blocks in a
meta-storage tracking each block's boundaries (i.e., its base address and
length), per-byte initialization and the notion of an address being freeable
(i.e., whether it can be safely passed to the \texttt{free} function). During
an execution of the instrumented program code injected by \eacsl
transformations queries the meta-storage to identify properties of an address
in question. For instance, during the execution of the above program the
monitor injected by \eacsl first records information about the memory block
allocated via a call to \texttt{malloc}. Further, during the execution of the
first assertion the monitor queries the meta-storage about the address of the
memory location pointed to by \texttt{x}. Since the location belongs to an
allocated memory block, the meta-storage identifies it as belonging to the
tracked allocation. Consequently, the assertion evaluates to true and the
monitors allows the execution to continue. The second assertion, however,
fails. This is because the block pointed to by \T{x} has been removed from the
meta-storage by a call to \T{free}, and thus a meta-storage query identifies
location \T{x} as belonging unallocated memory space.
\subsubsection{\eacsl Memory Models}
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}.
Each of the supported memory models is implemented as a separate static library
installed along with \eacsl plug-in itself. This is such that
\T{libeacsl-rtl-bittree.a} implements memory tracking using Patricia-trie and
\T{libeacsl-rtl-segment.a} implements shadow-based tracking.
The functionality of the provided memory models (and therefore libraries
implementing them) is equivalent, however they differ in performance. We
further discuss performance considerations.
Additionally to memory tracking both libraries include customized version of
the \gmp library, \jemalloc\footnote{\url{http://jemalloc.net/}} memory
allocator replacing system-wide malloc and other utilities including \eacsl
assertions. It is therefore safe to link an \eacsl-instrumented program
against any of these libraries. For instance, in Section~\ref{sec:exec} we
have linked the instrumented program in \texttt{monitored\_first.i} against
\T{libeacsl-rtl-bittree.a}, but you can also link it against the library
implementing the segment-based memory model via \T{-leacsl-rtl-segment}.
At the level of \eacslgcc you can choose between different memory models using
the \shortopt{m} switch followed by the name of the memory model to link
against. For instance, command
\begin{shell}
\$ DIR=`frama-c -print-share-path`/e-acsl
\$ MDIR=\$DIR/memory_model
\$ gcc -o valid -DE_ACSL_MACHDEP=x86_64 \
\$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \$MDIR/e_acsl_mmodel.c \
monitored_valid.i
\$ e-acsl-gcc.sh -mbittree -c -Ovalid valid.c
\end{shell}
The \gcc's option \lstinline|-DE_ACSL_MACHDEP=x86_64| indicates to preprocess
the memory library for an x86-64bits architecture.
Now we can execute the generated binary which fails at runtime since the second
assertion is violated.
links a program generated from \T{valid.c} against the library implementing the
bittree-based memory model, whereas the following invocation uses shadow-based
tracking:
\begin{shell}
\$ ./valid
Assertion failed at line 11 in function main.
The failing predicate is:
freed: \valid(x).
\$ e-acsl-gcc.sh -msegment -c -Ovalid valid.c
\end{shell}
It is also possible to generate executables using both models as follows:
\begin{shell}
\$ e-acsl-gcc.sh -msegment,bittree -c -Ovalid valid.c
\end{shell}
In this case, \eacslgcc produces 3 executables: \T{valid},
\T{valid.e-acsl-segment} and \T{valid.e-acsl-bittree} corresponding to an
executable generated from the original source code, and the executables
generated from the \eacsl-instrumented sources linked against
segment-based and bittree-based memory models.
Unless specified, \eacsl defaults to the bittree-based memory model.
\subsubsection{Performance Considerations}
\label{sec:perf}
As pointed out in the previous section the functionalities provided by both
segment-based and bittree-based memory models are equivalent but differ in
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}.
%[Need ref here with comparison of the performance. Ideally a reference to the PLDI paper].
\subsubsection{Maximized Memory Tracking}
By default \eacsl uses static analysis to reduce instrumentation and therefore
runtime and memory overheads~\cite{scp16}. With respect to memory tracking this
means that
\eacsl may omit recording memory blocks irrelevant for runtime analysis. It
is, however, still possible to systematically instrument the code for handling
potential memory-related annotations even when it is not required. This
feature can be enabled using the \shortopt{M} switch of \eacslgcc or
\shortopt{e-acsl-full-mmodel} option of the \eacsl plug-in.
Like for integers, the \eacsl plug-in does its best to use the dedicated memory
library only when required~\cite{rv13,jfla15}. 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.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Debug Libraries}
\label{sec:runtime-debug}
However, if your program contains some 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}, witness the following
example.
\eacsl runtime libraries mentioned in Section~\ref{sec:memory} (i.e.,
\T{libeacsl-rtl-bittree.a} and \T{libeacsl-rtl-segment.a}) are optimized for
performance (via \shortopt{-O2} compiler flag). An \eacsl installation also
provides unoptimized versions of these libraries (suffixed \T{-dbg.a}) aimed at
being used during debugging.
\listingname{pointer.c}
\cinput{examples/pointer.c}
The main difference between unoptimized (debug) and optimized (production)
libraries is that debug libraries include assertions validating the correctness
of the RTL itself. For instance, during memory tracking such assertions ensure
that during a run of a program all tracked memory blocks are disjoint.
Consider the following program that violates an annotation
in function \T{foo} via a call \T{bar(p+1)} in the main function:
\listingname{rte\_debug.i}
\cinput{examples/rte_debug.i}
A monitored executable linked against a debug version of \eacsl RTL
can ge generated using
\longopt{rt-debug} flag of \eacslgcc as follows:
\begin{shell}
\$ e-acsl-gcc.sh --rt-debug -c -omonitored_rte_debug.c -Orte_debug rte_debug.i
\end{shell}
A run of the monitored executable shows violation of the \eacsl annotation.
\begin{shell}
\$ frama-c -machdep gcc_x86_64 -e-acsl pointer.c -then-last -print -ocode
monitored_pointer.i
\$ DIR=`frama-c -print-share-path`/e-acsl
\$ MDIR=\$DIR/memory_model
\$ gcc -o pointer \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \$MDIR/e_acsl_mmodel.c\
monitored_pointer.i
\$ ./pointer
RTE failed at line 12 in function main.
\$ rte_debug.e-acsl
Assertion failed at line 2 in function foo.
The failing predicate is:
mem_access: \valid_read(x).
\valid(p).
/** Backtrace **************************/
trace at e_acsl_trace.h:45
- exec_abort at e_acsl_assert.h:58
- runtime_assert at e_acsl_assert.h:93
- foo at monitored_rte_debug.c:92
- bar at monitored_rte_debug.c:102
- main at monitored_rte_debug.c:119
/***************************************/
Aborted
\end{shell}
The option \optiondef{-}{e-acsl-full-mmodel} (unset by default) may be set to
systematically instrument the code for handling potential memory-related
annotations, even when it is not required. If it is set, the generated program
must be always linked against the memory library.
A run of an executable linked against an unoptimized RTL shows a stack trace on
the instrumented program saved to \T{monitored\_rte\_debug.c}. In the example
above calls to \T{exec\_abort} and \T{runtime\_assert} belong to the \eacsl
RTL, whereas calls to \T{foo}, \T{bar} and \T{main} belong to the input
program.
It should be noted that because debug versions of \eacsl RTL are compiled
without compile-time optimizations and execute additional assertions the
runtime overheads of the instrumented programs linked against the debug
versions of \eacsl RTL can be up to 10 times greater than those linked against
the production versions.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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
defined in the file \texttt{e\_acsl.c} of the \eacsl library. By default, it
does nothing if the predicate is valid, while it prints an error message and
exits (with status 1) if the predicate is invalid.
\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} is called. By
default, it does nothing if the predicate is valid, and prints an error message
and aborts the execution if the predicate is invalid.
\texttt{\_\_e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} function is defined as
a weak symbol in the \eacsl library, therefore it is possible to modify this
behavior by providing an alternative definition of \texttt{\_\_e\_acsl\_assert}.
You must only respect the following signature:
It is however possible to modify this behavior by providing your own definition
of \texttt{e\_acsl\_assert}. You must only respect the signature of the function
as declared in the file \texttt{e\_acsl.h} of the \eacsl library. Below is an
example which prints the validity status of each property but never exits.
\cinput{examples/assert_sign.c}
Below is an 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 of \texttt{e\_acsl.c}, as shown below (we reuse the initial example
Then you can generate the program as usual, (we reuse the initial example
\texttt{first.i} of this manual).
\begin{shell}
\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.i
\$ gcc -o customized_first my_assert.c monitored_first.i
\$ ./customized_first
\$ e-acsl-gcc.sh -c first.i my_assert.c -Ocustomized_first
\$ ./customized_first.e-acsl
Assertion at line 3 in function main is valid.
The verified predicate was: `x == 0'.
Assertion at line 4 in function main is invalid.
......@@ -500,16 +694,14 @@ The verified predicate was: `x == 1'.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Incomplete Programs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{Incomplete Programs} % <<<
\label{sec:incomplete}
Executing a \C program requires to have a complete application. However, the
\eacsl plug-in does not necessarily require to have it to generate the
instrumented code. It is still possible to instrument a partial program with no
entry point or in which some functions remain undefined, even though a few
restrictions.
entry point or in which some functions remain undefined.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -517,9 +709,8 @@ restrictions.
\label{sec:no-main}
\index{Program!Without main}
The \eacsl plug-in may work even if there is no \texttt{main} function.
Consider for instance the following annotated program without such a
\texttt{main}.
The \eacsl plug-in can instrument a program without the \T{main} function.
Consider for instance the following annotated program without \texttt{main}.
\listingname{no\_main.i}
\cinput{examples/no_main.i}
......@@ -527,7 +718,7 @@ Consider for instance the following annotated program without such a
The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ frama-c -e-acsl no_main.i -then-last -print -ocode monitored_no_main.i
\$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
<skip preprocessing command line>
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
......@@ -537,33 +728,32 @@ warning.
[e-acsl] translation done in project "e-acsl".
\end{shell}
This warning indicates that the instrumentation would be incorrect if the
This warning indicates that the instrumentation could be incorrect if the
program contains memory-related annotations (see
Section~\ref{sec:limits:no-main}). That is 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 like
the following one. In this particular case, we also need to link against \gmp as
explained in Section~\ref{sec:integers}.
compiler in a standard way, and even link it against additional files such as
the following:
\listingname{main.c}
\cinput{examples/main.c}
\begin{shell}
\$ gcc -o with_main `frama-c -print-share-path`/e-acsl/e_acsl.c \
monitored_no_main.i main.c -lgmp
\$ ./with_main
\$ e-acsl-gcc.sh -C monitored_no_main.i main.c -Owith_main
\$ ./with_main.e-acsl
x = 65536
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\
\subsection{Undefined Functions}
\label{sec:no-code}
\index{Function!Undefined}
The \eacsl plug-in may also work if some functions have no implementation.
Consider for instance the following annotated program for which the
implementation of the function \texttt{my\_pow} is not provided.
Similar to the above section \eacsl is capable of instrumenting a program which
has definitions of arbitrary functions missing. Consider for instance the
following annotated program for which the implementation of the function
\texttt{my\_pow} is not provided.
\listingname{no\_code.c}
\cinput{examples/no_code.c}
......@@ -571,50 +761,49 @@ implementation of the function \texttt{my\_pow} is not provided.
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
[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.
[kernel] warning: No code nor implicit assigns clause for function my_pow,
no_code.c:9:[kernel] warning: No code nor implicit assigns clause for function my_pow,
generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
\end{shell}
Like in the previous Section, this warning indicates that the instrumentation
would be incorrect if the program contains memory-related annotations (see
Similar to the previous Section the warning indicates that the instrumentation
could 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
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}.
safely ignore it.
\listingname{pow.i}
\cinput{examples/pow.i}
Similar to the example shown in the previous section you can generate the
executable by providing definition of \T{my\_pow}.
\begin{shell}
\$ gcc -o no_code `frama-c -print-share-path`/e-acsl/e_acsl.c \
pow.i monitored_no_code.i -lgmp
\$ ./no_code
Postcondition failed at line 8 in function my_pow.
\$ 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.
\old(n % 2 == 0) ==> \result >= 1.
Aborted
\end{shell}
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 large exponentiations.
implementation of the function \texttt{my\_pow} overflows in case of large
exponentiations.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Combining E-ACSL with Other Plug-ins}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{Combining E-ACSL with Other Plug-ins} % <<<
\label{sec:combine}
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
the option \shortopt{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 make
intensive use of dynamic structures which are usually difficult to handle by
......@@ -632,25 +821,44 @@ Consider the following program.
\cinput{examples/combine.i}
To check at runtime that this program does not perform any runtime error (which
are potential overflows in this case), just do:
\begin{shell}
\$ frama-c -rte combine.i -then -e-acsl -then-last -print \
\$ frama-c -rte combine.i -then -e-acsl -then-last -print
-ocode monitored_combine.i
\$ gcc -o combine `frama-c -print-share-path`/e-acsl monitored_combine.i
\$ e-acsl-gcc.sh -C -Ocombine monitored_combine.i
\$ ./combine.
\end{shell}
Nevertheless if you run the \eacsl plug-in after another one, it first generates
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
\end{shell}
Note the use of \eacslgcc \longopt{rte} option which asks \framac to combine
\eacsl with \rte plug-in. This plug-in automatically instruments the input
program with runtime
assertions before running the \eacsl plug-in on it. \longopt{rte} option of
\eacslgcc also accepts a comma-separated list of arguments indicating the types
of assertions to generate. Consult the \eacslgcc man page for a detailed
list of arguments accepted by \longopt{rte}.
The present implementation of \eacslgcc does not fully support combining \eacsl
with other \framac plug-ins. However it is still possible to instrument programs
with \eacsl directly and use \eacslgcc to compile the generated code.
If you run the \eacsl plug-in after another one, it first generates
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, the results
of already executed analyzers (such as validity status of 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.
\shortopt{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
\optiondef{-}{e-acsl-valid}. For instance, \valueplugin~\cite{value} is able to
\shortopt{e-acsl-valid}. For instance, \valueplugin~\cite{value} is able to
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.
......@@ -666,49 +874,54 @@ The additional code will be generated with one of the two following commands.
-then-last -print -ocode monitored_combine.i
\end{shell}
In the first case, that is because it is explicitly required by the option
\texttt{-e-acsl-valid} while, in the second case, that is because the option
\texttt{-e-acsl-prepare} is not provided on the command line which results in
\shortopt{e-acsl-valid} while, in the second case, that is because the option
\shortopt{e-acsl-prepare} is not provided on the command line which results in
the fact that the result of the value analysis are unknown when the \eacsl
plug-in is running.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Customization}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{Customization} % <<<
\label{sec:custom}
There are several 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}.
Second, the directory where 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 shifts in annotation are not
yet supported by 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 \shortopt{e-acsl-project} option of the
\eacsl plug-in. While there is not direct support for this option in \eacslgcc
you can pass it using \shortopt{F} switch:
\listingname{check.i}
\cinput{examples/check.i}
\begin{shell}
\$ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i
<skip preprocessing commands>
[e-acsl] beginning translation.
check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "foobar".
\end{shell}
Further, the \eacsl plug-in option \shortopt{e-acsl-check} does not generate a
new project but verifies that each annotation is translatable. Then it produces
a summary as shown in the following example (left or right shifts in annotations
are not yet supported by the \eacsl plug-in~\cite{eacsl-implem}).
\begin{shell}
\$ frama-c -e-acsl-check check.i
<skip preprocessing commands>
check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
Ignoring annotation.
Ignoring annotation.
[e-acsl] 0 annotation was ignored, being untypable.
[e-acsl] 1 annotation was ignored, being unsupported.
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Verbosity Policy}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{Verbosity Policy} % <<<
\label{sec:verbose}
By default, \eacsl does not provide much information when it is running. Mainly,
......@@ -726,23 +939,23 @@ message categories which indicate the \emph{kind} of information to display.
\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
option \shortopt{e-acsl-verbose}. It is 1 by default. Below is indicated
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
\texttt{-e-acsl-verbose 0}& only warnings and errors\\
\shortopt{e-acsl-verbose 0}& only warnings and errors\\
\hline
\texttt{-e-acsl-verbose 1}& beginning and ending of the translation\\
\shortopt{e-acsl-verbose 1}& beginning and ending of the translation\\
\hline
\texttt{-e-acsl-verbose 2}& different parts of the translation and
\shortopt{e-acsl-verbose 2}& different parts of the translation and
functions-related information\\
\hline
\texttt{-e-acsl-verbose 3}& predicates- and statements-related information\\
\shortopt{e-acsl-verbose 3}& predicates- and statements-related information\\
\hline
\texttt{-e-acsl-verbose 4}& terms- and expressions-related information
\shortopt{e-acsl-verbose 4}& terms- and expressions-related information
\\
\hline
\end{tabular}
......@@ -753,8 +966,8 @@ also displays the information of all the lower levels.
\subsection{Message Categories}
The kind of information to display is settable by the option
\optiondef{-}{e-acsl-msg-key} (and unsettable by the option
\optiondef{-}{e-acsl-msg-key-unset}). The different keys refer to different
\shortopt{e-acsl-msg-key} (and unsettable by the option
\shortopt{e-acsl-msg-key-unset}). The different keys refer to different
parts of the translation, as detailed below.
\begin{center}
......@@ -773,5 +986,4 @@ typing & minimization of the instrumentation for integers
\hline
\end{tabular}
\end{center}
% >>>
src/plugins/e-acsl/visit.ml
+ 1
− 2
View file @ 5bfbc197
......@@ -246,8 +246,7 @@ class e_acsl_visitor prj generate = object (self)
f.globals <- new_globals
| None ->
Kernel.warning "@[no entry point specified:@ \
you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
fname;
you must call function `__e_acsl_memory_init` by yourself.@]";
f.globals <- f.globals @ [ cil_fct ]
in
Project.on prj build_initializer ()
......
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