No read permission when accessing slice via for-range loop instead of for loop

[ThomasMayerl]

When trying to access the elements of a slice that is in a struct behind a pointer using a for-range loop, Gobra reports that there might be insufficient read permissions to the range expression. However, when replacing the for-range loop with a for loop over the slice indices and accessing the slice manually, it verifies.

Consider the following struct:

type Foo struct {
    Bar []int
}

The following function does not verify:

preserves acc(foo) && len(foo.Bar) > 0 && forall k int :: 0 <= k && k < len(foo.Bar) ==> acc(&foo.Bar[k])
func ptr_does_not_work(foo *Foo) int {
    tmp := 0
    invariant acc(foo) && len(foo.Bar) > 0 && forall k int :: 0 <= k && k < len(foo.Bar) ==> acc(&foo.Bar[k])
    invariant 0 <= i && i <= len(foo.Bar)
    for i, j := range foo.Bar {
        tmp += j + i
    }
    return tmp
}

Now we change the for range loop to a classic for loop. The code now verifies:

preserves acc(foo) && len(foo.Bar) > 0 && forall k int :: 0 <= k && k < len(foo.Bar) ==> acc(&foo.Bar[k])
func ptr_works(foo *Foo) int {
    tmp := 0
    invariant acc(foo) && len(foo.Bar) > 0 && forall k int :: 0 <= k && k < len(foo.Bar) ==> acc(&foo.Bar[k])
    invariant 0 <= i && i <= len(foo.Bar)
    //for i, j := range foo.Bar {
    for i := 0; i < len(foo.Bar); i++ {
        j := foo.Bar[i]
        tmp += j + i
    }
    return tmp
}

If the struct is not behind a pointer, the for range loop works, too:

preserves len(foo.Bar) > 0 && forall k int :: 0 <= k && k < len(foo.Bar) ==> acc(&foo.Bar[k])
func noPtr(foo Foo) int {
    tmp := 0
    invariant len(foo.Bar) > 0 && forall k int :: 0 <= k && k < len(foo.Bar) ==> acc(&foo.Bar[k])
    invariant 0 <= i && i <= len(foo.Bar)
    for i, j := range foo.Bar {
        tmp += j + i
    }
    return tmp
}