Specification and Analysis of C(++) programs with Frama-C and ACSL.

D
Frama-C is a framework dedicated to build static analyzers for C
programs and make them cooperate to achieve better results. One
important component of this cooperation is the ANSI/ISO C Specification
Language (ACSL), a JML-like language allowing to formally specify the
behavior of C functions and statements. The analyses can indeed
generate verification conditions as ACSL formulas that will be taken as
input by the other ones (and hopefully discharged at some point). This
talk will first present the existing Frama-C analyses. Then, we will
have a look at the main ACSL constructions. Last, we will show how
these constructions can be used for the specification of existing code,
and how Frama-C could be extended to deal with C++.