Information Technology Reference
In-Depth Information
An Optimized Memory Monitoring for Runtime
Assertion Checking of C Programs
Nikolai Kosmatov, Guillaume Petiot, and Julien Signoles
CEA, LIST, Software Reliability Laboratory, PC 174, 91191 Gif-sur-Yvette France
firstname.lastname@cea.fr
Abstract.
Runtime assertion checking provides a powerful, highly au-
tomatizable technique to detect violations of specified program proper-
ties. However, monitoring of annotations for pointers and memory lo-
cations (such as being valid, initialized, in a particular block, with a
particular offset, etc.) is not straightforward and requires systematic in-
strumentation and monitoring of memory-related operations.
This paper describes the runtime memory monitoring library we devel-
oped for execution support of e-acsl, executable specification language
for C programs offered by the Frama-C platform for analysis of C code.
We present the global architecture of our solution as well as various op-
timizations we realized to make memory monitoring more e
cient. Our
experiments confirm the benefits of these optimizations and illustrate
the bug detection potential of runtime assertion checking with e-acsl.
Keywords:
runtime assertion checking, memory monitoring, executable
specification, invalid pointers, memory-related errors, Frama-C, e-acsl.
1 Introduction
Memory related errors, including invalid pointers, out-of-bounds memory ac-
cesses, uninitialized variables and memory leaks, are very common. For exam-
ple, the study for IBM MVS software in [1] reports that about 50% of detected
software errors were related to pointers and array accesses. This is particularly
an issue for a programming language like C that is paradoxically both the most
commonly used for development of system software with various critical com-
ponents, and one of the most poorly equipped with adequate protection mech-
anisms. The C developer is responsible for correct allocation and deallocation
of memory, pointer dereferencing and manipulation (like casts, offsets, etc.), as
well as for the validity of indices in array accesses.
Among the most useful techniques for detecting and locating software er-
rors,
runtime assertion checking
is now a widely used programming practice [2].
Turing advocated the use of assertions already in 1949 and wrote that “the
programmer should make a number of definite assertions which can be checked
individually, and from which the correctness of the whole program easily follows”
[3]. A lot of research works have addressed ecient techniques and tools for run-
time assertion checking. Leucker and Schallhart provide a survey on
runtime
