From 34e60bcaba6c403b5e25a855b9e773c5c26a7f42 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 22 Feb 2018 13:24:28 +0100
Subject: [PATCH] [userman] update and document new options
---
src/plugins/e-acsl/doc/Changelog | 2 +-
src/plugins/e-acsl/doc/userman/biblio.bib | 2 +-
src/plugins/e-acsl/doc/userman/changes.tex | 14 +-
.../doc/userman/examples/instrumented_first.c | 54 +++
.../doc/userman/examples/instrumented_first.i | 61 ----
.../e-acsl/doc/userman/examples/printf.c | 6 +
.../e-acsl/doc/userman/examples/strcpy.c | 8 +
.../e-acsl/doc/userman/introduction.tex | 2 +-
src/plugins/e-acsl/doc/userman/macros.tex | 4 +-
src/plugins/e-acsl/doc/userman/provides.tex | 309 +++++++++---------
10 files changed, 240 insertions(+), 222 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
delete mode 100644 src/plugins/e-acsl/doc/userman/examples/instrumented_first.i
create mode 100644 src/plugins/e-acsl/doc/userman/examples/printf.c
create mode 100644 src/plugins/e-acsl/doc/userman/examples/strcpy.c
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index d1bdd8f17b4..c9cfb7651e5 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -23,7 +23,7 @@
replace a few libc functions by built-ins that efficiently
detects when they are incorrectly called.
- E-ACSL [2018/02/21] New option -e-acsl-validate-format-strings to
- detect format string errors.
+ detect format string errors in printf-like functions.
-* E-ACSL [2018/02/21] Correct support of variable-length array
(fix bug #1834).
-* runtime [2018/02/16] Function __e_acsl_offset now returns size_t.
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index ff5bdf6668e..3a444b97790 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -14,7 +14,7 @@
note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
}
-@manual{value,
+@manual{eva,
author = {David B\"uhler and Pascal Cuoq and Boris Yakobowski and
Matthieu Lemerre and André Maroneze and Valentin Perelle and
Virgile Prevosto},
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 8b0dca325e5..af68ce7761d 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -3,7 +3,19 @@
This chapter summarizes the changes in this documentation between each \eacsl
release. First we list changes of the last release.
-\section*{E-ACSL \eacslversion}
+\begin{itemize}
+\item New section \textbf{Additional Verifications}.
+\item Update each section with respect to the changes introduced since \eacsl
+ Sulfur-20180101.
+\end{itemize}
+
+\section*{E-ACSL Sulfur-20180101}
+
+\begin{itemize}
+\item no changes
+\end{itemize}
+
+\section*{E-ACSL Phosphorus-20170501}
\begin{itemize}
\item Removed chapter \textbf{Easy Instrumentation with E-ACSL}.
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
new file mode 100644
index 00000000000..a940f8c891f
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
@@ -0,0 +1,54 @@
+\begin{shell}
+\$ frama-c -e-acsl first.i -then-last -print
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[kernel] Parsing first.i (no preprocessing)
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+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];
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ requires pred != 0;
+ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred, char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_init(int *argc_ref,
+ char ***argv,
+ size_t ptr_size);
+
+extern size_t __e_acsl_heap_allocation_size;
+
+/*@
+predicate diffSize{L1, L2}(integer i) =
+ \at(__e_acsl_heap_allocation_size,L1) -
+ \at(__e_acsl_heap_allocation_size,L2) == i;
+
+*/
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
+ int x = 0;
+ /*@ assert x == 0; */
+ __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
+ 3);
+ /*@ assert x == 1; */
+ __e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",
+ 4);
+ __retres = 0;
+ return __retres;
+}
+\end{shell}
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.i b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.i
deleted file mode 100644
index e777ec7e041..00000000000
--- a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.i
+++ /dev/null
@@ -1,61 +0,0 @@
-\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/printf.c b/src/plugins/e-acsl/doc/userman/examples/printf.c
new file mode 100644
index 00000000000..21ca4893ca9
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/printf.c
@@ -0,0 +1,6 @@
+#include <stdio.h>
+
+int main(void) {
+ printf("is %d really an int?", "foo");
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/examples/strcpy.c b/src/plugins/e-acsl/doc/userman/examples/strcpy.c
new file mode 100644
index 00000000000..40e530a2b30
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/strcpy.c
@@ -0,0 +1,8 @@
+#include <stdlib.h>
+#include <string.h>
+
+int main(void) {
+ char *dst = malloc(sizeof(char) * 6);
+ strcpy(dst, "foobar");
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index bad13d56f7d..03e8b405449 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -23,7 +23,7 @@ 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 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}.
+\Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}.
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
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index 3ccfbd99b5b..c53111f88fe 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -11,13 +11,13 @@
\newcommand{\rte}{\textsc{RTE}\xspace}
\newcommand{\C}{\textsc{C}\xspace}
\newcommand{\jml}{\textsc{JML}\xspace}
-\newcommand{\valueplugin}{\textsc{Value}\xspace}
+\newcommand{\Eva}{\textsc{Eva}\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{\dlmalloc}{\textsc{dlmalloc}\xspace}
\newcommand{\nodiff}{\emph{No difference with \acsl.}}
\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 2d91a08d34a..52b8769b6cd 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -66,7 +66,7 @@ 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}
+\input{examples/instrumented_first.c}
As you can see, the generated code contains additional type declarations,
constant declarations and global \acsl annotations not present in the initial
@@ -99,7 +99,7 @@ Section~\ref{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
+\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c
\end{shell}
\framac uses architecture-dependent configuration which
@@ -115,60 +115,22 @@ 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:
+\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
+ -print -ocode monitored_first.c
\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:
+This file can be compile with a \C compiler (for instance \gcc), as follows:
\lstset{escapechar=£}
\begin{shell}
-\$ gcc monitored_first.i -omonitored_first \
- -leacsl-rtl-bittree -leacsl-gmp -leacsl-jemalloc -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__));
+\$ gcc -c -Wno-attributes monitored_first.c
\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. The monitored executable is also linked
-against the customized versions of the \jemalloc memory allocator
-(\T{-leacsl-jemalloc}) and the \gmp library (\T{-leacsl-gmp}) used by \eacsl.
-Even though in this example they are not strictly needed (since the transformed
-executable neither tracks memory nor reasons about arbitrary precision
-integers) we show all libraries potentially used by a transformed executable
-for completeness purposes. We describe the 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.
+However, creating an executable through a proper invokation to \gcc is painful
+and is not documented. Instead, \eacsl comes with a companion wrapper script for
+this purpose.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -176,12 +138,6 @@ 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
@@ -220,6 +176,24 @@ instruments the code in \texttt{first.i}, outputs it to
\texttt{first.i}, while \texttt{a.out.e-acsl} is an executable compiled from
\texttt{monitored\_first.i} generated by \eacsl.
+You can execute the generate binaries, in particular \texttt{a.out.e-acsl} which
+detects at runtime the incorrect annotation.
+\begin{shell}
+\$ ./a.out.e-acsl
+Assertion failed at line 4 in function main.
+The failing predicate is:
+x == 1.
+Aborted
+\$ 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.
+
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
@@ -342,28 +316,10 @@ For full up-to-date documentation of \eacslgcc see its man page:
\$ man e-acsl-gcc.sh
\end{shell}
-A brief listing of the basic options of \eacslgcc
-can be viewed using its \shortopt{h} option:
+Alternatively, you can also use the \shortopt{h} option of \eacslgcc:
\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]
+ \$ man e-acsl-gcc.sh -h
\end{shell}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -540,31 +496,13 @@ Memory tracking implemented by the \eacsl library comes in two flavours dubbed
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.
-
-Both libraries use the same API and differ only in implementation, therefore it
-is 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}.
-
-The \eacsl libraries allocate heap memory using a customized version of the
-\jemalloc\footnote{\url{http://jemalloc.net/}} memory allocator replacing
+is based on shadow memory~\cite{pldi16}. The functionality of the provided
+memory models is equivalent, however they differ in performance. We further
+discuss performance considerations.
+
+The \eacsl models allocate heap memory using a customized version of the
+\dlmalloc\footnote{\url{http://dlmalloc.net/}} memory allocator replacing
system-wide \T{malloc} and similar functions (e.g., \T{calloc} or \T{free}).
-Mathematical integers used by \eacsl are implemented using a customized version
-of the \gmp library. Both, \jemalloc and \gmp should be added at link time as
-shown in Section~\ref{sec:exec}. We, however, recommend using \eacslgcc who
-adds necessary compile- and link-time dependencies and allows for easy
-switching between different memory models as discussed below.
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
@@ -588,7 +526,7 @@ 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.
+Unless specified, \eacsl defaults to the segment-based memory model.
\subsubsection{Performance Considerations}
\label{sec:perf}
@@ -615,62 +553,61 @@ 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{Debug Libraries}
+%% \label{sec:runtime-debug}
+
+%% \eacsl memory models mentioned in Section~\ref{sec:memory} 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.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -728,6 +665,68 @@ Assertion at line 4 in function main is invalid.
The verified predicate was: `x == 1'.
\end{shell}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
+\section{Additional Verifications} % <<<
+
+In addition to checking annotations at runtime, \eacsl is able to detect a few
+errors at runtime.
+
+\subsection{Format String Vulnerabilities}
+\index{Format String Vulnerabilities}
+
+Whenever option \longopt{validate-format-strings} of \eacslgcc is set, \eacsl
+detects format-string vulnerabilities in \texttt{printf}-like function. Below is
+an example which incorrectly tries to print a string through a \texttt{\%d}
+format.
+
+\listingname{printf.c}
+\cinput{examples/printf.c}
+
+This error can be detected by \eacsl as follows.
+
+\begin{shell}
+\$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings printf.c
+\$ ./printf.e-acsl
+printf: directive 1 ('%d') expects argument of type 'int' but the corresponding
+argument has type 'char*'
+Abort
+\end{shell}
+
+\subsection{Incorrect Usage of Libc Functions}
+\index{Libc}
+
+Whenever option \longopt{libc-replacements} of \eacslgcc is set, \eacsl is
+able to detect incorrect usage of the following libc functions:
+\begin{itemize}
+\item \texttt{memcmp}
+\item \texttt{memcpy}
+\item \texttt{memmove}
+\item \texttt{memset}
+\item \texttt{strcat}
+\item \texttt{strncat}
+\item \texttt{strcmp}
+\item \texttt{strcpy}
+\item \texttt{strncpy}
+\item \texttt{strlen}
+\end{itemize}
+
+For instance, the program below incorrectly uses \texttt{strcpy} because the
+destination string should contain at least 7 \texttt{char} (and not only 6).
+
+\listingname{strcpy.c}
+\cinput{examples/strcpy.c}
+
+This error can be reported by \eacsl as follows.
+
+\begin{shell}
+\$ e-acsl-gcc.sh -Ostrcpy -c --libc-replacements strcpy.c
+\$ ./strcpy.e-acsl
+strlen: insufficient space in destination string, at least 7 bytes required
+Abort
+\end{shell}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
@@ -894,7 +893,7 @@ known in this new project. If you want to keep them, you have to set the option
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
+\shortopt{e-acsl-valid}. For instance, \Eva~\cite{eva} 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.
--
GitLab