Commit 4c6038c6 authored by Virgile Robles's avatar Virgile Robles

Update MetAcsl's description

parent f355596e
Pipeline #30931 passed with stages
in 3 minutes and 46 seconds
---
layout: plugin
title: MetAcsl
description: Verification of meta-properties
description: Verification of high-level ACSL requirements
key: specifications
distrib_mode: proto
distrib_mode: free
repo_url: https://git.frama-c.com/pub/meta
---
## Overview
MetAcsl is a plug-in dedicated to specifying and verifying
*meta-properties*, that is, properties that are supposed
*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 property would be a confidentiality property indicating
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 meta-property.
code, while MetAcsl only needs a single HILARE.
In summary, MetAcsl defines a global ACSL extension for describing
meta properties, that are composed of three things:
HILAREs, that are composed of three elements:
- a target: the set of functions where the meta-property should hold;
- a target: the set of functions where the HILARE should hold;
- a context: the kind of program points that are concerned by the
meta-property. Two important contexts are `\writing` and
HILARE. Two important contexts are `\writing` and
`\reading` accesses;
- the property itself: it is an ACSL predicate, possibly enriched
......@@ -35,13 +35,13 @@ 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 meta-property. It is then possible to use one of the main analysis
each HILARE. It is then possible to use one of the main analysis
plug-ins of the platform (e.g. [WP](wp.html),
[E-ACSL](e-acsl.html), or [Eva](eva.html)) to
verify these annotations.
## Usage
MetAcsl is available as a separate open-source plug-in, on [Gitlab](https://git.frama-c.com/pub/meta).
MetAcsl is available as a separate open-source plug-in, on [Gitlab](https://git.frama-c.com/pub/meta) (more information here).
It is intended to be compatible with the latest state of [Frama-C's public repository](https://git.frama-c.com/pub/frama-c).
Once installed, the plugin is activated by the `-meta` option, which will parse the meta-properties and generate the corresponding ACSL annotations.
\ No newline at end of file
Once installed, the plugin is activated by the `-meta` option, which will parse the meta-properties and generate the corresponding ACSL annotations.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment