diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 0928d345e79fc1be3384a5729760e04394899f1e..f319a7d544db96e5f7fccbe60d7c5764cce0c065 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-0.6+dev
+0.7+dev
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 4492d7911122db32816ebd55dbff6eb442519c0c..2855dee8cda9a43228c879ec6d75e63de727cb39 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -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
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 6bc3d9e3068d7c377c74f4c443ffbb5a3df626d0..ff5bdf6668ebf41e34e2c3f038bda7bd6ed32096 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -1,10 +1,9 @@
@manual{userman,
title = {Frama-C User Manual},
- author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
- Armand Puccetti and Virgile Prevosto and Julien Signoles and
+ author = {Loïc 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 Loïc 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 = {Loïc Correnson and Zaynah Dargaye and Anne Pacalet},
+ author = {Patrick Baudin and François Bobot and Loïc 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 = {Loïc 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 Mickaël Delahaye and Stéphane
- 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},
+}
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 2afd8adb6ce837c61726a4586987394fdb614056..8b0dca325e5452bb0dbe2bf069d4dbe2ff9dd10c 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -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}
diff --git a/src/plugins/e-acsl/doc/userman/eacslgcc.tex b/src/plugins/e-acsl/doc/userman/eacslgcc.tex
deleted file mode 100644
index 43f8e99a9d6c86f50f0400b74b6a4873d9846237..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/doc/userman/eacslgcc.tex
+++ /dev/null
@@ -1,183 +0,0 @@
-\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.
diff --git a/src/plugins/e-acsl/doc/userman/examples/assert_sign.c b/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
new file mode 100644
index 0000000000000000000000000000000000000000..ce2e56c6fb9579df15f0211548e355dfcd5af08d
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/assert_sign.c
@@ -0,0 +1,2 @@
+void __e_acsl_assert(int pred, char *kind,
+ char *func_name, char *pred_text, int line);
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.i b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.i
new file mode 100644
index 0000000000000000000000000000000000000000..e777ec7e0417b5d5bfe0f114574ed0a626f868c8
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.i
@@ -0,0 +1,61 @@
+\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}
diff --git a/src/plugins/e-acsl/doc/userman/examples/modified_main.c b/src/plugins/e-acsl/doc/userman/examples/modified_main.c
index c990f33187a8d89bc4b32e2d880c4f89be28e182..b3ed0376bc42f408594d3c459f094bfe51c5fea9 100644
--- a/src/plugins/e-acsl/doc/userman/examples/modified_main.c
+++ b/src/plugins/e-acsl/doc/userman/examples/modified_main.c
@@ -1,10 +1,4 @@
-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;
}
diff --git a/src/plugins/e-acsl/doc/userman/examples/my_assert.c b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
index 4c124e0b1866d7674d034e5017d3fdb8f9caa6c8..e22ee0720a768054f143d792014d63ad9dcbb775 100644
--- a/src/plugins/e-acsl/doc/userman/examples/my_assert.c
+++ b/src/plugins/e-acsl/doc/userman/examples/my_assert.c
@@ -1,12 +1,8 @@
#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);
}
diff --git a/src/plugins/e-acsl/doc/userman/examples/no_main.i b/src/plugins/e-acsl/doc/userman/examples/no_main.i
index 6c21ce10d60b62147e5994827ea953731cf733fe..9047098909a043f63b5ffacfdfcce3e56e1467f2 100644
--- a/src/plugins/e-acsl/doc/userman/examples/no_main.i
+++ b/src/plugins/e-acsl/doc/userman/examples/no_main.i
@@ -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;
}
+
+
diff --git a/src/plugins/e-acsl/doc/userman/examples/rte_debug.i b/src/plugins/e-acsl/doc/userman/examples/rte_debug.i
new file mode 100644
index 0000000000000000000000000000000000000000..f541f1e8e2af1d09998af1c76b9c662daf889ba8
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/rte_debug.i
@@ -0,0 +1,16 @@
+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;
+}
+
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 3fd972fe589a41b976e2cd6433b8fcd5a8449193..e3a2edf31cefb7a71dbba36ff87f651325b043cc 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -1,37 +1,40 @@
\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.
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 534bfc4cddfde0e1ae2b3e0dd7331d9472494cc1..cb007c17c1462a65e53043a7d2d210be6dc61fae 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -1,11 +1,12 @@
\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.
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index 61572c7cba1c1e522b54dadcfd74599feaef92fd..3ccfbd99b5b523867c696a58860fb7b5490a08ee 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -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
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 4d713e7d3e24c0f3770b4bcf2627a4afa77345bb..11d07531f416aa0e1e03ef20666dbf8acc37f458 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index da6ca9a13c39a581fdffa34883d680953313533d..934325005ecf522ec30da5ad6275465a91f1f030 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -1,190 +1,150 @@
\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}
-
-
+% >>>
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 5a820826ce88158bfa6b2d9b335ec700d15ed429..2a76fd3872c10d5bf640501100b1143ed2d99cf3 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -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 ()