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.

Detect (and reject with an error) preprocessing numbers that are not valid integer or floating constants.

Cosmetic: README in MarkDown

Ccompuimm now depends on the memory, this is needed to proof the Lemma op_depends_on_memory_correct.

Extended annotations

Revised semantics of comparisons between a pointer and 0.

Fix overflows in printers for clight and csyntax.

Conflicts:
	Makefile
	driver/Driver.ml

ABI conformance for passing function arguments and returning function results of struct and union types

Refactored code, added comments and changed handling of types with attributes to avoid duplications.