package frama-c-metacsl
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
On This Page
MetAcsl plugin of Frama-C for writing pervasives properties
Install
dune-project
Dependency
Authors
Maintainers
Sources
meta-0.10-beta.tar.bz2
md5=ac22be301cb2feaa8de33af7ceb6e41b
sha512=40d7381924ef486a1d2e66f34729bbb615def46d48d9ff9916bdc39250f920d5134a3af3c0bf856225de910d2bf7f92649e1e4e17615076afa9562c451a53316
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