package frama-c-metacsl

  1. Overview
  2. No Docs
MetACSL plugin of Frama-C for writing pervasives properties

Install

Dune Dependency

Authors

Maintainers

Sources

frama-c-metacsl-0.1.tar.gz
md5=74e2a596816520793abc8c1266057520
sha256=95c35a9a21591aeb46a6955e7a7104b8cd359f907d35e9d1a1e38c2ed29aa5fb
sha512=10f317e32afc606390681a7e8091f48cb8141b75947c9f40e7203a30a1b6effe7038a8939f283ef8d69650c4e285865cafae75d3e6992fcc45942e56fcafd699

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.

Dependencies (3)

  1. why3 >= "1.3.1"
  2. frama-c >= "22.0" & < "23.0"
  3. ocaml >= "4.05.0" & (< "4.08.0~" | >= "4.08.1")

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.