Skip to content
GitLab
25.0 protected
33434c44 · Release 25.0 ·
Release Frama-C 25.0 Manganese

Main Changes since 24.0 Chromium

Kernel

  • The experimental Ast_diff module allows computing differences between the AST of two projects
  • significant changes in AST types that might break existing development

E-ACSL

  • add support for Linux's pthread concurrency

Eva

  • New public API to run the analysis and access its results, intended to replace the old API in Db.Value.
  • Improved multidim domain: it is now more precise and more robust, and is able to infer simple array invariants and disjunctive struct invariants.

WP

  • uses Why3 1.5.0
  • new supported ACSL features : decreases clause and general measures for variant and decreases
  • new tactics: Clear for hypothesis removal and ModMask for rewriting of mask and modulos
  • removed deprecated legacy WP engine and native prover output (always use Why3)
  • fixes loop invariant order and collect more hypotheses when proving them

Ivette (New Frama-C GUI)

We are introducing Ivette, a new GUI for Frama-C. In this preliminary version, only Eva and some of its derived plug-ins are supported.

Build & install instructions are in ivette/INSTALL.md from the source tarball. To try it, simply use ivette in replacement of frama-c-gui. Your feedback is welcome.