kernel.html

---
layout: feature
css: plugin
title: Kernel & Plugins - Frama-C
active: 2
---

<p>The Frama-C platform allows checking security, verifying requirements and
  guaranteeing trust in C programs, thanks to a collection of collaborative
  <a href="/html/kernel-plugin.html">plugins</a> 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 href="/html/acsl.html">a common specification language</a>.  
</p>

<h1>Architecture</h1>
<p>The Frama-C kernel is based on a modified version of
  <a href="https://link.springer.com/chapter/10.1007/3-540-45937-5_16">CIL</a>.
  CIL is a front-end for C that parses ISO C99 programs into a normalized
  representation. Frama-C extends CIL to support
  <a href="/html/acsl.html">ACSL</a>.
  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.
</p>

<ul>
<li>Messages, source code and annotations are uniformly displayed</li>
<li>Parameters and command line options are homogeneously handled</li>
<li>A serialization mechanism allows the user to save results of analyses
  and reload them later</li>
<li>Projects isolate unrelated program representations, and guarantee the
  integrity of analyses</li>
<li>Consistency mechanisms control the collaboration between analyzers</li>
<li>A visitor mechanism facilitates crawling through the AST and writing code
  transformation plug-ins</li>
</ul>

<p>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.
</p>

<h1>Projects</h1>
<p>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.
</p>

<h1>Collaborations across analyzers</h1>

<p>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.
</p>
<p>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".
</p>