Obviously true precondition "doesn't hold" when using predicate
ArmborstL opened this issue · 1 comments
The file below is a reduced version to highlight the problem:
function nonNull(): Ref
ensures result != null
function check(min_value1: Ref): Bool
requires min_value1 != null
predicate pred(nl: Ref) {
check(nonNull())
}
function funThatUnfolds( nl: Ref): Int
requires acc(pred( nl), write)
{
unfolding acc(pred(nl), write) in 1
}
function funThatUses(nl: Ref): Seq[Ref]
requires acc(pred(nl), write)
ensures |result| == funThatUnfolds(nl)
The function check
requires its argument to be non-null, and nonNull
never returns null. So everything should be fine.
However, Silicon reports for the call check(nonNull())
inside the predicate that the precondition of check
might not hold:
"Precondition of function check might not hold. Assertion nonNull() != null might not hold. (P.vpr@9.2--9.18)"
The error disappears if the predicate is not unfolded in funThatUnfolds
. It also disappears if funThatUnfolds
is not used in funThatUses
.
The issue occurs in the Viper VSCode plugin (version reported as Viper v4.3.1, seems to be most recent), as well as Silicon as used by VerCors (which uses commit 529d2a4).
The issue is that Silicon verifies funThatUnfolds
before nonNull
, and thus the postcondition of nonNull
is not available yet. Silicon computes which functions rely on which other functions to determine in what order to verify the functions, but by default does not take dependencies through a predicate unfolding (like in this case) into account.
This behavior can be changed by using the flag --alternativeFunctionVerificationOrder
(which unfortunately can lead to incompleteness in other cases, which is why it's not the default), and then the file verifies.