diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 0fac06906078bff672ef05555f9cafaa0820c22a..2eb3c4fe4eebcdea3da0790cc0ba74cb286ec4f4 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-0.4.1+dev
+0.5
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 86ac96a1e814dc3f02c0f061ae59820a0bd83450..30272295f402784cfca682a2b0c3b1fd186c7df2 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,10 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+########################
+Plugin E-ACSL 0.5 Sodium
+########################
+
- E-ACSL [2015/06/01] Support of \freeable. Thus illegal calls to
free (e.g. double free) are detected.
-* E-ACSL [2015/05/28] Fix types of \block_length and \offset.
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf
index 60374aa4a458eef18d85348491b499810d4fd453..008cf267af995537f7ece3fc7f26bfdcea23d019 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 1c7943103ab157f63da6431ac06c9cc2dfe03a19..25aafc00b0e30815481e645605c075a3e4ac397a 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -16,7 +16,7 @@ default: main.pdf
main.pdf: $(DEPS_MODERN)
EACSL_VERSION= $(shell cat $(VERSION_FILE))
-FC_VERSION= Neon
+FC_VERSION= Sodium
EACSL_DIR=../..
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 7d0c29f24a18dd3b96fc830318e200d04692fbf9..6bc3d9e3068d7c377c74f4c443ffbb5a3df626d0 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -38,26 +38,26 @@
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 = apr,
- title = {ACSL: ANSI/ISO C Specification Language. Version 1.8 ---
+ month = mar,
+ title = {ACSL: ANSI/ISO C Specification Language. Version 1.9 ---
Frama-C Neon implementation.},
- year = {2014}
+ year = {2015}
}
@manual{eacsl,
author = {Julien Signoles},
- title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.8},
- year = 2014,
- month = apr,
+ title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.9},
+ year = 2015,
+ month = jun,
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
}
@manual{eacsl-implem,
author = {Julien Signoles},
- title = {E-ACSL Version 1.7.
- Implementation in Frama-C Plug-in E-ACSL version 0.4},
- year = 2014,
- month = apr,
+ title = {E-ACSL Version 1.9.
+ Implementation in Frama-C Plug-in E-ACSL version 0.5},
+ year = 2015,
+ month = jun,
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
}
@@ -124,6 +124,19 @@
month = oct,
}
+@article{fac15,
+year={2015},
+month={jan},
+journal={Formal Aspects of Computing},
+title={{Frama-C: A Software Analysis Perspective}},
+publisher={Springer London},
+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,
author = {Lori A. Clarke and
David S. Rosenblum},
@@ -155,3 +168,13 @@
year = 2009,
publisher = {{IEEE} Computer Society},
}
+
+@inproceedings{jfla15,
+ title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
+ author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+ booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
+ editor = {David Baelde and Jade Alglave},
+ year = {2015},
+ month = jan,
+ note = {In French},
+}
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 2d98c60ec54379a10804a8e4c8c465aef8780f8b..5fd7532a3866c6863d2a64359cfa4c360cd43cad 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -6,13 +6,18 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslversion}
\begin{itemize}
+\item \textbf{Libc}: new section.
+\item \textbf{Architecture Dependent Annotations}: add a remark about \gcc's
+ machdep.
+\item Use \texttt{-then-last} whenever possible.
+\item Update output wrt \framac Sodium changes.
\item \textbf{Bibliography:} fix incorrect links.
\end{itemize}
\section*{E-ACSL 0.4}
\begin{itemize}
-\item No change
+\item No change.
\end{itemize}
\section*{E-ACSL 0.3}
diff --git a/src/plugins/e-acsl/doc/userman/eacslversion.tex b/src/plugins/e-acsl/doc/userman/eacslversion.tex
index e8d776727c61611ca4b294e6aead5c4277bd7ddb..b962244f9d57fc8b5f4b8cba06716cfe6bb23a5d 100644
--- a/src/plugins/e-acsl/doc/userman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/userman/eacslversion.tex
@@ -1,2 +1,2 @@
-\newcommand{\eacslversion}{0.4.1\xspace}
-\newcommand{\fcversion}{Neon\xspace}
+\newcommand{\eacslversion}{0.5\xspace}
+\newcommand{\fcversion}{Sodium\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/examples/pointer.c b/src/plugins/e-acsl/doc/userman/examples/pointer.c
index 4bab6d41faf74ecb1daff715fb4085a5cb1045e0..43d0fb4b088b7d84e19180568fa876c1327ffda6 100644
--- a/src/plugins/e-acsl/doc/userman/examples/pointer.c
+++ b/src/plugins/e-acsl/doc/userman/examples/pointer.c
@@ -1,4 +1,4 @@
-#include "stdlib.h"
+#include <stdlib.h>
extern void *malloc(size_t);
extern void free(void*);
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index d2e536b9453307788c6edde3059feaf2d601ab83..3fd972fe589a41b976e2cd6433b8fcd5a8449193 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -1,7 +1,7 @@
\chapter{Introduction}
-\framac~\cite{userman,sefm12} is a modular analysis framework for the C language
-which supports the ACSL specification language~\cite{acsl}. This manual
+\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
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index d666389d9db0282fd7c754b4728cf651de9ab7d5..c5c52f75339852fb785f00a2d0f75318e5913e1d 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -275,3 +275,11 @@
\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
+
+\definecolor{gris}{gray}{0.85}
+\makeatletter
+\newenvironment{important}%
+{\hspace{5pt plus \linewidth minus \marginparsep}%
+ \begin{lrbox}{\@tempboxa}%
+ \begin{minipage}{\linewidth - 2\fboxsep}}
+{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index f896579ded4a96452459fd4347dc3f0947669db8..3de64a5d6dbea2b68aedd97bd46cad8ec39ebdc8 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -42,14 +42,15 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
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}. However the development of the
-\eacsl plug-in is still ongoing: features described here may still evolve in the
-future.
+\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.
\section*{Acknowledgements}
-We gratefully thank all the people who contributed to this document: Florent
-Kirchner, Nikolaï Kosmatov and Guillaume Petiot.
+We gratefully thank all the people who contributed to this document: Jens
+Gerlach, Pierre-Lo\"ic Garoche, Florent Kirchner, Nikolaï Kosmatov and Guillaume
+Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 830a76bf2b5c133c57bd56c701436499a5376ecc..47981cbfc6d7bcc3f5aa4ee7bddc33308bf70f7e 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -39,38 +39,40 @@ Running \eacsl on this file just consists in adding the option
\optiondef{-}{e-acsl} to the \framac command line:
\begin{shell}
\$ frama-c -e-acsl first.i
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
+[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 first.i (no preprocessing)
[e-acsl] beginning translation.
[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 explain later, mainly in
+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-on} and \optionuse{-}{print} which respectively
-switch to another project and pretty prints the \C code~\cite{userman}:
+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}:
\begin{shell}
-\$ frama-c -e-acsl first.i -then-on e-acsl -print
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
+\$ 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 */
@@ -82,9 +84,6 @@ struct __anonstruct___mpz_struct_1 {
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
-/*@
-model __mpz_struct { integer n };
-*/
/*@ requires predicate != 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -93,18 +92,24 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *pred_txt,
int line);
-int __fc_random_counter __attribute__((__unused__));
+/*@
+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; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__); */
/*@
-axiomatic
- dynamic_allocation {
+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;
/*@
@@ -152,20 +157,22 @@ precise error reports as shown in Section~\ref{sec:exec}.
\label{sec:exec}
By using the option \optionuse{-}{ocode} of \framac~\cite{userman}, we can
-redirect the generated code into a \C file as follows.
+redirect the generated code into a \C file as follow.
\begin{shell}
-\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
+\$ 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.
-\lstset{escapechar=£}
+\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:19:60: 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
@@ -223,8 +230,8 @@ undefined as soon as $e$ has to be evaluated in order to evaluate $t$
undefined term is never evaluated''}~\cite{eacsl}.
Accordingly, the \eacsl plug-in prevents an undefined term from being
-evaluated. Should it be because an annotation contains such a term, it will
-report a proper error at runtime instead.
+evaluated. If an annotation contains such a term, \eacsl will report a proper
+error at runtime instead of evaluating it.
Consider for instance the following annotated program.
@@ -239,7 +246,7 @@ However we can generate an instrumented code and compile it through the
following command lines:
\begin{shell}
-\$ frama-c -e-acsl rte.i -then-on e-acsl -print -ocode monitored_rte.i
+\$ 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
\end{shell}
@@ -255,7 +262,7 @@ division_by_zero: y != 0.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Architecture Dependent Annotations}
+\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
@@ -279,7 +286,7 @@ 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-on e-acsl -print -ocode monitored_archi.i
+\$ 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}
@@ -298,9 +305,32 @@ when running the \eacsl plug-in.
\begin{shell}
\$ frama-c -machdep x86_64 -pp-annot -e-acsl archi.c \
- -then-on e-acsl -print -ocode monitored_archi.i
+ -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:
+
+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 your system libc and the \framac libc mismatch about several function
+ types (for instance, your system libc is not 100\% posix compliant); or
+\item several \framac lib functions get a contract and you are not interested in
+ verifying them (for instance, only runtime errors matter).
+\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -312,9 +342,9 @@ when running the \eacsl plug-in.
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}, it may generate such
-integers from time to time. In such cases, the generated code must be linked
-against \gmp to be executed.
+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.
Consider for instance the following program.
@@ -328,11 +358,11 @@ We can generate an instrumented code as usual through the following command
line:
\begin{shell}
-\$ frama-c -e-acsl gmp.i -then-on e-acsl -print -ocode monitored_gmp.i
+\$ 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 follows:
+\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
@@ -370,17 +400,17 @@ 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,
-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.
+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.
\begin{shell}
-\$ frama-c -machdep x86_64 -e-acsl valid.c -then-on e-acsl -print -ocode monitored_valid.i
+\$ frama-c -machdep gcc_x86_64 -e-acsl valid.c -then-last -print -ocode monitored_valid.i
\end{shell}
Since the original code uses \lstinline|\valid|, the executable binary
-must be generated from \texttt{monitored\_valid.i} as follows:
+must be generated from \texttt{monitored\_valid.i} as follow:
\begin{shell}
\$ DIR=`frama-c -print-share-path`/e-acsl
@@ -403,9 +433,9 @@ freed: \valid(x).
\end{shell}
Like for integers, the \eacsl plug-in does its best to use the dedicated memory
-library only when required~\cite{rv13}. So, if your program does not contain
-memory-related annotations, the generated one does not require to be linked
-against the dedicated memory library, like the examples of the previous
+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.
However, if your program contains some annotations with pointer dereferencing
@@ -419,7 +449,7 @@ example.
\cinput{examples/pointer.c}
\begin{shell}
-\$ frama-c -machdep x86_64 -e-acsl pointer.c -then-on e-acsl -print -ocode
+\$ 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
@@ -459,7 +489,7 @@ instead of \texttt{e\_acsl.c}, as shown below (we reuse the initial example
\texttt{first.i} of this manual).
\begin{shell}
-\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
+\$ 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
Assertion at line 3 in function main is valid.
@@ -497,7 +527,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-on e-acsl -print -ocode monitored_no_main.i
+\$ frama-c -e-acsl no_main.i -then-last -print -ocode monitored_no_main.i
<skip preprocessing command line>
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
@@ -603,7 +633,7 @@ Consider the following program.
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-on e-acsl -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
\$ ./combine.
@@ -626,14 +656,14 @@ plug-in does not generate additional code for checking them if you run the
following command.
\begin{shell}
\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
- -then-on e-acsl -print -ocode monitored_combine.i
+ -then-last -print -ocode monitored_combine.i
\end{shell}
The additional code will be generated with one of the two following commands.
\begin{shell}
\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
- -e-acsl-valid -then-on e-acsl -print -ocode monitored_combine.i
+ -e-acsl-valid -then-last -print -ocode monitored_combine.i
\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -then-on e-acsl -print -ocode monitored_combine.i
+ -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
@@ -712,7 +742,7 @@ also displays the information of all the lower levels.
\hline
\texttt{-e-acsl-verbose 3}& predicates- and statements-related information\\
\hline
-\texttt{-e-acsl-verbose 4 and above}& terms- and expressions-related information
+\texttt{-e-acsl-verbose 4}& terms- and expressions-related information
\\
\hline
\end{tabular}