CompCert release 18.04

New features

  • New builtin for tool coupling with which allows inserting AIS annotations in the original source code.
  • JSON export of abstract ARM assembly.
  • New builtins for the PowerPC 32-/64-bit hybrid mode:
    • __builtin_mulhd (PowerPC instruction mulhd)
    • __builtin_mulhdu (PowerPC instruction mulhdu)
    • __builtin_read64_reversed (PowerPC instruction ldbrx)
    • __builtin_write64_reversed (PowerPC instruction stdbrx)
  • The -t option of dcc for the Diab-based backend is now supported and passed on to the assembler, preprocessor and linker.

Valex

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

Diagnostics

  • Improved and unified error diagnostics.
  • New diagnostics for:
    • duplicated cases inside of switch statements
    • usage of void as type for parameters
    • empty typedefs and using _Noreturn in typedefs
    • incomplete array element types
    • empty declarations in K&R functions
    • assigning a volatile struct to a struct
    • casts involving composite types as required by ISO standard
    • static or extern variables defined inside a for statement
    • comparing a pointer to complete and incomplete type
  • Improved handling and diagnostics for the auto storage class.
  • Improved error messages for:
    • exhausted ELF code during instruction comparison
    • subtraction of arithmetic type and pointer
  • Improved check for incomplete types in pointer subtraction.
  • Added check for enums that have the same tag as composites.
  • Empty enum declarations after nonempty enum definitions are accepted.

Other 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.

Fixes

  • New check for constant expression and redeclarations of static variables and functions.
  • 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.
  • For addressing modes symbol + ofs in the 64-bit x86 backend, the range of ofs is limited to 24 bits.
  • For sizeof and _Alignof on expressions designating bit-fields, an error is triggered.
  • Fixed initialization of anonymous bit-fields in structs.