Skip to content

GitLab

Commit 672baa63 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'kostyantyn/feature/format-functions' into 'master' 

Kostyantyn/feature/format functions

See merge request frama-c/e-acsl!163
parents 4f5b36bb 78777fb2
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/.gitignore
View file @ 672baa63
......@@ -56,6 +56,8 @@
/tests/test_config
/tests/runtime/*.cm*
/tests/runtime/result/*
/tests/format/result/*
/tests/builtin/result/*
/tests/temporal/result/*
/tests/special/result/*
/tests/no-main/result/*
......
src/plugins/e-acsl/Makefile.in
View file @ 672baa63
......@@ -62,6 +62,7 @@ PLUGIN_CMO:= local_config \
rte \
error \
builtins \
functions \
misc \
gmpz \
literal_strings \
......@@ -84,7 +85,6 @@ PLUGIN_CMO:= local_config \
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=yes
# We "save" this variable so that it can be used once PLUGIN_DIR has been reset
EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)
......@@ -130,7 +130,20 @@ $(EACSL_PLUGIN_DIR)/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_F
ifeq (@MAY_RUN_TESTS@,yes)
PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main full-mmodel temporal special
PLUGIN_TESTS_DIRS := \
format \
reject \
runtime \
bts \
gmp \
no-main \
full-mmodel \
temporal
# the following test suite is deactivated for the time being:
# uncompatible with OCI
# builtin
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
E_ACSL_TESTS: $(EACSL_PLUGIN_DIR)/tests/test_config
......
src/plugins/e-acsl/doc/Changelog
View file @ 672baa63
......@@ -19,6 +19,13 @@
# configure configure
###############################################################################
- E-ACSL [2018/02/21] New option -e-acsl-replace-libc-functions to
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 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.
-* E-ACSL [2018/02/07] Fix incorrect typing in presence of
comparison operators (may only be visible when directly
......
src/plugins/e-acsl/doc/userman/biblio.bib
View file @ 672baa63
......@@ -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},
......
src/plugins/e-acsl/doc/userman/changes.tex
View file @ 672baa63
......@@ -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}.
......
src/plugins/e-acsl/doc/userman/examples/instrumented_first.i → src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
View file @ 672baa63
\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_gmp_api.h (with 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;
#include "stdio.h"
#include "stdlib.h"
struct __e_acsl_mpz_struct {
int _mp_alloc ;
int _mp_size ;
......@@ -16,45 +15,39 @@ struct __e_acsl_mpz_struct {
};
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; */
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; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred, char *kind,
char *fct,
char *pred_txt,
int line);
/*@ ghost extern int __e_acsl_internal_heap; */
/*@ 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;
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;
__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);
__e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
3);
/*@ assert x == 1; */
__e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1", 4);
__e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",
4);
__retres = 0;
return __retres;
}
......
src/plugins/e-acsl/doc/userman/examples/printf.c 0 → 100644
View file @ 672baa63
#include <stdio.h>
int main(void) {
printf("is %d really an int?", "foo");
return 0;
}
src/plugins/e-acsl/doc/userman/examples/strcpy.c 0 → 100644
View file @ 672baa63
#include <stdlib.h>
#include <string.h>
int main(void) {
char *dst = malloc(sizeof(char) * 6);
strcpy(dst, "foobar");
return 0;
}
src/plugins/e-acsl/doc/userman/introduction.tex
View file @ 672baa63
......@@ -13,17 +13,17 @@ program.
\eacsl translation brings several benefits. First, it allows a user to monitor
\C code and perform what is usually referred to as ``runtime assertion
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
annotation checking'' would be more precise.}. This is the
primary goal of \eacsl. Second, it allows to combine \framac and its
existing analyzers with other \C analyzers that do not natively understand the
\acsl
specification language. Third, the possibility to detect invalid annotations
during a concrete execution may be very helpful while writing a correct
specification of a given program, \emph{e.g.} for later program proving.
Finally, an executable specification makes it possible to check assertions that
cannot be verified statically 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}.
annotation checking'' would be more precise.}. This is the primary goal of
\eacsl. Indirectly, in combination with the \rte~\cite{rte}, this usage
allows the user to detect undefined behaviors in its \C code. Second, it allows
to combine \framac and its existing analyzers with other \C analyzers that do
not natively understand the \acsl specification language. Third, the possibility
to detect invalid annotations during a concrete execution may be very helpful
while writing a correct specification of a given program, \emph{e.g.} for later
program proving. Finally, an executable specification makes it possible to
check assertions that cannot be verified statically and thus to establish a link
between runtime monitoring and static analysis tools such as
\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
......
src/plugins/e-acsl/doc/userman/macros.tex
View file @ 672baa63
......@@ -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.}}
......
src/plugins/e-acsl/doc/userman/provides.tex
View file @ 672baa63
......@@ -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.