From 235a41ae79324d523e7e0c20194846a0a93aecd9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 25 Feb 2019 19:43:19 +0100 Subject: Update Changelog in preparation for release 3.5 --- Changelog | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index fda9417e..e4ef5b12 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,38 @@ +Release 3.5, 2019-02-27 +======================= + +Bug fixing: +- Modeling error in PowerPC ISA: how register 0 is interpreted when + used as base register for indexed load/stores. The code generated + by CompCert was correct, but was proved correct against the wrong + specification. +- Modeling error in x86 ISA: how flag ZF is set by floating-point + comparisons. Here as well, the code generated by CompCert was + correct, but was proved correct against the wrong specification. +- Revised handling of attributes so that they behave more like in + GCC and Clang. CompCert now distinguishes between attributes that + attach to names (variables, fields, typedefs, structs and unions) + and attributes that attach to objects (variables). In particular, + the `aligned(N)` attribute now attaches to names, while the `_Alignas(N)` + modifier still attaches to objects. This fixes issue 256. +- Issue with NULL as argument to a variadic function on 64-bit platforms + (issue 265) +- Macro __bool_true_false_are_defined was missing from (issue 266) + +Coq development: +- Can now be entirely rechecked using coqchk + (contributed by Vincent Laporte) +- Support Coq version 8.9.0 +- Avoid using "refine mode" when defining Instance + (contributed by Maxime Dénès) +- Do not support Menhir versions more recent than 20181026, because + they will introduce an incompatibility with this CompCert release. + +New feature: +- PowerPC port: add __builtin_isel (conditional move) at types int64, uint64, + and _Bool. + + Release 3.4, 2018-09-17 ======================= -- cgit