The Frama-C platform allows checking security, verifying requirements and guaranteeing trust in C programs, thanks to a collection of collaborative plugins that perform static and dynamic analysis, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language.
Architecture
The Frama-C kernel is based on a modified version of CIL. CIL is a front-end for C that parses ISO C99 programs into a normalized representation. Frama-C extends CIL to support ACSL. This modified CIL front-end produces the C + ACSL abstract syntax tree (AST), an abstract view of the program shared among all analyzers. In addition to the AST, the kernel provides several general services.
- Messages, source code and annotations are uniformly displayed
- Parameters and command line options are homogeneously handled
- A serialization mechanism allows the user to save results of analyses and reload them later
- Projects isolate unrelated program representations, and guarantee the integrity of analyses
- Consistency mechanisms control the collaboration between analyzers
- A visitor mechanism facilitates crawling through the AST and writing code transformation plug-ins
Analyzers are developed as separate plug-ins on top of the kernel. Plug-ins are dynamically linked against the kernel to offer new analyses, or to modify existing ones. Any plug-in can register new services in a plug-in database stored in the kernel, thereby making these services available to all plug-ins.
Projects
Frama-C allows a user to work on several programs in parallel thanks to the notion of project. A project consistently stores a program with all its required information, including results computed by analyzers and their parameters. Several projects may coexist in memory at the same time. The projects are partitioned so that a modification on a particular projet does not impact the others. The project mechanism may also be used for example to perform different code transformations on the same original project, or to execute a particular analysis on the same project but with different parameters.
Collaborations across analyzers
In Frama-C, analyzers can interoperate in two different ways: either sequentially, by chaining analysis results to perform complex operations; or in parallel, by combining partial analysis results into a full program verification. The former consists in using the results of an analyzer as input to another one thanks to the plug-in database stored by the Frama-C kernel. The parallel collaboration of analyzers consists in verifying a program by heterogeneous means. ACSL is used to this end as a collaborative language: plug-ins generate program annotations, which are then validated by other plug-ins. Partial results coming from various plug-ins are integrated by the kernel to provide a consolidated status of the validity of all ACSL properties. The kernel automatically computes the validity status of each program property from the information provided by all analyzers and ensures the correctness of the entire verification process.
The main correctness property of the Frama-C kernel can be stated as: "if the consolidated status of a property is computed as valid [resp. invalid] by the kernel, then the property is valid [resp. invalid] with respect to ACSL semantics".