Commit b0a2dce9 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

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

23.0-Vanadium release

See merge request !119
parents 2c30fea8 63a79d9e
Pipeline #36314 passed with stage
in 2 minutes and 39 seconds
---
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
releases:
- number: 0
categories:
- name: Frama-C v23.0~rc1 Vanadium
- name: Frama-C v23.0 Vanadium
files:
- 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
files:
- 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
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