Skip to content

Frama C Phosphorus 20170501 beta1

Jump to bottom
Virgile Prevosto edited this page Apr 21, 2017 · 2 revisions

Frama-C release Phosphorus-20170501-beta1

Sources

Main changes

(see Changelog in the archive for the complete list of changes)

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

Manuals

Clone this wiki locally