Skip to content
Snippets Groups Projects
Commit dd053d25 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'Harmonize-last-event' into 'master'

Harmonize last event

See merge request !77
parents 5b1f641b bd71ede1
No related branches found
No related tags found
1 merge request!77Harmonize last event
Pipeline #30487 passed
...@@ -9,7 +9,7 @@ Frama-C 22.0-beta (Titanium) is out. Download it [here](/fc-versions/titanium.ht ...@@ -9,7 +9,7 @@ Frama-C 22.0-beta (Titanium) is out. Download it [here](/fc-versions/titanium.ht
Main changes with respect to Frama-C 21 (Scandium) include: Main changes with respect to Frama-C 21 (Scandium) include:
### Kernel #### Kernel:
- OCaml version greater than or equal to 4.08.1 required. - OCaml version greater than or equal to 4.08.1 required.
- introduce check-only annotations for requires, ensures, loop invariant and lemmas - introduce check-only annotations for requires, ensures, loop invariant and lemmas
...@@ -20,32 +20,32 @@ Main changes with respect to Frama-C 21 (Scandium) include: ...@@ -20,32 +20,32 @@ Main changes with respect to Frama-C 21 (Scandium) include:
- support for C11's `_Noreturn` and `_Thread_local` specifiers - support for C11's `_Noreturn` and `_Thread_local` specifiers
- allows for axiomatic blocks-like extensions - allows for axiomatic blocks-like extensions
### Aorai #### Aorai:
- Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards. - Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards.
### E-ACSL #### E-ACSL:
- support of bitwise operators - support of bitwise operators
- support of `\separated` - support of `\separated`
- support of `complete` and `disjoint` behaviors - support of `complete` and `disjoint` behaviors
- support of logical array comparisons - support of logical array comparisons
### Eva #### 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 - 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`) - 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 - 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 #### Markdown Report:
- update Sarif output to 2.1.0 and prettier URI - update Sarif output to 2.1.0 and prettier URI
### Variadic #### Variadic:
- the generated code is now compilable and compatible with E-ACSL - the generated code is now compilable and compatible with E-ACSL
### WP #### WP:
- upgraded Why3 backend (requires why3 1.3.3) - upgraded Why3 backend (requires why3 1.3.3)
- support of the `\initialized` ACSL predicate - support of the `\initialized` ACSL predicate
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment