Repository navigation
Add non-fatal failure check to rmc prelude #695
Description
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.
Activity
celinval commentedon Dec 14, 2021
Note to self: Revert the hack made to the existing testcases here: #687
adpaco commentedon Nov 23, 2022
Found this issue while looking for "shuffle"... Is this something we still want?
celinval commentedon Nov 24, 2022
I'm OK closing this.
tedinski commentedon Nov 28, 2022
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
assertaborts execution.carolynzech commentedon Jan 9, 2025
@celinval should we close this as "won't do? given #3561?
celinval commentedon Jan 10, 2025
Closing this one since we haven't found any use case for it.