Name the other Rc test case 'fixme'

model-checking · Jan 31, 2024 · 9b17d94 · 9b17d94
1 parent 6bbbb24
commit 9b17d94
Showing 1 changed file with 10 additions and 9 deletions.
diff --git a/...cted/function-contract/.unsafe_assigns_rc → ...d/function-contract/modifies/unsafe_rc.rs b/...cted/function-contract/.unsafe_assigns_rc → ...d/function-contract/modifies/unsafe_rc.rs
@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
+/// Illustrates the problem from https://github.com/model-checking/kani/issues/2907
+
 use std::rc::Rc;
 use std::ops::Deref;
 
@@ -22,12 +24,11 @@ fn main() {
     modify(ptr.clone());
 }
 
-
-// #[kani::proof]
-// #[kani::stub_verified(modify)]
-// fn replace_modify() {
-//     let begin = kani::any_where(|i| *i < 100);
-//     let i = Rc::new(RefCell::new(begin));
-//     modify(i.clone());
-//     kani::assert(*i.borrow() == begin + 1, "end");
-// }
+#[kani::proof]
+#[kani::stub_verified(modify)]
+fn replace_modify() {
+    let begin = kani::any_where(|i| *i < 100);
+    let i = Rc::new(RefCell::new(begin));
+    modify(i.clone());
+    kani::assert(*i.borrow() == begin + 1, "end");
+}