Commit 64ded739 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'release/stable-23.0-vanadium' into 'master'

Fix title style event Vanadium

See merge request pub.frama-c.com!121
parents 5ed0d1fa 45d41016
...@@ -10,28 +10,28 @@ Frama-C 23.0 (Vanadium) is out. Download it [here](/fc-versions/vanadium.html). ...@@ -10,28 +10,28 @@ Frama-C 23.0 (Vanadium) is out. Download it [here](/fc-versions/vanadium.html).
Main changes with respect to Frama-C 22 (Titanium) include: Main changes with respect to Frama-C 22 (Titanium) include:
###### Kernel #### Kernel
- New `admit` annotations (which already accepted `assert` and `check`) to express hypotheses to be admitted but not verified by Frama-C - 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` - Set default machdep to `x86_64`; allow setting machdep via environment variable `FRAMAC_MACHDEP`
###### AORAI #### AORAI
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva - New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva
###### E-ACSL #### E-ACSL
- Add runtime support for Windows - Add runtime support for Windows
- Add support for loop variant - Add support for loop variant
- Add support for multiple binders in guarded quantifications - Add support for multiple binders in guarded quantifications
###### EVA #### 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 - 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 widening thresholds
- Improved automatic loop unroll - Improved automatic loop unroll
###### WP #### 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 - 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 - Bump Why3 version to 1.4.0
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment