29/03/2011:
  Label moved out of ASM.ma labelled_instruction datatype, as the Paris compiler
  can only produce at most one label per instruction emitted.

  Merged the LTL and LIN datatypes.

  Added comments to the ASM datatypes.

  Changed identifiers from bytes to words.

  Formalised missing Assembly.ma file.

30/03/2011:
  Split translate_statements into two functions.

  Added a dependent type for the invariant that a LIN function body does not
  start with a label, and is not empty.

01/04/2011:
  In retrospect:

  The Clight semantics are based on CompCert 1.6 rather than the prototype's;
  this also affects some of the common files.

    The identifiers are Words so that we can use BitVectorTries for maps.
    Similarly, integers are based on BitVectors rather than Coq-style binary
    integers + range proof.

  8051 memory spaces are present, but are not (yet?) in the prototype.

  Dependent types are used to fix the number of arguments for addressing modes
  in RTLabs.

04/04/2011:
  common/Identifiers.ma provides identifiers similar to atomSig in the
  prototype, except that we use the universe's name as a tag for the type of
  identifiers to provide some extra type safety.

08/04/2011:
  Make return register optional in RTLabs

26/04/2011:
  Remove register from RTLabs return statements because it ends up being
  redundant (we always use the register in the function record).

  The constants follow CompCert's rather than the prototype's with the result
  that they match up more closely with the addressing modes in RTLabs.

  One of the front end operations for subtraction (subpp) appears to be missing
  from the prototype at present.

19/05/2011:
  Dump Param var_type from the Clight to Cminor stage - we need to treat them
  like the other variables.

  Generate list of pointer variables from Clight types rather than
  recalculation.

  Drop signatures from function call statements in Cminor and RTLabs - they
  appear to be unused.

13/07/2011:  [belatedly]
  Offsets haven't been abstracted in the front end.  They might be later if it
  turns out to be useful in the proofs.  (See the messages in the thread
  "32 and 16 bits integers support" from the 16th June 2011.)

  The integer cast operation in the front end doesn't take the operand size.
  In keeping with the other operations, we deduce it from the operand.
  The sizes of the results are always mentioned so that they can be evaluated
  without consulting the type information (although this is a somewhat
  arbitrary decision).

30/08/2011:  [annotation]
  There is a mismatch between the capability of external functions in the
  OCaml and Matita code. In OCaml they can interact with the memory. In
  Matita (following old? CompCert) they cannot. Hence, in the semantics
  of intermediate languages from ERTL on, we need to recover the arguments
  for the function not only from the registers, but also from the stack.

08/09/2011:
  The Clight cast simplification algorithm is quite different to the prototype's:
  it only needs to do a simple pattern match per recursion and copes with deeper
  arithmetic expressions such as (char)((int)x + (int)y + (int)z).

17/10/2011: (CSC)
  In OCaml, RTL's and ERTL's St_return statement holds the return register list,
  to be used in is_final. In Matita, they don't. For RTL the information was
  duplicated in the internal function record. I have done the same for ERTL too.
  To be double checked with the OCaml semantics.