|
|
# Frama-C release Phosphorus-20170501-beta1
|
|
|
## Sources
|
|
|
- [Frama-C-Phosphorus-20170501-beta1.tar.gz](downloads/frama-c-Phosphorus-20170501-beta1.tar.gz)
|
|
|
|
|
|
## 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
|
|
|
- [user-manual](manuals/user-manual-Phosphorus-20170501-beta1.pdf)
|
|
|
- [acsl-implementation](manuals/acsl-implementation-Phosphorus-20170501-beta1.pdf)
|
|
|
- [value-analysis](manuals/value-analysis-Phosphorus-20170501-beta1.pdf)
|
|
|
- [plugin-development-guide](manuals/plugin-development-guide-Phosphorus-20170501-beta1.pdf)
|
|
|
- [rte-manual](manuals/rte-manual-Phosphorus-20170501-beta1.pdf)
|
|
|
- [wp-manual](manuals/wp-manual-Phosphorus-20170501-beta1.pdf)
|
|
|
- [metrics-manual](manuals/metrics-manual-Phosphorus-20170501-beta1.pdf)
|
|
|
- [aorai-manual](manuals/aorai-manual-Phosphorus-20170501-beta1.pdf)
|
|
|
- [e-acsl-manual](manuals/e-acsl-manual_Phosphorus-20170501-beta1.pdf)
|
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation_Phosphorus-20170501-beta1.pdf)
|
|
|
- [e-acsl](manuals/e-acsl_Phosphorus-20170501-beta1.pdf) |