From 68b959aa3855dc62ff371546551a6bc82e1d1cfb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Wed, 3 May 2023 15:22:56 +0200 Subject: [PATCH] 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. --- Changelog | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/Changelog b/Changelog index e2a780622ce..cdb8117caf1 100644 --- a/Changelog +++ b/Changelog @@ -18,9 +18,30 @@ 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. +-* 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). +- 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. +-* 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) -- GitLab