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:

• 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 and Wp, two deductive verification plug-ins
  These plug-ins are based on weakest precondition computation techniques. They allow 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 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:

• 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.
• Metrics calculation
  This plug-in allows the user to compute various metrics from the source code.

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 according to a user-provided criterion: it creates a copy of the program, but keeps only those parts which are necessary with respect to the given criterion.
• Spare code: remove "spare code", code that does not contribute to the final results of the program.
• E-ACSL: translate annotations into C code for runtime assertion checking.

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 verifying low-level functional specifications (inputs, outputs, dependencies,…)

For test-case generation:

• PathCrawler automatically finds test-case inputs to ensure coverage of a C function. It can be used for structural unit testing, as a complement to static analysis or to study the feasible execution paths of the function.

For concurrent programs:

• Mthread
  This plug-in automatically analyzes concurrent C programs, using the Value analysis, taking into account all possible thread interactions. At the end of its execution, the concurrent behavior of each thread is over-approximated, resulting in precise information about shared variables, which mutex protects a part of the code, etc.

External plugins

A list of plugins developed outside of the Frama-C team is available on the 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, 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.