Disallow use of ghost members in non-ghost code

[viper-admin]

Created by @ArquintL on 2020-06-19 09:45

I’ve observed that the following code snippet successfully verifies with Gobra. However, in my opinion this should only work if h is marked as a ghost variable.

package main

type Rectangle struct {
    Width, Height int
}

ghost
requires acc(r.Height)
ensures acc(r.Height)
pure func GetHeight(r *Rectangle) (res int) {
    return r.Height
}

func main() {
    r! := Rectangle{Width: 2, Height: 5}
    h := GetHeight(&r)
    assert h == GetHeight(&r) && h == 5
}

‌

[Felalolf]

Here is another example from Peter.
anotherExample.txt

[ArquintL]

This issue might have been fixed by #239