OnceCell

tests/expected/function-contract/interior-mutability/cell.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, UnsafeCell};
+use std::cell::{Cell, OnceCell, UnsafeCell};
 use std::mem::transmute;
 
 trait ToHack<T: ?Sized> {
@@ -21,6 +21,12 @@ impl<T: ?Sized> ToHack<T> for Cell<T> {
     }
 }
 
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+    unsafe fn hack(&self) -> &Option<T> {
+        transmute(self)
+    }
+}
+
 // ---------------------------------------------------
 
 struct InteriorMutability {

tests/expected/function-contract/interior-mutability/oncecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ x.x.hack() }.is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/oncecell.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::{Cell, OnceCell, UnsafeCell};
+use std::mem::transmute;
+
+trait ToHack<T: ?Sized> {
+    unsafe fn hack(&self) -> &T;
+}
+
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
+    unsafe fn hack(&self) -> &T {
+        transmute(self)
+    }
+}
+
+impl<T: ?Sized> ToHack<T> for Cell<T> {
+    unsafe fn hack(&self) -> &T {
+        transmute(self)
+    }
+}
+
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+    unsafe fn hack(&self) -> &Option<T> {
+        transmute(self)
+    }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+    x: OnceCell<u32>,
+}
+
+#[kani::requires(unsafe{x.x.hack()}.is_none())]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| unsafe{x.x.hack()}.is_some())]
+fn modify(x: &InteriorMutability) {
+    x.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+    let x: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+    modify(&x)
+}

tests/expected/function-contract/interior-mutability/unsafecell.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-use std::cell::{Cell, UnsafeCell};
+use std::cell::{Cell, OnceCell, UnsafeCell};
 use std::mem::transmute;
 
 trait ToHack<T: ?Sized> {
@@ -21,6 +21,12 @@ impl<T: ?Sized> ToHack<T> for Cell<T> {
     }
 }
 
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+    unsafe fn hack(&self) -> &Option<T> {
+        transmute(self)
+    }
+}
+
 // ---------------------------------------------------
 
 struct InteriorMutability {