The port makes the following notable changes:

* The carrier types of separation algebras and integer environments are no
  longer in Set. Now they have a type at a fixed type level above Set. This
  both works better in 8.5 and makes the formalization more general.
  I have tried putting them at polymorphic type levels, but that increased the
  compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
  That bug has been fixed, so this custom tactic can be removed when the next
  beta of 8.5 is out.

It would still be far more efficient to have a counter for the next memory
index in the executable semantics/frontend.

Ported from popl2014 branch.

First it would destruct on the decider, which sometimes would result
in unfolded hypotheses.

The tactic "injection' H" now uses the name "H" for the first hypothesis it
generates. Fresh names will still be used for the remaining hypotheses.

Important changes in the core semantics:
* Types extended with function types. Since function types are a special kind
  of pointer types, types now have an additional mutual part called "ptr_type".
* Pointers extended with function pointers. Theses are just names that refer
  to an actual function in the function environment.
* Typing environments extended to assign argument and return types to function
  names. Before we used a separate environment for these, but since the
  argument and return types are already needed to type function pointers, this
  environment would appear in pretty much every typing judgment.

As a side-effect, the frontend has been rewritten entirely. The important
changes are:

* Type checking of expressions is more involved: there is a special kind of
  expression type corresponding to a function designator.
* To handle things like block scoped extern function, more state-fullness was
  needed. To prepare for future extensions, the entire frontend now uses a
  state monad.

Type environments now describe alignment, this allows to:
* Prove properties about alignment, for example that bit offsets
  of addresses are always aligned.
* Support align_of expressions in the frontend.

addresses.

The operation "mem_force Γ m a" used to apply the identify function to
pricisely the object "a", even in case "a" is an "unsigned char" address
refering to an individual byte. This caused the ctree substructure of the
entire subobject to disappear and had the undesired effect that:

  mem_force Γ a m ⊑{Γ,true@Γm} m

failed to hold (i.e. unused reads cannot be removed).

* This behavior is "implementation defined" and can be turned on and off
  using the Boolean field "alloc_can_fail" of the class "Env".
* The expression "EAlloc" is now an r-value of pointer type instead of an
  l-value.
* The executable semantics for expressions is now non-deterministic. Hence,
  some proofs had to be revised.

Pointer equality is now defined using absolute object offsets. The treatment
is similar to CompCert:

* Equality of pointers in the same object is defined provided the object has
  not been deallocated.
* Equality of pointers in different objects is defined provided both pointers
  have not been deallocated and both are strict (i.e. not end-of-array).

Thus, pointer equality is defined for all pointers that are not-end-of-array
and have not been deallocated. The following examples have defined behavior:

  int x, y;
  printf("%d\n", &x == &y);
  int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
  printf("%d\n", p == q);
  struct S { int a; int b; } s, *r = &s;
  printf("%d\n", &s.a + 1 == &(r->b));

The following not:

  int x, y;
  printf("%d\n", &x + 1 == &y);

The refinement relation on addresses allows union references to be refined:

  (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2

The result is that frozen values are below their unfrozen variant, which made
it possible to prove that constant propagation (see constant_propagation.v) can
be performed on the level of the memory model.