Skip to content
Snippets Groups Projects
Commit 68b959aa authored by David Bühler's avatar David Bühler
Browse files

Retroactively updates the Changelog for Eva.

- MR !4164: fixes interpretation of Eva annotations.
- MR !3993: allows comments in .ya automata files and specifications about
  floating-point variables. Also, Eva shows the name of enumeration tags
  instead of their integer values.
- MR !4147: ivette shows the status of uninitialized and escaping variables.
- MR !4151: better display of large integer sets.
- MR !4134: the values table can show the status of ACSL predicates, the values
  of C lvalues in these predicates, and the values of function parameters.
- MR !4098: fixes a soundness bug of the equality domain.
- MR !4065: fixes performances issues on programs with too many callsites.
- MR !4015: fixes the bitwise domain on big-endian architecture.
- MR !4046: better partitioning splits on ACSL predicates.
parent 9d14adc4
No related branches found
No related tags found
No related merge requests found
...@@ -18,9 +18,30 @@ ...@@ -18,9 +18,30 @@
Open Source Release <next-release> Open Source Release <next-release>
############################################################################### ###############################################################################
-* Eva [2023-05-02] Fixes interpretation of Eva annotations at the end of
a block, and of multiple split annotations after a function call.
- Eva [2023-04-24] When possible, Eva shows the name of enumeration tags
instead of their integer values, in the log and the GUI.
- Aorai [2023-04-24] Allows comments in .ya automata files.
- Aorai [2023-04-24] Supports specification about floating-point variables.
- Ivette [2023-04-07] The values table shows the status of uninitialized
and escaping variables.
- Eva [2023-04-05] Better display of large integer sets for high values
of the -eva-ilevel parameter.
- Ivette [2023-03-31] The values table shows values of function parameters.
- Ivette [2023-03-31] The values table can show the logical status of ACSL
predicates, and the values of C lvalues in these predicates.
o! GUI [2023-03-27] Remove GTK2 bindings. Only support GTK3 as of now. o! GUI [2023-03-27] Remove GTK2 bindings. Only support GTK3 as of now.
-* Eva [2023-03-13] Fixes a soundness bug of the equality domain when
the same equality holds in two programs paths, but involving a
pointer pointing to different variables in the two paths.
- Kernel [2023-03-03] Deprecate option -c11 (now enabled by default). - Kernel [2023-03-03] Deprecate option -c11 (now enabled by default).
- Eva [2023-02-06] Fixes performance issues on programs with too many
function calls (more than 20000 callsites).
-! Kernel [2023-01-25] Add support for C11's _Generic. Modifies Cabs AST. -! Kernel [2023-01-25] Add support for C11's _Generic. Modifies Cabs AST.
-* Eva [2023-01-16] Fixes unsoundness of the bitwise domain on shifts
and casts on big-endian architectures.
- Eva [2023-01-12] Better partitioning splits on ACSL predicates.
############################################################################### ###############################################################################
Open Source Release 26.1 (Iron) Open Source Release 26.1 (Iron)
......
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