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

Frama-C 22 release

parent e8715c03
layout: default
date: 20-11-2020
event: Frama-C 22.0 (Titanium)
title: Release of Frama-C 22.0 (Titanium)
Frama-C 22.0 (Titanium) is out. Download it [here](/fc-versions/titanium.html).
Main changes with respect to Frama-C 21 (Scandium) include:
#### Kernel:
- OCaml version greater than or equal to 4.08.1 required.
- introduce check-only annotations for requires, ensures, loop invariant and lemmas
- `\from` now accepts `&v` expressions
- add option `-print-config-json`, to output Frama-C configuration data in JSON format
- new option `-explain`, which provides help messages for options used on the command line
- add option `-print-cpp-commands`, to print the preprocessing commands used by Frama-C
- support for C11's `_Noreturn` and `_Thread_local` specifiers
- allows for axiomatic blocks-like extensions
#### Aorai:
- Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards.
#### E-ACSL:
- support of bitwise operators
- support of `\separated`
- support of `complete` and `disjoint` behaviors
- support of logical array comparisons
#### Eva:
- easier setup of dynamic allocation builtins: new option `-eva-alloc-builtin` to configure uniformly their behavior (instead of mapping each `malloc`/`calloc`/`realloc` function to the corresponding builtin), and new annotation `eva_allocate` to locally override the global option
- new builtins for trigonometric functions `acos`, `asin` and `atan` (and their single-precision version `acosf`, `asinf`, `atanf`)
- improved automatic loop unroll (`-eva-auto-loop-unroll` option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C normalization or `goto` statements
#### Markdown Report:
- update Sarif output to 2.1.0 and prettier URI
#### Variadic:
- the generated code is now compilable and compatible with E-ACSL
#### WP:
- upgraded Why3 backend (requires why3 1.3.3)
- support of the `\initialized` ACSL predicate
- support for generalized check-only ACSL annotations
- added support for Why3 interactive prover (Coq)
- new tactic Bit-Test range
- memory model hypotheses warnings are more precise
- new experimental option: `-wp-check-memory-model` to automatically check memory model hypotheses
- new warning `pedantic-assigns`. WP needs precise `assigns ... \from ...` specification about out pointers to generate precise proof hypotheses
A complete changelog can be found [here](/html/changelog.html#Titanium-22.0).
\ No newline at end of file
layout: version
number: 22
beta: yes
name: Titanium
acsl: 16
- number: 0
- name: Frama-C v22.0-beta Titanium
- name: Frama-C v22.0 Titanium
- name: Source distribution
link: /download/frama-c-22.0-beta-Titanium.tar.gz
link: /download/frama-c-22.0-Titanium.tar.gz
help: Compilation instructions
help_link: /html/installations/titanium.html
- name: User manual
link: /download/user-manual-22.0-beta-Titanium.pdf
link: /download/user-manual-22.0-Titanium.pdf
- name: Plugin-In development guide
link: /download/plugin-development-guide-22.0-beta-Titanium.pdf
link: /download/plugin-development-guide-22.0-Titanium.pdf
help: Hello plug-in tutorial archive
help_link: /download/hello-22.0-Titanium.tar.gz
- name: API Documentation
link: /download/frama-c-22.0-Titanium-api.tar.gz
- name: ACSL 1.15 (Titanium implementation)
link: /download/acsl-implementation-22.0-Titanium.pdf
- name: Plug-in Manuals
sort: true
- name: Aoraï manual
link: /download/aorai-manual-22.0-beta-Titanium.pdf
link: /download/aorai-manual-22.0-Titanium.pdf
- name: Metrics manual
link: /download/metrics-manual-22.0-beta-Titanium.pdf
link: /download/metrics-manual-22.0-Titanium.pdf
- name: Rte manual
link: /download/rte-manual-22.0-beta-Titanium.pdf
link: /download/rte-manual-22.0-Titanium.pdf
- name: Eva manual
link: /download/eva-manual-22.0-beta-Titanium.pdf
link: /download/eva-manual-22.0-Titanium.pdf
- name: WP manual
link: /download/wp-manual-22.0-beta-Titanium.pdf
link: /download/wp-manual-22.0-Titanium.pdf
- name: E-ACSL manual
link: /download/e-acsl/e-acsl-manual-22.0-beta-Titanium.pdf
link: /download/e-acsl/e-acsl-manual-22.0-Titanium.pdf
\ No newline at end of file
\ No newline at end of file
\ No newline at end of file
\ No newline at end of file
\ No newline at end of file
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