Skip to content
Snippets Groups Projects
Commit 7da43daa authored by Virgile Robles's avatar Virgile Robles
Browse files

MetACSL->MetAcsl. Mention the public release.

parent 3d9ac63f
No related branches found
No related tags found
No related merge requests found
Pipeline #30329 passed
--- ---
layout: plugin layout: plugin
title: MetACSL title: MetAcsl
description: Verification of meta-properties description: Verification of meta-properties
key: specifications key: specifications
distrib_mode: proto distrib_mode: proto
repo_url: https://git.frama-c.com/pub/meta
--- ---
## Overview ## Overview
MetACSL is a plug-in dedicated to specifying and verifying MetAcsl is a plug-in dedicated to specifying and verifying
*meta-properties*, that is, properties that are supposed *meta-properties*, that is, properties that are supposed
to be checked at many points of the code base under analysis, to be checked at many points of the code base under analysis,
so that writing the corresponding ACSL annotations manually so that writing the corresponding ACSL annotations manually
...@@ -17,9 +18,9 @@ of such a property would be a confidentiality property indicating ...@@ -17,9 +18,9 @@ of such a property would be a confidentiality property indicating
that no access to a particular memory block should occur unless that no access to a particular memory block should occur unless
some clearance condition holds. Specifying that in pure ACSL some clearance condition holds. Specifying that in pure ACSL
would require writing an assertion for each read access in the 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 meta-property.
In summary, MetACSL defines a global ACSL extension for describing In summary, MetAcsl defines a global ACSL extension for describing
meta properties, that are composed of three things: meta properties, that are composed of three things:
- a target: the set of functions where the meta-property should hold; - a target: the set of functions where the meta-property should hold;
...@@ -41,5 +42,6 @@ verify these annotations. ...@@ -41,5 +42,6 @@ verify these annotations.
## Usage ## Usage
As the plugin is in an early stage of development, it is currently only MetAcsl is available as a separate open-source plug-in, on [Gitlab](https://git.frama-c.com/pub/meta).
available upon request. 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment