From 7da43daa132a8cd0ddea3e8fdba44e3dd51d9f03 Mon Sep 17 00:00:00 2001 From: Virgile Robles <virgile.robles@protonmail.ch> Date: Fri, 23 Oct 2020 09:13:21 +0200 Subject: [PATCH] MetACSL->MetAcsl. Mention the public release. --- _fc-plugins/metacsl.md | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/_fc-plugins/metacsl.md b/_fc-plugins/metacsl.md index bfe71360..136819e0 100644 --- a/_fc-plugins/metacsl.md +++ b/_fc-plugins/metacsl.md @@ -1,14 +1,15 @@ --- layout: plugin -title: MetACSL +title: MetAcsl description: Verification of meta-properties key: specifications distrib_mode: proto +repo_url: https://git.frama-c.com/pub/meta --- ## 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 to be checked at many points of the code base under analysis, so that writing the corresponding ACSL annotations manually @@ -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 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 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: - a target: the set of functions where the meta-property should hold; @@ -41,5 +42,6 @@ verify these annotations. ## Usage -As the plugin is in an early stage of development, it is currently only -available upon request. +MetAcsl is available as a separate open-source plug-in, on [Gitlab](https://git.frama-c.com/pub/meta). +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 -- GitLab