Skip to content

Wrong error reported when cached #23

Closed
@tdardinier

Description

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
}

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions