diff options
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 35 |
1 files changed, 35 insertions, 0 deletions
@@ -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 <stdbool.h> (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 ======================= |