Information Technology Reference
In-Depth Information
A Lesson on Runtime Assertion Checking
with Frama-C
Nikolai Kosmatov 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. This paper provides a lesson on runtime assertion checking with
Frama-C, a publicly available toolset for analysis of C programs. We
illustrate how a C program can be specified in executable specifica-
tion language e-acsl and how this specification can be automatically
translated into instrumented C code suitable for monitoring and run-
time verification of specified properties. We show how various errors can
be automatically detected on the instrumented code, including C run-
time errors, failures in postconditions, assertions, preconditions of called
functions, and memory leaks. Benefits of combining runtime assertion
checking with other Frama-C analyzers are illustrated as well.
Keywords:
runtime assertion checking, program monitoring, executable
specification, invalid pointers, Frama-C, e-acsl.
1 Introduction
Runtime assertion checking
has become nowadays a widely used programming
practice [1]. More and more practitioners and researchers are interested in ver-
ification tools allowing to automatically check specified program properties at
runtime.
Assertions
offer one of the most convenient and scalable automated
techniques for detecting errors and providing information about their locations,
even for errors that are traversed during execution but do not lead to failures.
This tutorial paper presents a lesson on runtime assertion checking using
Frama-C [2,3], an open-source platform dedicated to the analysis of C programs
and developed at CEA LIST. It has an extensible architecture organized as a
kernel with several plug-ins for individual analyses which may collaborate with
each other. Frama-C offers various analyzers [3] such as control-flow graph
construction, abstract-interpretation-based value analysis, dependency analysis,
program slicing, automatic test generation, impact analysis, proof of programs,
etc.
All static analyzers of Frama-C share a common specification language,
called acsl [4]. To bridge the gap between static and dynamic tools, a recent
work [5,6] specified e-acsl, an expressive sub-language of acsl that can be
