CompCert release 18.04

New features

  • New builtin for tool coupling with which allows inserting AIS annotations in the original source code.
  • Added JSON export of abstract ARM assembly.
  • The dcc-based backend now supports the -t option to be passed on to the assembler, preprocessor and linker.

Valex

Valex for ARM is now available, including the corresponding Qualification Support Kit.

Improvements

  • Improved strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc.
  • New inline heuristic finline-functions-called-once that considers all static functions called once for inlining into their caller even if they are not marked inline. If a call to a given function is integrated, then the function is not output as assembler code in its own right.
  • Unified emitting of constant literals in RISC-V, PowerPC and x86 backends.
  • Improved error message for exhausted ELF code during instruction comparison.
  • Improved and unified error diagnostics.

Fixes

  • More conservative value analysis of dubious comparisons such as (uintptr_t) &global == 0x1234 which are undefined behavior in CompCert.
  • Fixed scoping of variables declared within the first clause of a for loop.
  • In the symbol + ofs addressing modes of the x86_64 backend, limit the range of ofs in 64 bits.