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 ACSL MetACSL |
|---|---|
| Author | Virgile Robles |
| 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/uploads/9d6ad7136916ce78965434dde5a62567/frama-c-metacsl-0.3.tar.gz md5=967ffd6ab144b426269417b65eb928c3 sha256=3b0fd8a37e4b71f6a2c4fe7c6599498480a87ae646028e1e53abf90dde224ee5 sha512=dbfd459ce2b51cb5325c8e8bcf2f28629d192017285369cf8144a13326c598503997da11764163c42585cfeb2a3ffdf59f13f5cf8e7f15fb2fc8f3c59c6fe82e |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/frama-c-metacsl/frama-c-metacsl.0.3/opam |
No package is dependent
