diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-02-25 19:43:19 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-02-25 19:43:19 +0100 |
commit | 235a41ae79324d523e7e0c20194846a0a93aecd9 (patch) | |
tree | fc5ce79931d036e03e3a60c62f485f87cc53faca /Changelog | |
parent | fc9bc6437a91d8ba4541c2671acb49574f3aeb77 (diff) | |
download | compcert-235a41ae79324d523e7e0c20194846a0a93aecd9.tar.gz compcert-235a41ae79324d523e7e0c20194846a0a93aecd9.zip |
Update Changelog in preparation for release 3.5
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 ======================= |