Syntactic sugar in the parser to allow statements in expression positions

[viper-admin]

Created by @mschwerhoff on 2016-04-08 10:07
Last updated on 2017-11-26 15:34

A common mistake is writing

var x: Ref := new(*)

which is not allowed since x := new is a statement (which happens to look like a regular assignment). The above could be automatically desugared into

var x: Ref
x := new(*)

Statements in expression positions could in general be allowed by the parser, and internally rewritten by pulling out nested statements and storing them in temporary variables. Bernhard Brodowsky essentially did then in his master's thesis on translating Scala to Silver.

Another example:

#!text

method f(n: Int) returns (res: Int)
{
	if (n > 100) { res := n - 10}
	else {
		res := f(f(n + 11))
	}
}

[viper-admin]

@mschwerhoff commented on 2017-11-26 15:34

See also #157