|
|
|
# Frama-C release 22.0 (Titanium)
|
|
|
|
## Sources
|
|
|
|
- [frama-c-22.0-Titanium.tar.gz](downloads/frama-c-22.0-Titanium.tar.gz)
|
|
|
|
|
|
|
|
## Manuals
|
|
|
|
- [acsl-1.16](manuals/acsl-1.16.pdf)
|
|
|
|
- [acsl-implementation](manuals/acsl-implementation-22.0-Titanium.pdf)
|
|
|
|
- [aorai-example-22.0-Titanium.tgz](manuals/aorai-example-22.0-Titanium.tgz)
|
|
|
|
- [aorai-manual](manuals/aorai-manual-22.0-Titanium.pdf)
|
|
|
|
- [e-acsl-1.16](manuals/e-acsl-1.16.pdf)
|
|
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation-22.0-Titanium.pdf)
|
|
|
|
- [e-acsl-manual](manuals/e-acsl-manual-22.0-Titanium.pdf)
|
|
|
|
- [eva-manual](manuals/eva-manual-22.0-Titanium.pdf)
|
|
|
|
- [metrics-manual](manuals/metrics-manual-22.0-Titanium.pdf)
|
|
|
|
- [plugin-development-guide](manuals/plugin-development-guide-22.0-Titanium.pdf)
|
|
|
|
- [rte-manual](manuals/rte-manual-22.0-Titanium.pdf)
|
|
|
|
- [user-manual](manuals/user-manual-22.0-Titanium.pdf)
|
|
|
|
- [wp-manual](manuals/wp-manual-22.0-Titanium.pdf)
|
|
|
|
|
|
|
|
## Main Changes
|
|
|
|
### 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 |
