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 is out

  • Subject: [Frama-c-discuss] Frama-C 15 Phosphorus is out
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 31 May 2017 17:34:55 +0200
Dear list,

it is with utmost pleasure that we celebrate the 200th anniversary of
the première of La Gazza Ladra by Gioachino Rossini at La Scala in
Milan by announcing the release of Frama-C 15 Phosphorus.

Main changes with respect to Frama-C 14 - Silicon 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

As usual, the complete Changelog can be found at
http://frama-c.com/changelog.html, while sources and manuals are
available at http://frama-c.com/download.html.
https://github.com/Frama-C/Frama-C-snapshot has been updated too. opam
packages should be upgraded shortly.

Please don't hesitate to try it out and provide feedback.

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