Array Pointer Shorthand

[gottschali]

For a of pointer to array type: a[x] is shorthand for (*a)[x] (go spec)

This is currently not handled by Gobra and one must explicitly dereference the pointers.
The specs can get hard to read:

// @ preserves acc(&((*p)[0]))
// @ ensures (*p)[0] == 0
func dereferencing(p *[10]int) {
	(*p)[0] = 0
}

We should be able to write:

// @ preserves acc(&p[0])
// @ ensures p[0] == 0
func shorthand(p *[10]int) {
	p[0] = 0
}

15:18:02.095 [main] ERROR viper.gobra.GobraRunner$ - An assumption was violated during execution.
15:18:02.096 [main] ERROR viper.gobra.GobraRunner$ - Logic error: Expected slice, array, map, or sequence, but got *[10]int
viper.gobra.util.Violation$LogicException: Logic error: Expected slice, array, map, or sequence, but got *[10]int

For pointers to structs the indirection works:

func structs() {
	p := new(struct{ value int })
	p.value = 1
	//@ assert p.value == 1
}