diff --git a/_events/metacsl-0.4.md b/_events/metacsl-0.4.md new file mode 100644 index 0000000000000000000000000000000000000000..58be57ac580dbbc4160065199e03fda915589f84 --- /dev/null +++ b/_events/metacsl-0.4.md @@ -0,0 +1,15 @@ +--- +layout: default +date: 09-12-2022 +short_title: MetAcsl 0.4 +title: MetAcsl for Frama-C 26.0 Iron +link: /fc-plugins/metacsl.html +--- + +Following the release of Frama-C 26.0 (Iron), [MetAcsl](/fc-plugins/metacsl.html) [v0.4](https://git.frama-c.com/pub/meta/-/releases/0.4) is out. The corresponding `opam` package should be available soon. + +MetAcsl intends to provide simple and compact ways to express properties that +would demand peppering the code with thousands of annotations in plain ACSL. +Its main use cases focus on security properties (notably ensuring that +write and read accesses to sensitive memory locations are guarded appropriately). +Feel free to consult its [homepage](/fc-plugins/metacsl.html) for more information. diff --git a/_fc-plugins/metacsl.md b/_fc-plugins/metacsl.md index 4cc79626255e16b0093551ee4ce9732f1a82e050..e732c904cc35595e8f8d7d99bdbdb19c73f9a6bf 100644 --- a/_fc-plugins/metacsl.md +++ b/_fc-plugins/metacsl.md @@ -45,8 +45,7 @@ verify these annotations. MetAcsl is available as a separate open-source plug-in, on [Gitlab](https://git.frama-c.com/pub/meta) (more information there). It is intended to be compatible with the latest state of [Frama-C's public repository](https://git.frama-c.com/pub/frama-c). -For installing the plug-in against the stable version Frama-C 22.0 Titanium, -there also exists a companion [MetAcsl 0.1 release](https://git.frama-c.com/pub/meta/-/releases/0.1). It is also available through `opam` as the +Since Frama-C 22.0 Titanium, there also exists a companion [MetAcsl release](https://git.frama-c.com/pub/meta/-/releases/) 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.