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.
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.