Shared Array Range

[gottschali]

For the following valid go program

package main

func sharedArrayRange1() {
	arr /*@@@*/ := [3]int{0, 1, 1}
	for i, a := range arr {
		arr[i] = a + 1
	}
}

Gobra reports a long error

17:42:34.877 [main] ERROR viper.gobra.GobraRunner$ - An assumption was violated during execution.
17:42:34.878 [main] ERROR viper.gobra.GobraRunner$ - Logic error: Node N0 (class viper.gobra.ast.internal.LocalVar) :: [3]int°° did not match with any implemented case of reference. 
viper.gobra.util.Violation$LogicException: Logic error: Node N0 (class viper.gobra.ast.internal.LocalVar) :: [3]int°° did not match with any implemented case of reference. 
	at viper.gobra.util.Violation$.violation(Violation.scala:27)
	at viper.gobra.translator.encodings.combinators.FinalTypeEncoding$$anonfun$expectedMatch$1.applyOrElse(FinalTypeEncoding.scala:23)
	at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
	at viper.gobra.translator.util.PartialFunctionCombiner$SafeCombiner$$anon$1.$anonfun$applyOrElse$1(PartialFunctionCombiner.scala:32)
	at scala.Option.getOrElse(Option.scala:201)
... omitted

full error.

If this is not supported in Gobra, the error could indicate this directly.

[gottschali]

If the range is only over the indices i there is no error

func sharedArrayRange2() {
	arr /*@@@*/ := [3]int{0, 1, 1}
	for i := range arr {
		arr[i] = arr[i] + 1
	}
	for i, _ := range arr {
		arr[i] = arr[i] + 1
	}
}