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
Sources
frama-c-metacsl-0.1.tar.gz
md5=74e2a596816520793abc8c1266057520
sha256=95c35a9a21591aeb46a6955e7a7104b8cd359f907d35e9d1a1e38c2ed29aa5fb
sha512=10f317e32afc606390681a7e8091f48cb8141b75947c9f40e7203a30a1b6effe7038a8939f283ef8d69650c4e285865cafae75d3e6992fcc45942e56fcafd699
Dependencies
why3
>= "1.3.1"
frama-c
>= "22.0" & < "23.0"
ocaml
>= "4.05.0" & (< "4.08.0~" | >= "4.08.1")
Reverse Dependencies