frama-c-metacsl

MetACSL plugin of Frama-C for writing pervasives properties
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.

Install
Published
08 Jan 2022
Sources
frama-c-metacsl-0.2.tar.gz
md5=12ebc297fae1405a498d1b508970d682
sha256=5fb259f3ffce9c9174d611271bef7af64fb8e354c618e6f3b6e559d26fd15e32
sha512=3a0916baef02622528b43e1a6df73074ffc1ebecb9a444e3a6593f0d0487b366196eda8b00b9d498888e5a61de996de435a1a27f1e3d2d3810f56470d9f8a8ae
Dependencies
why3
>= "1.3.1"
frama-c
>= "24.0" & < "25.0~"
ocaml
>= "4.08.1"
Reverse Dependencies