This tutorial shows how to implement your own new C code analysis technique by leveraging existing Frama-C analysis. It is composed of two parts.

Extending Frama-C/Value

The Frama-C platform provides an abstract-interpretation-based plugin, Value. Its main feature is an automatic analysis that infers:

• an over-approximation of the possible values for all the memory locations of the program;
• all the instructions that might lead to an undefined behavior at runtime.

In former Frama-C releases, the abstract domain internally used by Value could only be changed marginally, by patching the Frama-C sources. Adding new analysis domains, typically to increase precision on a given code construct, was not possible.

Since Frama-C Aluminium, users can add their own domain to the analyzer. In its simplest form, the analyzer provides a fixpoint engine over C programs. It only requires abstract transformers for standards constructs such as assignments or conditionals. More expressive domains can however choose to inter-reduce their abstract state with the main analysis, in order to gain precision. Each domain benefits from the presence of the other one, and contributes to the global results.

In this tutorial, we present the API that must be implemented to add a new analysis domain. The communication mechanisms between domains will also be presented.

Extending Frama-C/WP

The WP plug-in of Frama-C is dedicated to proving ACSL annotation using Weakest Precondition calculus. An API is also made available to plug-in developers for launching such proofs programmatically.

However, this API also exposes reusable major building blocks that make WP so efficient. Namely:

• Wp.Lang, an instance of Qed to represent on-the-fly fully normalized first-order logic terms with a lot of built-ins theories (integers, bitwise, lists, arrays, records, memory models)
• Wp.Compilers, a collection of compilers and (extensible) memory models to interpret C and ACSL snippets into Wp.Lang terms and formula
• Wp.Conditions, a Sequent simplifier (proof obligations) that can be used to preprocess proof obligations
• Wp.Export, a collection of API to export Wp.Lang formula to SMT solvers

Those building blocks can be used to craft an efficient Frama-C plug-in based on a symbolic interpretation of C/ACSL. For instance, one might generate a path-predicate for reaching a statement and dump it to a constraint generator to obtain a counter-example. Another presented example will be how we used this API to extract a Lustre program from an embedded software main loop.

The tutorial aims at presenting an overview of this API and illustrating how it can be used to develop symbolic-based analysis inside Frama-C.