diff options
Diffstat (limited to 'Changelog')
-rw-r--r-- | Changelog | 100 |
1 files changed, 100 insertions, 0 deletions
@@ -1,3 +1,103 @@ +Release 3.7, 2020-03-31 +======================= + +ISO C conformance: +- Functions declared `extern` then implemented `inline` remain `extern` +- The type of a wide char constant is `wchar_t`, not `int` +- Support vertical tabs and treat them as whitespace +- Define the semantics of `free(NULL)` + +Bug fixing: +- Take sign into account for conversions from 32-bit integers to 64-bit pointers +- PowerPC: more precise determination of small data accesses +- AArch64: when addressing global variables, check for correct alignment +- PowerPC, ARM: double rounding error in int64->float32 conversions + +ABI conformance: +- x86, AArch64: re-normalize values of small integer types returned by + function calls +- PowerPC: `float` arguments passed on stack are passed in 64-bit format +- RISC-V: use the new ELF psABI instead of the old ABI from ISA 2.1 + +Usability and diagnostics: +- Unknown builtin functions trigger a specific error message +- Improved error messages + +Coq formalization: +- Revised modeling of the PowerPC/EREF `isel` instruction +- Weaker `ec_readonly` condition over external calls + (permissions can be dropped on read-only locations) + +Coq and OCaml development: +- Compatibility with Coq version 8.10.1, 8.10.2, 8.11.0 +- Compatibility with OCaml 4.10 and up +- Compatibility with Menhir 20200123 and up +- Coq versions prior to 8.8.0 are no longer supported +- OCaml versions prior to 4.05.0 are no longer supported + + +Release 3.6, 2019-09-17 +======================= + +New features and optimizations: +- New port targeting the AArch64 architecture: ARMv8 in 64-bit mode. +- New optimization: if-conversion. Some `if`/`else` statements + and `a ? b : c` conditional expressions are compiled to branchless + conditional move instructions, when supported by the target processor +- New optimization flag: `-Obranchless`, to favor the generation of + branchless instruction sequences, even if probably slower than branches. +- Built-in functions can now be given a formal semantics within + CompCert, instead of being treated as I/O interactions. + Currently, `__builtin_fsqrt` and `__builtin_bswap*` have semantics. +- Extend constant propagation and CSE optimizations to built-in + functions that have known semantics. +- New "polymorphic" built-in function: `__builtin_sel(a,b,c)`. + Similar to `a ? b : c` but `b` and `c` are always evaluated, + and a branchless conditional move instruction is produced if possible. +- x86 64 bits: faster, branchless instruction sequences are produced + for conversions between `double` and `unsigned int`. +- `__builtin_bswap64` is now available for all platforms. + +Usability and diagnostics: +- Improved the DWARF debug information generated in -g mode. +- Added options -fcommon and -fno-common to control the generation + of "common" declarations for uninitialized global. +- Check for reserved keywords `_Complex` and `_Imaginary`. +- Reject function declarations with multiple `void` parameters. +- Define macros `__COMPCERT_MAJOR__`, `__COMPCERT_MINOR__`, and + `__COMPCERT_VERSION__` with CompCert's version number. (#284) +- Prepend `$(DESTDIR)` to the installation target. (#169) +- Extended inline asm: print register names according to the + types of the corresponding arguments (e.g. for x86_64, + `%eax` if int and `%rax` if long). + +Bug fixing: +- Introduce distinct scopes for iteration and selection statements, + as required by ISO C99. +- Handle dependencies in sequences of declarations + (e.g. `int * x, sz = sizeof(x);`). (#267) +- Corrected the check for overflow in integer literals. +- On x86, __builtin_fma was producing wrong code in some cases. +- `float` arguments to `__builtin_annot` and `__builtin_ais_annot` + were uselessly promoted to type `double`. + +Coq formalization and development: +- Improved C parser based on Menhir version 20190626: + fewer run-time checks, faster validation, no axioms. (#276) +- Compatibility with Coq versions 8.9.1 and 8.10.0. +- Compatibility with OCaml versions 4.08.0 and 4.08.1. +- Updated to Flocq version 3.1. +- Revised the construction of NaN payloads in processor descriptions + so as to accommodate FMA. +- Removed some definitions and lemmas from lib/Coqlib.v, using Coq's + standard library instead. + +The clightgen tool: +- Fix normalization of Clight `switch` statements. (#285) +- Add more tracing options: `-dprepro`, `-dall`. (#298) +- Fix the output of `-dclight`. (#314) + + Release 3.5, 2019-02-27 ======================= |