viperproject/viperserver

Wrong error reported when cached

tdardinier opened this issue · 1 comments

When using the VSCode extension for Viper, I first get an error at the last line of this method, which is the expected behavior. However, when I verify the file a second time, I get a spurious error reported: The first assert x == 5, which should hold. I think this is due to how the server caches errors.

method wrong_assertion_false_when_cached() {
    var x: Int := 5
    assert x == 5 // Wrong cached error reported here
    x := 3
    assert x == 5 // Error here
}

There's finally a fix 🥳