Abstract integer types in the frontend.

* The IntCoding interface is extended with ranks for short and long.
* The frontend now has a data type cint_type for C integer types (char, short,
  ...) and translates these to the corresponding internal int_type.
* The Coq part of the interpreter now instantiates the alignment and ptr_size
  functions instead of the OCaml part.