From 5e445cdd3581190b77a4115505e79dc2e9663626 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 27 Nov 2024 16:19:52 +0100 Subject: [PATCH] Updates in preparation for release 3.15 --- Changelog.md | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/Changelog.md b/Changelog.md index 969bbf910c..b7b30dd7e0 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,3 +1,38 @@ +# Release 3.15 + +C language support: +- Minimal syntactic support for `_Float16` type (half-precision FP numbers). Function declarations using `_Float16` are correctly parsed, but any actual use of `_Float16` is rejected later during compilation. (#525) + +Code generation and optimization: +- Better support for `_Bool` type in the back-end and in the memory model. + This avoids redundant normalizations to `_Bool`. +- Take types of function parameters into account during value analysis. + This avoids redundant normalizations on parameters of small integer types. +- More conservative static analysis of pointer comparisons. (#516) +- Refined heuristic for if-conversion. Turn if-conversion off in some cases where it would prevent later optimization of conditional branches in the continuation of the `if`. +- CSE: remember pointer alias information in `Load` equations, making it possible to remove more redundant memory loads. (#518) +- More precise value analysis of integer multiplication, division, modulus. +- Constant propagation: optimize "known integer or undefined" results. For example, `&x == &x`, which is either 1 or undefined, is now replaced by 1. +- Optimize `(x ^ cst) != 0` into `x != cst`. +- Avoid quadratic compile-time behavior on deeply-nested `if` statements. (#519) + +Bug fixes: +- More robust determination of symbols that may be defined in a shared object. (#538) + +Usability: +- Mark stack as non-executable in binaries produced by `ccomp`. +- Check that preprocessed sources (`.i` files) do not contain backslash-newline sequences. + +Supporting libraries: +- ARM library for 64-bit integer arithmetic: faster division, cleaned-up code. + +Coq development: +- Support Coq 8.20. +- Install `.glob` and `.v` files along `.vo` files. +- Build: support TIMING and PROFILING like `coq_makefile`. (#512) +- Make dependency on `Extraction` explicit. (#515) + + # Release 3.14, 2024-05-02 ISO C conformance: