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 ACSL MetACSL
AuthorVirgile Robles
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/uploads/deea5fb23305cdfa62976bec2cbce45c/frama-c-metacsl-0.1.tar.gz
md5=74e2a596816520793abc8c1266057520
sha256=95c35a9a21591aeb46a6955e7a7104b8cd359f907d35e9d1a1e38c2ed29aa5fb
sha512=10f317e32afc606390681a7e8091f48cb8141b75947c9f40e7203a30a1b6effe7038a8939f283ef8d69650c4e285865cafae75d3e6992fcc45942e56fcafd699
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/frama-c-metacsl/frama-c-metacsl.0.1/opam
No package is dependent