Lessons Learned from Verifying Actual C Code with Frama-C
Nearly since its inception more than 15 years ago, the Frama-C C software verification platform has been used on existing code bases, in a wide variety of contexts, ranging from early assessment of a new plug-in over a small open-source library to operational deployment for formally verifying industrial applications. While the reliance on realistic case studies has been fundamental in ensuring that the development of the platform was headed in the right direction, having to cope with typical C code in the wild comes with some challenges, both scientific and technical.
In this talk, we will first briefly present Frama-C itself and its main verification plugins, as well as the ACSL formal specification language, which also aims at letting users write specifications for actual programs, and imposes as few restrictions as possible over the semantics described by the C ISO standard. Then, we will recall the main verification tasks that have been achieved with Frama-C over the years.
Finally, a large part of the talk will be dedicated to explore the various issues that arise when one sets to use Frama-C on an arbitrary piece of C code, at all stages of the process. First, the perimeter of the analysis must somehow be clearly defined (i.e. identifying external dependencies and deciding what to do with them). Then, some information must be extracted from the compilation toolchain (which macros are defined when processing which files). Only after that can we address the intricacies of the C standard, and of its main compiler-specific variants, to establish what the Frama-C's kernel should accept as legitimate C programs. Finally, some parts of C's semantics have an important impact on the design of the analysis plug-ins themselves, notably when the analyzer has to deal with the fact that any C object can also be manipulated as an array of bytes.
As a conclusion, we will propose some hindsights on currently on-going work aiming at enhancing the ability of Frama-C to be incorporated in existing software development toolchains.