frama-c-metacslversion Documentation on ocaml.org
MetAcsl plugin of Frama-C for writing pervasives properties
MetAcsl let users write properties that need to be checked at particular contexts (e.g. each time a location is written to inside a given set of functions). It will then generate all the corresponding ACSL annotations, leaving it to analysis plug-ins (e.g. WP) to prove the resulting clauses.
| Tags | program verification formal specification C plugins ACSL MetACSL |
|---|---|
| Authors | Virgile Robles, Téo Bernier and Nikolai Kosmatov |
| License | LGPL-2.1-only |
| Published | |
| Homepage | https://frama-c.com/ |
| Issue Tracker | https://git.frama-c.com/pub/meta/-/issues |
| Maintainer | Virgile.Prevosto@cea.fr |
| Dependencies | |
| Optional dependencies |
|
| Source [http] | https://git.frama-c.com/pub/meta/-/archive/0.11/meta-0.11.tar.bz2 md5=47e6ad1f070e3c8e51b59d33c904375d sha512=b8b7ba58d543b4d2b42f81071361952dc80302a836e3be6bb5c6d0f4db72f3ab358beae6ba3a524a8d40839ca5ae9bfc0be2876cbf4bccac64d046ddcd29cc4e |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/frama-c-metacsl/frama-c-metacsl.0.11/opam |
No package is dependent
