package frama-c-metacsl

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

Install

Authors

Maintainers

Sources

meta-0.5.tar.bz2
md5=c2f0fd2ae9b412e16c58a5391410183f
sha512=7c738ac097a5cea1010b9dff993d40573746d85e430e9c93409c4aea7e171a7b31fec7f580c9a168dce281c9159662a7dd61fc1179f4d94f76795adc28c68ef1

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. frama-c >= "27.0~" & < "28.0~"
  2. ocaml >= "4.11.1"
  3. dune >= "3.2"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None