viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
111 stars 28 forks source link

Losing array length information of field in outline #760

Open Dspil opened 6 months ago

Dspil commented 6 months ago

The assertion in the following code snippet fails although it should be obvious from the type of x.m.

package pkg

type A struct {
    m [6]int
}

requires acc(&x.m)
func f(x *A) {
    preserves acc(&x.m)
    outline (
        assert len(x.m) == 6 // this assertion fails
    )
}