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.9-beta.tar.bz2
md5=32bd324617144e618a39e0015445effb
sha512=d96bc4fb9e4c9771efeca815aa1d6f2bae0676cce56d9ed227370bacf4fb04c0811d53470cd15981406ae11a0e95af9f16ab31f7cac04ae2a92cbf85233fb496
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