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.tar.bz2
md5=7efd0ca166d8bd6df1d522ca246fda4b
sha512=24f67db46bf50b04e34da4d7e30d6ed34c1b3ad18e11913f596fb1b227d21a49b12bb8bee52fdc35c79c8363f19cbeed7d9183f19e02a25a2fb09f379ccfd51d
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