frama-c-metacslversion

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
AuthorsVirgile Robles, Téo Bernier and Nikolai Kosmatov
LicenseLGPL-2.1-only
Published
Homepagehttps://frama-c.com/
Issue Trackerhttps://git.frama-c.com/pub/meta/-/issues
MaintainerVirgile.Prevosto@cea.fr
Dependencies
Optional dependencies
Source [http] https://git.frama-c.com/pub/meta/-/archive/0.8-beta/meta-0.8-beta.tar.bz2
md5=ae04d3559fba78100a5b07bf66407e8e
sha512=faeea239a1238dc344f0ca467aa9602b453832ac6f7f10d0a4f329bc1641aea77d4f425fcd2bf7a73c54def7874f9c58ef67c78c3935a0c8bb66746cfbb54cd4
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/frama-c-metacsl/frama-c-metacsl.0.8~beta/opam
No package is dependent