Allow the option -o to be also the prefix of the file name for compability with different build systems.

Use this info in printing function types for Csyntax and Clight.

Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.

Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline.  Then, retyping would
no longer be performed in C2C.  We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.

 Changed the enter_or_refine_ident function to produce an error if a non-static declaration is followed by a static declaration/definition.

- Treat clobbered registers as being destroyed by EF_inline_asm builtins
  (which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
  and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.

-# Please enter the commit message for your changes. Lines starting

Detect uses of anonymous structs/unions (a C2011 feature and GCC extension) and produce a diagnostic instead of ignoring them.

Bitfield improvements continued: perform bitfield expansion before unblocking; improve translation of bitfield initializers and compound literals.

Bitfields: better translation of initializers and compound literals; run this pass before unblocking.
Transform.stmt: extend with ability to treat unblocked code.
test/regression: more bitfield tests.

Also: spurious '\n' in C2C.warning.

GCC-style extended inline asm.

The subset implemented is:

- zero or one output
- output constraints "=r" (to register) or "=m" (to memory)
- zero, one or several inputs
- input constraints "r" (in register), "m" (in memory), "i" and "n" (compile-time integer constant)
- clobbered registers (the 3rd argument)
- both anonymous (%3) and named (%[name]) operands
- modifiers %R and %Q to refer to the most significant / least significant part of a register pair holding a 64-bit integer. (Undocumented GCC ARM feature.)

All asm statements are treated as "volatile", possibly modifying memory and condition codes.

We can ignore alternatives as long as one of the constraints we
handle (r, m, i, n) is there.

- support "r", "m" and "i" constraints
- support "%Q" and "%R" modifiers for register pairs
- support register clobbers
- split off analysis and transformation of asm statements in
  cparser/ExtendedAsm.ml

Added the Dwarf v2 debugging information for global variables and functions for the Diab Backend.

As opposed to the default "gnu99" mode, the C99 mode turns off a number of GNU-isms in standard header files like those of glibc.