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

Two heavyweight plug-ins that are used by the other plug-ins are the value analysis plug-in and the weakest precondition plug-in:

• Value analysis
  This plug-in computes variation domains for variables. It is quite automatic, although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses abstract interpretation techniques.
• Jessie, the deductive verification plug-in
  This plug-in is based on weakest precondition computation techniques. It allows to prove that C functions satisfy their specification as expressed in ACSL. These proofs are modular: the specifications of the called functions are used to establish the proof without looking at their code.

The availability of the above two 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:

• Impact analysis
  This plug-in highlights the locations in the source code that are impacted by a modification.
• Scope & Data-flow browsing
  This plug-in allows the user to navigate the dataflow of the program, from definition to use or from use to definition.
• Variable occurrence browsing
  Also provided as a simple example for new plug-in development, this plug-in allows the user to reach the statements where a given variable is used.

For code transformation:

• Semantic constant folding
  This plug-in makes use of the results of the value analysis to replace in the source code the constant expressions by their values. Because it relies on the value analysis, it is able to do more of these simplifications than a syntactic analysis would.
• Slicing: This plug-in slices the code. The slicing plug-in creates a copy of the program, but keeps only those parts which are necessary for one particular computation.
• Spare code: remove "spare code", code that does not contribute to the final results of the program.

For verifying functional specifications:

• Aoraï: verify specifications expressed as LTL (Linear Temporal Logic) formulas
• Other functionalities documented together with the value analysis plug-in can be considered as low-level functional specifications (inputs, outputs, dependencies,…)

Writing new plug-ins

If you are a researcher in the field of static 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, the value analysis 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:

• a custom plug-in can emit very specific queries for the existing plug-ins, and in this way obtain information which is not directly available through the normal user interface;
• a custom plug-in has more latitude for finely tuning the behavior of the existing analyses;
• some analyses may offer specific opportunities for extension.

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.