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.
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:
- observe sets of possible values for the variables of the program at each point of the execution;
- slice the original program into simplified ones;
- navigate the dataflow of the program, from definition to use or from use to definition.
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.