--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on April 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C 15 Phosphorus beta1



Dear list,

I have the pleasure to announce the beta release of the next version
of Frama-C, 15 (Phosphorus). It is available in the release-candidates
branch of Frama-C-snapshot's repository on github
(https://github.com/Frama-C/Frama-C-snapshot/tree/release-candidates),
and a link to a tar.gz archive and the manuals is available at
https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-Phosphorus-20170501-beta1

You are encouraged to try it out and report any potential regression
on this list or on https://bts.frama-c.com as usual.

Barring any critical issue, final Frama-C 15 release is scheduled for mid-may.

Main changes include:
### Kernel

- E-ACSL is now included in the standard distribution
- Better handling of Variable-Length Arrays (VLA)
- ZArith is now a required dependency. Support of Big_int has been dropped
- Bash and Zsh completion for Frama-C options
- new AST nodes to explicitly mark local variable initialization

### EVA

- better set of default options
- dropped support for legacy version of Value Analysis

### WP

- Interactive Proof Editor in the GUI
- Extensible Proof Engine via Tactics and Strategies
- More powerful simplifications of goals
- Dynamic API is deprecated in favor of static API
- Fatally flawed support of generalized invariants (`-wp-invariants`)
has been dropped

### E-ACSL

- included in the standard Frama-C distribution
- use of a (much more efficient) shadow memory model by default
- much better support of unstructured control flow (complex goto, ...)

### Variadic

- translation of variadic calls is now enabled by default
- option names have changed to avoid confusion with EVA

For the Frama-C team,
-- 
E tutto per oggi, a la prossima volta
Virgile