Information Technology Reference
In-Depth Information
be also due to the incapacity of the proving tool to find the proof automatically.
Proof failures have to be analyzed and fixed manually.
Runtime assertion checking provides an automatic technique allowing the val-
idation engineer to check the conformance between program and specification at
runtime on a number of program executions. The instrumented program can be
executed on an available test suite, or generated test inputs (e.g. randomly, or
by a structural test generation tool like PathCrawler [14], another Frama-C
plug-in). Runtime checking does not give a precise answer in all cases, but it
can provide a useful indication. When a failure is detected at runtime, the failed
annotation and the corresponding program inputs indicate the case that has not
been properly taken into consideration in the implementation or in the specifi-
cation. The engineer can immediately deduce that the proof failure is not due to
the limitations of the prover. For example, if the postcondition of the program
of Fig. 2a were erroneously written as
ensures
(x >= 0 &&
\result
== x) && (x < 0 &&
\result
== -x);
or as
ensures
(x >= 0 &&
\result
== x) || (x < 0 &&
\result
== x);
the failure would be detected on a concrete program input as illustrated in
Sec. 3.2. Although the specification error is obvious for this simple example,
automatic runtime checking can save significant time for more complex programs.
When no failure is detected at runtime, the prover may need additional an-
notations (e.g. assertions, loop invariants), so the specification effort is worth to
be continued (even if the risk of an error cannot be completely excluded since
runtime checking was performed only on a final set of tests).
5 Combinations with Other Analyzers
Frama-C is a platform which provides a wide variety of plug-ins. The e-acsl
plug-in is only one of them. It is possible to make e-acsl more ecient by com-
bining it with other existing plug-ins. Section 5.1 explains how to automatically
generate annotations to be checked by e-acsl, while Section 5.2 shows how to
reduce the number of dynamic checks by verifying some of them statically.
5.1 Generating Annotations Automatically
The e-acsl plug-in may be used to dynamically verify the absence of runtime
errors in C code, by combining it with the rte plug-in. Indeed, this plug-in gener-
ates e-acsl annotations preventing potential runtime errors: if these annotations
are proven valid, then we get the guarantee that the code provokes no runtime er-
ror. For instance, rte generates
/
*
@
assert \valid_read
(p);
*
/
each time a pointer
p
is read, and two assertions
/
*
@
assert
0<=i;
*
/
and
/
*
@
assert
i < 10;
*
/
each
time an access
t[i]
in an array
t
of length 10 is performed. If these annotations
are translated into C code by the e-acsl plug-in, they will be checked at runtime:
either a dynamic check fails and the program reports a clear assertion failure, or
