model-checking
Add non-fatal failure check to rmc prelude
Requested feature: Provide a mechanism for users to add property check to their code that do not abort the program when a failure occurs. Use case: This can be extremely helpful for adding more information to potential fatal failures without affecting the code path. This can also help while writing tests for RMC. Link to relevant documentation (Rust reference, Nomicon, RFC): Is this a breaking change? None
Test case:
/// Dummy verification harness that ensures that method shuffle generates a new array that has all the
/// elements from the source array.
#[rmc::proof]
fn check_shuffle() {
let a1: [u8; 5] = rmc::nondet();
let a2 = shuffle(&a1);
rmc::check(a2.size() == a1.size());
for x in &a1 {
rmc::check(a2.contains(x));
}
}
In this harness, it might be helpful to understand if 1 or more items are missing from the array. With rmc::check() we can easily verify all the elements and find as many failures as possible. If we replace rmc::check by assert the analysis would stop in the first failure.
Note to self: Revert the hack made to the existing testcases here: https://github.com/model-checking/rmc/pull/687
Found this issue while looking for "shuffle"... Is this something we still want?
I still want kani::check, re-opening unless I get overruled :)
I think it'd at least be good for ourselves writing tests, and possibly as extra documentation making it clear that assert aborts execution.
