--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on May 2017 ---
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