Open celinval opened 3 days ago
Note that a normal harness where we havoc using kani::any()
succeeds:
/// Without contracts, we can safely verify `next`.
#[kani::proof]
fn check_next_directly() {
// First check that initial iteration returns 0 (base case).
let first = next();
assert_eq!(first, 0);
// Havoc WRAP_COUNTER and invoke next.
unsafe { WRAP_COUNTER = kani::any() };
let ret = next();
kani::cover!(ret == 0);
}
Result:
Checking harness check_next_directly...
VERIFICATION RESULT:
** 0 of 41 failed
** 1 of 1 cover properties satisfied
VERIFICATION:- SUCCESSFUL
Verification Time: 0.3075676s
One possible solution is to disable CBMC static havoc and initialize all reachable mutable static variables as part of the kani::internal::init_contracts()
function.
I tried this code:
using the following command line invocation:
with Kani version: 0.52.0
I expected to see this happen: Verification succeeds
Instead, this happened: Verification fails because WRAP_COUNTER is havoc and it can contain an invalid discriminant. Thus, the match statement unreachable block is reached.