package frama-c-metacsl
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
MetAcsl plugin of Frama-C for writing pervasives properties
Install
Dune Dependency
Authors
Maintainers
Sources
meta-0.4.tar.gz
md5=e8e8feff1a13cdcb505d379672bbd9a9
sha512=83a51b32d84a7ade48da6f1e6a232fb4f22abebe6aae29726d46e0d35eb74230dcb649a3474a37699d3a60687a7a6916158ecc74bbe998449227989d6b0080f4
Description
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.
On This Page