Separate builtins and external function calls.

I have made the following changes:

* Separate builtins from external calls in the AST. We now have two types:

  + external_function: proper external calls that are not inlined and
    translated into actual function calls in the assembly.
    Examples: long long division, malloc, free, system calls/

  + builtin: compiler intrinsics that do not correspond to actual calls in the
    assembly and are pretty printed to custom assembly code.
    Examples:  volatile read/write, long long addition/multiplication,
      memcpy, annotations, inline assembly/

* Ensure that builtins/external calls are used in a coherent way in the
  expression/statement syntax. In Clight, we now have

  Inductive statement : Type :=
    ...
    | Scall: option ident -> expr -> list expr -> statement
    | Sbuiltin: option ident -> builtin -> typelist -> list expr -> statement
    ...

  Inductive fundef : Type :=
    | Internal: function -> fundef
    | External: external_function -> typelist -> type -> fundef.

  As a result, it is now easier for the compiler to distinguish the two with
  respect to inlining. The boolean predicate ef_inline has been removed, and
  the classification of calls in Selection is not needed anymore because it is
  guaranteed by the syntax.

* Give explicit semantics to builtins for i64 operations. I now have the
  following two types:

  Inductive i64_function :=
    | i64_dtos
    | i64_dtou
    ...

  Inductive i64_builtin :=
    | i64_neg
    | i64_add
    ...

  And these are given an actual semantics in Coq. This yields the improvement
  that Properties as preservation under memory injections/extensions (as
  captured by extcall_properties) are explicitly proven, rather than assumed
  (as previously done by get_helpers_correct).

  Gordon Stewart remarked that the axiomatization of i64 functions used to be
  inconsistent in CompCert 2.1 (it was assumed that i64 calls had both 1
  event, and 0 events). Since the number of axioms has decreased, I have
  reduced the chance of such inconsistencies to occur.

* To make it possible for the compiler to translate actual i64 operations (as
  in Cminor and before) into function calls, the i64 functions should be in
  global environment. The compiler itself cannot insert such functions, so I
  let C2C.ml insert them, and let Selection check whether they are indeed there.