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.

[bgregoir]

Maybe we can remove form option if we create a special path "_".
Having special path can be useful also if we want to have return anywhere in the code: we can have a return exception. Similarly if we want to add "break".

[bgregoir]

It would be good to use a different name than post. Maybe hoare_post.

[bgregoir]

ss2 seems to be a strange name for a hs_inv

[bgregoir]

use a correct error message

[bgregoir]

Improve error message