Simplify generated code for variable declarations with initialization expressions

[jcp19]

Shared variables

Whenever we have an assignment of the form

x@ := expr // of type T

Gobra translates this as following (internal representation)

init x
*x = expr

At the Viper level, this is expanded roughly to

// init
inhale footprint x && *x == dflt[T]

// assign
exhale footprint x
inhale footprint x
inhale *x == [ expr ]

This PR simplifies that to

// init
inhale footprint x
inhale *x === [ expr ]

Non-shared variables

x := expr // of type T

Gobra translates this as following (internal representation)

init x
x = expr

At the Viper level, this is expanded roughly to

x := dflt[T]
x := [ expr ]

Instead, this PR encodes it as follows

inhale x === [ expr ]

PS: in both cases, the new encoding is only applied if the identifier is being defined. otherwise, it uses the old encoding.

[Felalolf]

The desugarer is not the place to generate inhales to encode assignments. This is clearly part of the encoding. I liked your idea of adding an argument to the initialize node. I think you should do that instead.

[Felalolf]

Also, I would not mix code analysis and the desugarer. The necessary information for the desugaring step should be collecting by the Info object. The main concern is that the desugarer is getting way too complicated and hard to maintain.

[Felalolf]

If it is ultra urgent, then you could introduce another internal node, e.g. "InitialAssignment" and then replace the inhales with that. That would still be an ugly solution, but at it maintaines the separation of purposes somewhat.

[jcp19]

This may be a nice use-case for quasi-havoc