provides.tex

\chapter{What the Plug-in Provides}

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} % <<<
\label{sec:simple}

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 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 \texttt{first.i} consists of adding \shortopt{e-acsl} option
to the \framac command line:
\begin{shell}
\$ frama-c -e-acsl first.i
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
<skip a warning when translating the Frama-C libc>
[e-acsl] translation done in project "e-acsl".
\end{shell}

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}:

\input{examples/instrumented_first.i}

As you can see, the generated code contains additional type declarations,
constant declarations and global \acsl annotations not present in the initial
file \texttt{first.i}. They are part of the \eacsl monitoring library. You can
safely ignore them for now. The translated \texttt{main} function of
\texttt{first.i} is displayed at the end. After each \eacsl annotation,
a call to \texttt{\_\_e\_acsl\_assert}\codeidx{e\_acsl\_assert} has been added.

\begin{minipage}{\linewidth}
\begin{ccode}
  /*@ assert x == 0; */
  __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
  /*@ assert x == 1; */
  __e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
\end{ccode}
\end{minipage}

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}

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}

\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 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}
\$ ./monitored_first
Assertion failed at line 4 in function main.
The failing predicate is:
x == 1.
Aborted
\$ echo \$?
134
\end{shell}
The execution aborts with a non-zero exit code (134) and an error message
indicating \eacsl annotation that has been violated. There is no output for the
valid \eacsl annotation. That is, the run of an executable generated from the
instrumented source file (i.e., \texttt{monitored\_first.i}) detects that the
second annotation in the initial program is invalid, whereas the first
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}

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.

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
the one assumed by \framac. You should take care of that when running the \eacsl
plug-in and when compiling the generated code with \gcc. In this aspect, the
plug-in offers a few possibilities of customization.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Runtime Errors in Annotations}
\label{sec:runtime-error}
\index{Runtime Error}

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 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 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}.

Accordingly, the \eacsl plug-in prevents an undefined term from being
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.

\listingname{rte.i}
\cinput{examples/rte.i}

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}
\$ e-acsl-gcc.sh -c -omonitored_rte.i -Orte rte.i
\end{shell}

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.e-acsl
RTE failed at line 5 in function is_dividable.
The failing predicate is:
division_by_zero: y != 0.
Aborted
\end{shell}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\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
\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 used by the analyzed program are still not defined
  in the \framac libc; or
\item your system libc and the \framac libc mismatch about several function
  types (for instance, your system libc is not 100\% POSIX compliant); or
\item several \framac lib functions get a contract and you are not interested in
  verifying them (for instance, only checking undefine behaviors matters).
\end{itemize}

\begin{important} \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 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.

\listingname{gmp.i}
\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.  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:

\begin{shell}
\$ 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.

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.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Memory-related Annotations}
\label{sec:memory}

The \eacsl plug-in handles memory-related annotations such as
\lstinline|\valid|.  Consider for instance the following program.

\listingname{valid.c}
\cinput{examples/valid.c}

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}
\$ 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}

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}
\$ e-acsl-gcc.sh -mbittree -c -Ovalid valid.c
\end{shell}
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}
\$ 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.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Debug Libraries}
\label{sec:runtime-debug}

\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.

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}
\$ rte_debug.e-acsl
Assertion failed at line 2 in function foo.
The failing predicate is:
\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}

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.  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:

\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, (we reuse the initial example
\texttt{first.i} of this manual).

\begin{shell}
\$ 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.
The verified predicate was: `x == 1'.
\end{shell}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\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.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Programs without Main}
\label{sec:no-main}
\index{Program!Without 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}

The instrumented code is generated as usual, even though you get an additional
warning.
\begin{shell}
\$ e-acsl-gcc.sh no_main.i -omonitored_no_main.i
<skip preprocessing command line>
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
                  Please use option `-main' for specifying a valid entry point.
                  The generated program may miss memory instrumentation.
                  if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
\end{shell}

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 link it against additional files such as
the following:

\listingname{main.c}
\cinput{examples/main.c}

\begin{shell}
\$ 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}

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}

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.
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}

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.

\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}
\$ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i
\$ ./no_code.e-acsl
Postcondition failed at line 5 in function my_pow.
The failing predicate is:
\old(n % 2 == 0) ==> \result >= 1.
Aborted
\end{shell}

The execution of the corresponding binary fails at runtime: actually, our
implementation of the function \texttt{my\_pow} overflows in case of large
exponentiations.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\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 \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
analysis tools.

Another way to combine \eacsl with other plug-ins is to run \eacsl last.  For
instance, the \rte plug-in~\cite{rte} may be used to generate annotations
corresponding to runtime errors. Then the \eacsl plug-in may generate an
instrumented program to verify that there are no such runtime errors during the
execution of the program.

Consider the following program.

\listingname{combine.i}
\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
          -ocode monitored_combine.i
\$ e-acsl-gcc.sh -C -Ocombine  monitored_combine.i
\$ ./combine.
\end{shell}

Automatic assertion generation can also be enabled via \eacslgcc directly via
the following command:
\begin{shell}
\$ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all
\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
\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
\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.
\begin{shell}
\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
          -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-last -print -ocode monitored_combine.i
\$ frama-c -rte combine.i -then -val -then -e-acsl \
          -then-last -print -ocode monitored_combine.i
\end{shell}
In the first case, that is because it is explicitly required by the option
\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} % <<<
\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 \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.
[e-acsl] 0 annotation was ignored, being untypable.
[e-acsl] 1 annotation was ignored, being unsupported.
\end{shell}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
\section{Verbosity Policy} % <<<
\label{sec:verbose}

By default, \eacsl does not provide much information when it is running. Mainly,
it prints a message when it begins the translation, and another one when the
translation is done. It may also display warnings when something requires the
attention of the user, for instance if it is not able to translate an
annotation. Such information is usually enough but, in some cases, you might
want to get additional control on what is displayed. As quite usual with
\framac plug-ins, \eacsl offers two different ways to do this: the verbosity
level which indicates the \emph{amount} of information to display, and the
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 \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
\shortopt{e-acsl-verbose 0}& only warnings and errors\\
\hline
\shortopt{e-acsl-verbose 1}& beginning and ending of the translation\\
\hline
\shortopt{e-acsl-verbose 2}& different parts of the translation and
  functions-related information\\
\hline
\shortopt{e-acsl-verbose 3}& predicates- and statements-related information\\
\hline
\shortopt{e-acsl-verbose 4}& terms- and expressions-related information
\\
\hline
\end{tabular}
\end{center}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Message Categories}

The kind of information to display is settable by the option
\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}
\begin{tabular}{|l|l|}
\hline
analysis & minimization of the instrumentation for memory-related annotation
(section~\ref{sec:memory}) \\
\hline
duplication & duplication of functions with contracts
(section~\ref{sec:no-code}) \\
\hline
translation & translation of an annotation into \C code\\
\hline
typing & minimization of the instrumentation for integers
(section~\ref{sec:integers}) \\
\hline
\end{tabular}
\end{center}
% >>>