CompCert Release 18.04
----------------------


New features
------------
● New builtin for tool coupling with a³ 
  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.


------------------------------------------------------------------------------
Last modified on 8 May 2018 by alex@absint.com. Copyright 2018 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
www.absint.com/releasenotes/compcert/18.04