The architecture of Frama-C

Frama-C is organized with a plug-in architecture (comparable to that of the Gimp or Eclipse). A common kernel centralizes information and conducts the analysis. Plug-ins interact with each other through interfaces defined by the kernel. This makes for robustness in the development of Frama-C while allowing a wide functionality spectrum.

Build Your
Own Plug-In
Frama-C is extensible. It contains several ready-to-use plug-ins for the static analysis of C code, but more importantly, any new plug-in may use the results or functionalities provided by the existing plug-ins. This allows very powerful plug-ins to be written with relatively little effort.

Available plug-ins

Three heavyweight plug-ins that are used by the other plug-ins:

The availability of the above three plug-ins make it possible to write additional plug-ins that provide a wide palette of possibilities with relatively little effort. Here is a non-exhaustive list of plug-ins that have already been written and are distributed with Frama-C. Note that some of these plug-ins are still in development.

For browsing unfamiliar code:

For code transformation:

For verifying functional specifications:

For test-case generation:

For concurrent programs:

External plugins

A list of plugins developed outside of the Frama-C team is available on the Frama-C wiki.

Writing new plug-ins

If you are a researcher in the field of static or dynamic analysis, using Frama-C as a testbed for your ideas is a choice to consider. You may benefit from the ready-made parser for C programs with ACSL annotations. The results of existing analyses may simplify the problems that are orthogonal to those you want to consider (in particular, EVA provides sets of possible targets of every pointer in the analyzed C program). And lastly, being available as a Frama-C plug-in increases your work's visibility among existing industrial users of Frama-C.

There are also a number of reasons for an advanced user of Frama-C to be interested in writing his own plug-in:

For developing new plug-ins: The plug-in development guide

If you intend to make your own plug-in do not hesitate to contact us for help.