Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
---
layout: default
date: "21-06-2022"
short_title: Frama-C 25.0 (Manganese)
title: Release of Frama-C 25.0 (Manganese)
link: /fc-versions/manganese.html
---
Frama-C 25.0 (Manganese) is out. Download it [here](/fc-versions/manganese.html).
Main changes with respect to Frama-C 24 (Chromium) include:
#### Kernel
- The experimental AST Diff module allows to compute difference 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.
Have fun !