| ... | ... | @@ -19,29 +19,35 @@ |
|
|
|
|
|
|
|
## Main changes
|
|
|
|
### Kernel
|
|
|
|
- New `admit` annotations (which already accepted `assert` and `check`) to express hypotheses to be admitted but not verified by Frama-C
|
|
|
|
- Set default machdep to `x86_64`; allow setting machdep via environment variable FRAMAC_MACHDEP
|
|
|
|
|
|
|
|
### AORAI
|
|
|
|
|
|
|
|
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva.
|
|
|
|
- The experimental AST Diff module allows to compute difference between the AST
|
|
|
|
of two projects
|
|
|
|
- significant changes in AST types that might break existing development
|
|
|
|
|
|
|
|
### E-ACSL
|
|
|
|
- Add runtime support for Windows
|
|
|
|
- Add support for loop variant
|
|
|
|
- Add support for multiple binders in guarded quantifications
|
|
|
|
|
|
|
|
- add support for Linux's pthread concurrency
|
|
|
|
|
|
|
|
### EVA
|
|
|
|
- Partial support for recursion: new option -eva-unroll-recursive-calls to
|
|
|
|
precisely analyze the n first recursive calls, before using the function
|
|
|
|
specification to interpret the remaining calls.
|
|
|
|
- Improved automatic widening thresholds
|
|
|
|
- Improved automatic loop unroll
|
|
|
|
|
|
|
|
- New public API to run the analysis and access its results, intended to replace the old API in Db.Value.
|
|
|
|
- Improved multidim domain: it is now more precise and more robust, and is able to infer simple array invariants and disjunctive struct invariants.
|
|
|
|
|
|
|
|
### WP
|
|
|
|
- New internal WP engine, fixing many issues related to control flow graph and
|
|
|
|
local variable scoping. Support for stmt contracts has been removed. Support
|
|
|
|
for looping gotos has been removed. Altough unsound, the legacy engine is
|
|
|
|
still accessible via -wp-legacy option.
|
|
|
|
- Bump Why3 version to 1.4.0
|
|
|
|
- Section « Limitation & Roadmap » added to the WP manual. |
|
|
|
|
|
|
|
- uses Why3 1.5.0
|
|
|
|
- new supported ACSL features : decreases clause and general measures for variant and decreases
|
|
|
|
- new tactics: Clear for hypothesis removal and ModMask for rewriting of mask and modulos
|
|
|
|
- removed deprecated legacy WP engine and native prover output (always use Why3)
|
|
|
|
- fixes loop invariant order and collect more hypotheses when proving them
|
|
|
|
|
|
|
|
### Ivette (New Frama-C GUI)
|
|
|
|
|
|
|
|
We are introducing Ivette, a new GUI for Frama-C.
|
|
|
|
In this preliminary version, only EVA and some of its derived plug-ins are supported.
|
|
|
|
|
|
|
|
Build & install instructions are in `ivette/INSTALL.md` from the source tarball.
|
|
|
|
To try it, simply use `ivette` in replacement of `frama-c-gui`.
|
|
|
|
Your feedback is welcome.
|
|
|
|
|
|
|
|
Have fun ! |
