package frama-c-metacsl

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

Install

Dune Dependency

frama-c.com Readme LGPL-2.1-only License Edit opam file Versions (7)

Authors

  1. V
    Virgile Robles
  2. T
    Téo Bernier
  3. N
    Nikolai Kosmatov

Maintainers

  1. V
    Virgile.Prevosto@cea.fr

Sources

meta-0.6.tar.bz2
md5=2b453b80f85c7b358afda6a9e3c72d26
sha512=2039616a471d0d9ecc7bc0531bc7a07bc7f91e8f48e8caecbab09bf41570f2445ae0c3e4b6e19390e0e338708886acf42c891ece7cf6df6d9e98323b4fc122b1

CHANGELOG.md.html

Version 0.6

  • compatibility with Frama-C 28.x Nickel

  • -meta-check-callee-assigns can now also be given declared functions

Version 0.5

  • compatibility with Frama-C 27.x Cobalt

  • added -meta-check-callee-assigns option (contributed by Thales Research & Technology)

Version 0.4

  • compatibility with Frama-C 26.0 Iron

  • ensure Wookey case study can be handled (with non-free ACSL-importer plug-in)

Version 0.3

  • compatibility with Frama-C 25.0 Manganese

Version 0.2

  • add warning category unknown-func which aborts by default

  • add \func meta-variables in all contexts

  • remove unused -meta-eacsl option

  • more simplification of trivial instances

  • add \called_arg family of meta-variables in \calling context

Version 0.1: first public release