diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-09-14 13:56:05 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-09-14 13:56:05 +0200 |
| commit | 932d40637eaa84e6d335a0a997eacc35379e2bec (patch) | |
| tree | 6276068c1ef21d66ac4cddd9f00596ed55aa2fef /Changelog | |
| parent | b55fa30ad44a647aca8ae8786da2d4cc1a881cd8 (diff) | |
| download | compcert-kvx-932d40637eaa84e6d335a0a997eacc35379e2bec.tar.gz compcert-kvx-932d40637eaa84e6d335a0a997eacc35379e2bec.zip | |
Update change log for 3.4, continued
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -20,7 +20,10 @@ Bug fixing: the label. - Wrong parsing of the command-line options `-u <symbol>` and `-iquote`. - PowerPC in hybrid 32/64 bit mode: reject %Q and %R register specifications - in inline assembly code. + in inline assembly code, since 64-bit integer arguments are not split + in two registers. +- x86 64-bit mode: wrong expansion of __builtin_clzl and builtin_ctzl + (issue #127). New checks for ISO C conformance: - Removed support for `_Alignof(expr)`, which is not C11; @@ -50,7 +53,7 @@ Semantic preservation proof: and Outgoing stack slots; adapt the proofs accordingly. Coq and OCaml development: -- Support Coq version 8.8.1. +- Support Coq versions 8.8.1 and 8.8.2. - Support OCaml versions 4.7.0 and up. - Support Menhir versions 20180530 and up. |