Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Frama-C 15 Phosphorus beta1
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Fri, 21 Apr 2017 16:01:46 +0200
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