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.

[marcoeilers]

@Dev-XYS: I remembered why I added the uniqueName stuff: Since this is a Viper-to-Viper rewrite, I need a name that's unique inside the Viper program, not just in the final Boogie program. And unfortunately, it doesn't look like I can just create an Identifier and extract a unique name, since the unique names are only generated while pretty-printing the Boogie AST. So I don't think there is an easy way to use the existing namespace mechanism here; do you see one? If not, I'll at least move this uniqueName stuff somewhere else; getting unique names in a Viper program seems like a general enough problem that there should probably be a solution in Silver.

[Dev-XYS]

I see the issue now. The current namespace mechanism indeed works only for Boogie names. Let's keep your changes and improve it as needed in the future.