You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Requested feature: Loop contracts
Use case: Verify the provided loop contracts, and use the loop contracts to abstract out the loops from the verification process.
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167
Test case:
#[kani::proof]fnmain(){letmut x:u64 = kani::any_where(|i| *i >= 1);#[kani::loop_invariant(x >= 1)]while x > 1{
x = x - 1;};assert!(x == 1);}
The text was updated successfully, but these errors were encountered:
Requested feature: Loop contracts
Use case: Verify the provided loop contracts, and use the loop contracts to abstract out the loops from the verification process.
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167
Test case:
The text was updated successfully, but these errors were encountered: