Better handling of reserved Gobra keywords

[wytseoortwijn]

The specification language of Gobra has several extra reserved keywords, in addition to the ones already reserved by Go. One example would be the get(e) destructor for expressions e of an option type. However, it could be very annoying to have some of these keywords, like get, reserved.

One possibility to fix this, is to make gobra a reserved keyword and to write e.g. gobra.get(...) instead of get(...); and likewise with all other keywords reserved by Gobra.

One disadvantage of this however, is that it might somewhat clutter expressions. For example some(e1 union e2 setminus e3) would become gobra.some(e1 gobra.union e2 gobra.setminus e3).

[witemap]

I noticed this issue as well. The problem with reserved keywords also extends to fields of a type. For example len is a perfectly valid field name in a Go program (see https://go.dev/play/p/bx3W3OHLzbZ or https://github.com/golang/go/blob/master/src/container/list/list.go). But Gobra cannot parse programs that have len as the field name of a type. E.g. verification of the following program reports "unexpected len in structType, expecting '}'":

package` keywordissue

type Collection struct {
    len int
}

requires acc(c)
ensures  acc(c) && c.len == 1 + old(c.len)
func (c *Collection) incrementLen() {
    c.len++
}