Commit 63a79d9e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

23.0-Vanadium release

parent 2c30fea8
layout: default
date: "06-07-2021"
event: Frama-C 23.0 (Vanadium)
title: Release of Frama-C 23.0 (Vanadium)
link: /fc-versions/vanadium.html
Frama-C 23.0 (Vanadium) is out. Download it [here](/fc-versions/vanadium.html).
Main changes with respect to Frama-C 22 (Titanium) include:
###### 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
###### E-ACSL
- Add runtime support for Windows
- Add support for loop variant
- Add support for multiple binders in guarded quantifications
###### 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
###### 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
\ No newline at end of file
......@@ -2,41 +2,41 @@
layout: version
number: 23
name: Vanadium
beta: true
acsl: 17
- number: 0
- name: Frama-C v23.0~rc1 Vanadium
- name: Frama-C v23.0 Vanadium
- name: Source distribution
link: /download/frama-c-23.0-rc1-Vanadium.tar.gz
link: /download/frama-c-23.0-Vanadium.tar.gz
help: Compilation instructions
help_link: /html/installations/vanadium.html
- name: User manual
link: /download/user-manual-23.0-rc1-Vanadium.pdf
link: /download/user-manual-23.0-Vanadium.pdf
- name: Plug-in development guide
link: /download/plugin-development-guide-23.0-rc1-Vanadium.pdf
link: /download/plugin-development-guide-23.0-Vanadium.pdf
help: Hello plug-in tutorial archive
help_link: /download/hello-23.0-rc1-Vanadium.tar.gz
help_link: /download/hello-23.0-Vanadium.tar.gz
- name: API Documentation
link: /download/frama-c-23.0-rc1-Vanadium-api.tar.gz
- name: ACSL 1.16 (Vanadium implementation)
link: /download/acsl-implementation-23.0-rc1-Vanadium.pdf
link: /download/frama-c-23.0-Vanadium-api.tar.gz
- name: ACSL 1.17 (Vanadium implementation)
link: /download/acsl-implementation-23.0-Vanadium.pdf
- name: Plug-in Manuals
sort: true
- name: Aoraï manual
link: /download/aorai-manual-23.0-rc1-Vanadium.pdf
link: /download/aorai-manual-23.0-Vanadium.pdf
help: Aoraï example
help_link: /download/aorai-example-23.0-rc1-Vanadium.tgz
help_link: /download/aorai-example-23.0-Vanadium.tgz
- name: Metrics manual
link: /download/metrics-manual-23.0-rc1-Vanadium.pdf
link: /download/metrics-manual-23.0-Vanadium.pdf
- name: Rte manual
link: /download/rte-manual-23.0-rc1-Vanadium.pdf
link: /download/rte-manual-23.0-Vanadium.pdf
- name: Eva manual
link: /download/eva-manual-23.0-rc1-Vanadium.pdf
link: /download/eva-manual-23.0-Vanadium.pdf
- name: WP manual
link: /download/wp-manual-23.0-rc1-Vanadium.pdf
link: /download/wp-manual-23.0-Vanadium.pdf
- name: E-ACSL manual
link: /download/e-acsl/e-acsl-manual-23.0-rc1-Vanadium.pdf
link: /download/e-acsl/e-acsl-manual-23.0-Vanadium.pdf
No preview for this file type
No preview for this file type
Supports Markdown
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