MetAcsl

Overview

MetAcsl is a plug-in dedicated to specifying and verifying high-level ACSL requirements (HILARE), that is, properties that are supposed to be checked at many points of the code base under analysis, so that writing the corresponding ACSL annotations manually would be extremely tedious and error-prone. A simple example of such a requirement would be a confidentiality property indicating that no access to a particular memory block should occur unless some clearance condition holds. Specifying that in pure ACSL would require writing an assertion for each read access in the code, while MetAcsl only needs a single HILARE.

In summary, MetAcsl defines a global ACSL extension for describing HILAREs, that are composed of three elements:

• a target: the set of functions where the HILARE should hold;

• a context: the kind of program points that are concerned by the HILARE. Two important contexts are \writing and \reading accesses;

• the property itself: it is an ACSL predicate, possibly enriched with meta-variables, depending on the context. For instance, a \writing context gives rise to a \written meta-variable denoting the location being written to.

The plug-in proceeds by generating all ACSL annotations corresponding to each HILARE. It is then possible to use one of the main analysis plug-ins of the platform (e.g. WP, E-ACSL, or Eva) to verify these annotations.

Usage

MetAcsl is available as a separate open-source plug-in, on Gitlab (more information there). It is intended to be compatible with the latest state of Frama-C’s public repository.

Since Frama-C 22.0 Titanium, there also exists a companion MetAcsl release for each Frama-C version. It is also available through opam as the frama-c-metacsl package.

Once installed, the plugin is activated by the -meta option, which will parse the meta-properties and generate the corresponding ACSL annotations.