Information Technology Reference
In-Depth Information
alarms mutants equivalent killed % erroneous killed
fibonacci
19
27
2
25
100%
bubbleSort
15
44
2
42
100%
insertionSort
10
39
3
36
100%
binarySearch
7
38
1
37
100%
merge
5
92
5
87
100%
Fig. 10.
Error detection for mutants
instrumented by e-acsl2c and executed on each test case in order to check
at runtime if the specification was satisfied. The original programs successfully
passed all these checks. As usual, when a violation of an annotation was reported
for at least one test case, the mutant was considered to be
killed
. Fig. 10 illus-
trates the results. Except for equivalent mutants (where the mutation produced
by chance an equivalent program), all erroneous mutants were killed.
8 Related Work
Runtime Assertion Checking.
The present work is part of an extension of
Frama-C, an existing toolset for analysis of C code, for supporting runtime
assertion checking. It is therefore related to a lot of works on runtime assertion
checking [2] and, more generally, runtime verification [4]. More specifically, one
of our main objectives is to support and execute annotations in e-acsl,anex-
pressive executable specification language shared by static and dynamic analysis
tools. Hence, our work continues previous contributions to development of ex-
pressive specification languages such as Eiffel [14], JML [19] for Java and Alfa
[20] for Ada.
Memory Safety.
Since the main purpose of this paper is the support of memory-
related e-acsl annotations, our work is also related to previous efforts for en-
suring memory safety of C programs at runtime. They include safe dialects of C,
specific fail-safe C compilers and memory safety verification tools for C code. In
particular, the idea to store object metadata on valid memory blocks in a sepa-
rate database was previously exploited in [16, 21-24] and appeared well-adapted
for most spatial errors (that is, accesses outside the bounds [25]). Advantages
of this approach include relative eciency (propagation of pointer metadata at
each pointer assignment is not required) and compatibility (the memory layout
of objects is preserved). However, this technique results in significant time over-
head due to lookup operations in the database, and is not directly adapted to
detect sub-object overflows inside nested objects (e.g. an array of structures) and
temporal errors (that is, accesses to an object that has been deallocated [25]). An
alternative approach is based on pointer metadata stored inside multi-word
fat
pointers
extending the pointer representation with bounds information [26-28].
Hybrid techniques combining ideas of both approaches have been proposed as
well [29, 25]. The technique of
shadow pages
[17, 30] makes it possible to imme-
diately find stored validity information for a pointer without providing an easy
