Supports very simple programs that load integer immediates. It starts
the main, loads integer in registers, and return correctly.

Addition in Mach not yet supported, but should not be hard to add them.

Function calls are not yet supported.

The ABI for now is the same as the RiscV, with a small twist: $ra is
first loaded in a user register, then this user register is pushed
(instead of pushing $ra straight away).

ça va un peu plus loin!

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.