Using Frama-C to grasp source code internals

The C language has been in use for a long time, and numerous programs today make use of C routines. This ubiquity is due to historical reasons, and to the fact that C is well adapted for a significant number of applications (e.g. embedded code). However, the C language exposes many notoriously awkward constructs.

precise analyses
despite the pitfalls of C

Many Frama-C plug-ins are able to reveal what the analyzed C code actually does. Equipped with Frama-C, you can:

Proving formal properties for critical software

Frama-C allows to verify that the source code complies with a provided formal specification. Functional specifications can be written in a dedicated language, ACSL. The specifications can be partial, concentrating on one aspect of the analyzed program at a time.

The most structured sections of your existing design documents can also be considered as formal specifications. For instance, the list of global variables that a function is supposed to read from or write to is a formal specification. Frama-C can compute this information automatically from the source code of the function, allowing you to verify that the code satisfies this part of the design document, faster and with less risks than a code review.