Fix swap when exception are in call

[lyonel2017]

Fix for #1129

[strub]

Thanks for this fix. We went for a new PR, #1188, which supersedes this one, for the following reasons.

• Too restrictive. Refusing every swap on a hoare goal with exceptional postconditions also rejects swaps that cannot change what the exceptional postcondition observes, e.g. exchanging two assignments next to a raise (swap 1 1 and swap 4 1 in tests/exception/exception_swap.ec, which had to become fail). Only moving code across something that may raise is a problem.
• Too permissive elsewhere. The syntactic raise check of Tactic swap is unsound in the presence of raise #926 was removed, so on goals without exceptional postconditions (and in the other logics) swap now moves code across a raise.
• Calls were still the real gap. swap's raise check (#926) does not look inside called procedures #1129 is about a raise inside a called procedure. fix: unlisted exceptions are unconstrained; no swap across raising calls #1188 makes swap refuse, on hoare goals that constrain exceptions, blocks that may raise: a raise, a call to a procedure whose body may raise (transitively), a call to an abstract procedure (assumed to possibly raise), or an abstract instruction. fission / fusion had the same gap (a FIXME) and get the same check.
• What "no exceptional postcondition" means. Deciding when raising is observable required fixing the meaning of an exception that is neither named nor covered by a default branch _ => Q. The abstract procedure rule already treats it as unconstrained (hoare [A.f : I ==> I] holds for every instance of A, including raising ones), so fix: unlisted exceptions are unconstrained; no swap across raising calls #1188 makes this explicit everywhere (_ => true): wp gives true instead of failing, and conseq / call no longer fail with Failure "no default exception". A goal therefore constrains exceptions only when it has a branch other than true; otherwise raising is as good as not terminating, which swapping independent blocks preserves.

The tests of #1129 are included in #1188 (tests/exception/exception_default.ec). Closing in favour of #1188.