Consider:
  struct P { int x, y; }
  struct S { struct P p; }

  struct P p0 = { 1,2 };
  struct S s1 = { .p = p0; .p.x = 3 };

ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e.
the initialization of s1.p.y to p0.y implied by ".p = p0" is kept,
even though the initialization of s1.p.x to p0.x is overwritten
by ".p.x = 3".

GCC, old versions of Clang, and previous versions of CompCert
initialize s1.p.y to the default value 0.  I.e. the initialization
".p = p0" is forgotten, leaving default values for the fields of .p
before ".p.x = 3" takes effect.

Implementing the proper ISO C99 semantics in CompCert is difficult,
owing to a mismatch between the intended semantics and the C.init
representation of initializers.

This commit turns the delicate case of reinitialization above
(re-initializing a member of a composite that has already been
initialized as a whole) into a compile-time error.

We will then see if the delicate case occurs in practice and needs
further attention.

The ISO C99 standard allows cast only if the type name involved
is either a void type or a scalar type.  
For compatibility with GCC and Clang we used to support casting
a struct or union to exactly the same struct or union type.
That does not seem useful in practice and complicates conformance
testing.  This commit gets rid of this exception to the C99 rule.

Bug 23310

Instead of overwriting the initializer of the anonymous member we
should just keep it.
Bug 23353

Implicit Arguments is deprecated in Coq since 8.6 or so.  
Some Implicit Arguments remained in Flocq but were recently changed to Arguments.  
Apply the same change to our local copy of Flocq.
As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.

Sizeof and _Alignof are not allowed on bit-fields

Sizeof and _Alignof are not allowed to be applied to a expression
that designates a bit-field member.
Bug 23311

Unions containing multiple bit fields were transformed incorrectly.

Arrays should decay to pointers except if they are used as operands of sizeof, _Alignof or as
operand of the unary &.  The "comma" sequencing operator was missing a "decay" on the type of its second argument.  All other operators "decay" their operands correctly.
Bug 23299
Bug 23311

If an anonymous bit-field member is declared wrong, i.e. a wrong
type is used or a too large size is used the error message now
prints <anonymous> instead of an empty string.
Bug 23292

* Do not allow inline on main().

The C99 standard says that in a hosted environment inline shall
not appear in a declaration of main.
Bug 23274

* Added warning for _Noreturn on main().

The C11 standard does not allow any function specifier on the
main function.
Bug 23274

This should avoid cluttering the assembler output with .ascii "\n"
lines if the annotation ends with a string and make for a better
readability.
Bug 23169

It's OK to ignore *.o in any directory, but it's safer to ignore
"/ccomp" (ccomp in the top-level directory) than to ignore
"ccomp"  (ccomp in any directory).

Init_space has an argument of type Z and it can exceed the range of a 32-bit integer.
Reported by Frédéric Besson.

It seems necessary that the mulitplication for the high part of
split registers is put into brackets.
Bug 23169

The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3.
Fix 23199

This will soon be deprecated by Coq.

Manual merge of pull request #224 by vbgl.  Closes: #224

struct/union arguments to annotations should not be transformed at top level,
but the regular function calls contained within must be transformed recursively.

In order to ensure that no transformation for arguments to
builtin annotations are used, the original unchanged arguments are
used.
Bug 23179

This should help with parallel builds, which currently fail sometimes
owing to a lack of a dependency on pre_parser_aux.cmi.

Also: move documentation comments from the .ml to the .mli

Make sure struct/union arguments to __builtin_annot and related
builtins are always passed by reference using the default passing mode,
regardless of the ABI for passing struct/unions to "real" functions.

This ensures portability of annotations across ABIs, and avoids mismatches
between the annotation text and the actual number of arguments
(when a struct/union argument is passed as N integer arguments).

A similar special case already existed for __builtin_va_arg.

Printing variable names with the default expression printer
results in newlines in the outputed error message.
Bug 23169

The strings for json need quoting of special characters such as
\" and \\.
Bug 22438

x2 is the stack pointer of the riscV, both sp and x2 are supported
but to be safe use x2 in annotations.
Bug 23176

This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438

It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and
'sp' for riscV.
Bug 23176.

Registers should not contain the % prefix for ais annotations.
Bug 23176

Include the format specifier in error message when available in
order to make it easier to spot the broken ais parameter.

Futhermore introduce a new warning for unused ais parameters.
Bug 22464

Mention that it is a global memory cell.
Fix 22464

This should avoid problems when newlines are used in string
constants etc.
Bug 23172

The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.

The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.

Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.

Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.