Unsoundness due to loop invariant

[bruggerl]

If you run Silicon with option --numberOfErrorsToReport=0 on the Viper code below, it successfully detects the failing assert false inside the loop, but fails to catch the error which should arise from the second assert false at the end of the method, even though it should report both errors. Using the second invariant which is commented out in the snippet below instead of the first one solves the problem, although the invariants are actually equivalent.

field f: Bool

method test()
{
    var curr: Ref := null

    while (curr != null)
        invariant curr != null ==> acc(curr.f) // problematic invariant
        // invariant acc(curr.f, curr != null ? write : none) // if you use this invariant instead, it works as expected
    {
        assert false // error detected
        curr := null
    }
    assert false // no error detected
}

[vakaras]

The original example was:

field f: Bool

method fails(a: Bool)
{
    var curr: Ref := null

    while (curr != null) 
        invariant curr != null ==> acc(curr.f)
    {
        refute false
        curr := null
    }

    assert false
}

This verifies, while it clearly should not.

[marcoeilers]

Fixed in PR #741