CompCert Release 18.04

New features
------------
● New builtin for tool coupling with a³ 
  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
-----
Added support for validating the linking of ARM binaries.


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.