Exceptions support in CF

[Armael]

Not finished yet.

Progress:

• Support raise and handle in the cf function
• Update the soundness proof
• Update the existing tactics and specifications of the examples so they still work
• Implement tactics and add examples for raise and handle
• Be able to use translator representation predicates for exceptions
• Optionally generalize existing cfs (eg for division or array access), to specify the case where an exception is raised (at the moment, the user has to prove that this case cannot happen) [for later]

Some questions:

• Does something need to be added to basisProgramScript about exceptions?
• please bikeshed about the auxiliary predicates used for post-conditions. At the moment, one writes POSTv v. Qv v for writing a "pure" postcondition (meaning that the exception case cannot happen), POSTe v. Qe v for a postcondition for the exception case only (the value case cannot happen), and POST Qv Qe for specifying one post-condition for each case
• does something else need to be done?

[xrchz]

Looking good. I think it's fine to just finish raise and handle tactics for this, and anything more can be done later.

[Armael]

Everything should be done now.
I'll rebase on top of master later tonight.

[Armael]

Rebase done (it includes new changes, related to normalisation).