diff --git a/Changelog b/Changelog index 217c2c3d43c25c5dd0a168ef1eb34ebf095d42e7..24556d96caa91efa08bcbcd861ac124f2ec178f6 100644 --- a/Changelog +++ b/Changelog @@ -24,14 +24,22 @@ Open Source Release 29.0 (Copper) - Kernel [2024-04-30] new warning category too-large-array, allowing to use array > SIZE_MAX by changing its status (default is error). +- Eva [2024-04-26] Improve builtins memcpy, memmove and memset when + arguments are imprecise. o Dev [2024-04-22] Remove frama-c-build-scripts.sh; add a section in the user manual about how to manually replace it. -! Kernel [2024-04-19] Change format of custom_defs field in machdep schema and allow #undefining builtin macros in the command-line. +- Eva [2024-04-18] Remove support for deprecated WIDEN_HINTS loop pragma. + Use ACSL extension "widen_hints" instead. o Kernel [2024-04-17] Remove deprecated funcs Extlib.string_{pre,suf}fix - Alias [2024-04-16] Fix analysis results in the presence of structures. Complete rework of the API. Improved documentation. Fix stack overflow in case of a cyclic graph. +- Eva [2024-04-10] Reduce pointer values according to ACSL predicate + \base_addr. +-* Eva [2024-04-10] Fix a crash when running successive analyses using + the -eva-domains-function parameter. - Kernel [2024-04-04] Avoid ambiguous pretty-printing when C labels match the name of an ACSL built-in label (fix #@1359) -! Kernel [2024-04-02] Systematically abort when a function is redeclared @@ -41,6 +49,8 @@ o Kernel [2024-04-17] Remove deprecated funcs Extlib.string_{pre,suf}fix o Kernel [2024-04-02] Annotations.{fold,iter}_behaviors now pass full behaviors to the iterated function. To iter on fragments split by behavior and emitter, use {fold,iter}_behaviors_by_emitter. +- Eva [2024-03-29] Reduce pointer values according to ACSL predicate + valid_string and valid_read_string. o! Kernel [2024-03-29] Refactor current location handling mechanism - Kernel [2024-03-26] Introduce \plugin:: prefix for ACSL extensions, unknown extensions can be safely ignored when the plug-in that @@ -48,6 +58,10 @@ o! Kernel [2024-03-29] Refactor current location handling mechanism -* Variadic [2024-03-07] Make sure that generated functions have fresh names o! Kernel [2024-03-07] More coherent naming of functions determining if a symbol is a Frama-C built-in. +- Eva [2024-03-04] Better reporting of imprecise "garbled mix" values + (resulting from imprecise or unsupported operations on addresses) + through more relevant messages and a compact summary at the end of + the analysis, enabled by default. -* Kernel [2024-03-04] Accept conditional expr whose 2d and 3d operands have type void, as per C11 6.5.15§3 -* Kernel [2024-02-22] When an array is declared with a fixed length l,