Feature exception

[lyonel2017]

This PR introduce exceptions for Hoare Logic.

We can define exception :

exception assume.
exception assert.

We can raise exception using raise assume or raise (x = 3) assert (raise an exception when a condition is not true):

module M ={
  proc f (x:int) : int = {
    raise (x = 3) assert;
    x <- 1;
    if (x = 3)  {
       raise assume;
    }
    if (x=3) {
        raise assert;
      }
  return x;
  }
}.

We can define postconditions for each exception and a default postcondition:

lemma assume_assert : hoare [M.f : pre ==> post | assume:p1 |assert: p2 | p3].

Examples are available in examples/exception.ec.