diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-28 16:12:51 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-28 16:12:51 +0200 |
| commit | f2fe37ccc79649dbb622b1bf2d0d144f2e0a5768 (patch) | |
| tree | 6d673f3f73a7fa43036dc1eed9463740fdc235c5 /Changelog | |
| parent | f642817f0dc761e51c3bd362f75b0068a8d4b0c8 (diff) | |
| download | compcert-kvx-f2fe37ccc79649dbb622b1bf2d0d144f2e0a5768.tar.gz compcert-kvx-f2fe37ccc79649dbb622b1bf2d0d144f2e0a5768.zip | |
Update Changelog with recent changes
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 8 |
1 files changed, 7 insertions, 1 deletions
@@ -1,9 +1,15 @@ - New port targeting the RISC-V architecture, in 32- and 64-bit modes. - +- Always generate .merlin and _CoqProject files. +- PowerPC back-end: leaf functions optimization. +- Add options -finline / -fno-inline to control function inlining. +- Avoid generating useless conditional branches for empty if/else statements. - Removed the compilation of '.cm' files written in Cminor concrete syntax. Bug fixing: - Issue #179: clightgen produces wrong output for "switch" statements. +- Do not generate code for functions with "inline" specifier that are + neither static nor extern, as per ISO C99. +- Some line number information was missing for some goto labels and switch cases. Release 3.0.1, 2017-02-14 |