Desugaring quasihavocall to an exhale-inhale pair

[marcoeilers]

This PR adds support for quasihavocall similar to the existing support for quasihavoc, namely by desugaring it into an exhale-inhale pair (which unfortunately means that magic wands cannot be supported).

quasihavoc vars :: cond ==> P(args)

is desugared to

label perm_temp_quasihavoc_
exhale forall vars :: { P(args) } cond ==> acc(P(args), old[perm_temp_quasihavoc_](perm(P(args))))
inhale forall vars :: { P(args) } cond ==> acc(P(args), old[perm_temp_quasihavoc_](perm(P(args))))

This partially addresses #438.