Unsoundness due to loop invariant
bruggerl opened this issue · 2 comments
bruggerl commented
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 commented
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 commented
Fixed in PR #741