henriman
henriman
Using the extended encoding (and adapting the generated Viper file, see #882), the above now fails as expected. However, there remain some problems. Firstly, this function cannot be verified successfully...
For `pure` functions, `low` occurring in the contract is also replaced by `true` (with `--hyperMode=on`; `--hyperMode=off` leads to a crash). This is limiting when we need to establish that `low(len(a))...
This bug also occurs when unfolding a predicate *not* containing `low` in an assertion or pre- or postcondition, in order to assert `low`. ```go pred Mem(x *int) { acc(x) }...
hyperGobra crashes when comparing value accessed through `unfolding` a predicate that contains `low`
Edit: See #883 for the bug I describe in this comment. Note: If I use `assert (unfolding Pred(tmp) in low(tmp))` (instead of `true == ...`), I get the error `Permission...
hyperGobra crashes when comparing value accessed through `unfolding` a predicate that contains `low`
When specifying `--hyperMode=extended`, this (i.e. the "main" issue and what I describe in my comment) verifies successfully (after adapting the generated Viper file; see https://github.com/viperproject/gobra/issues/882).
When specifying `--hyperMode=extended`, this verifies successfully (after adapting the generated Viper file; see https://github.com/viperproject/gobra/issues/882).
Yes, we still get the same error messages then. --- I just noticed that the original title of this issue was incorrect, I corrected it now: the problem is that...
Likely related: `test1` verifies successfully, `test2` does not. ```go ghost hyper requires acc(ptr) decreases pure func IsLowPtr(ptr *int) bool { return low(*ptr) } requires acc(ptr) requires IsLowPtr(ptr) func test1(ptr *int)...
Also likely related: Gobra complains about insufficient permissions on call to `IsLowSlice` in `unfolding`. ```go type T []byte pred (t T) Mem() { acc(t) } ghost hyper requires acc(b) decreases...
The encoding used when specifying `--hyperMode=extended` is able to verify the quantified assertion (after adapting the generated Viper encoding; see #882).