Release 3.5, 2019-02-27

Bug fixing:

Modeling error in PowerPC ISA: how register 0 is interpreted when used as base register for indexed load/stores. The code generated by CompCert was correct, but was proved correct against the wrong specification.
Modeling error in x86 ISA: how flag ZF is set by floating-point comparisons. Here as well, the code generated by CompCert was correct, but was proved correct against the wrong specification.
Revised handling of attributes so that they behave more like in GCC and Clang. CompCert now distinguishes between attributes that attach to names (variables, fields, typedefs, structs and unions) and attributes that attach to objects (variables). In particular, the aligned(N) attribute now attaches to names, while the _Alignas(N) modifier still attaches to objects. This fixes issue #256.
Issue with NULL as argument to a variadic function on 64-bit platforms (issue #265)
Macro __bool_true_false_are_defined was missing from <stdbool.h> (issue #266)

Can now be entirely rechecked using coqchk (contributed by Vincent Laporte)
Support Coq version 8.9.0
Avoid using "refine mode" when defining Instance (contributed by Maxime Dénès)
Do not support Menhir versions more recent than 20181113, because they will introduce an incompatibility with this CompCert release.

PowerPC port: add __builtin_isel (conditional move) at types int64, uint64, and _Bool.