fix tests

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

@@ -10,13 +10,11 @@ struct InteriorMutability {
     x: Cell<u32>,
 }
 
-/// contracts need to access im.x internal data through the api im.x.as_ptr
 #[kani::requires(im.x.get() < 100)]
 #[kani::modifies(im.x.as_ptr())]
 #[kani::ensures(|_| im.x.get() < 101)]
 ///im is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
-    // valid rust methodology for getting and setting value without breaking encapsulation
     im.x.set(im.x.get() + 1)
 }
 

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

@@ -9,7 +9,6 @@ struct InteriorMutability {
     x: UnsafeCell<u32>,
 }
 
-/// contracts need to access im.x internal data through im.x.get() with an unsafe raw pointer dereference
 #[kani::requires(unsafe{*im.x.get()} < 100)]
 #[kani::modifies(im.x.get())]
 #[kani::ensures(|_| unsafe{*im.x.get()} < 101)]

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

@@ -15,7 +15,6 @@ struct InteriorMutability {
 #[kani::ensures(|_| im.x.get() < 101)]
 ///im is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
-    // valid rust methodology for getting and setting value without breaking encapsulation
     im.x.set(im.x.get() + 1)
 }
 

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

@@ -14,7 +14,6 @@ struct InteriorMutability {
 #[kani::modifies(&im.x)]
 #[kani::ensures(|_| im.x.get().is_some())]
 fn modify(im: &InteriorMutability) {
-    // method for setting value in OnceCell without breaking encapsulation
     im.x.set(5).expect("")
 }
 

tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs

@@ -15,7 +15,6 @@ struct InteriorMutability {
 #[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)]
 ///im is an immutable reference with interior mutability
 fn modify(im: &InteriorMutability) {
-    // valid rust methodology for getting and setting value without breaking encapsulation
     im.x.replace_with(|&mut old| old + 1);
 }
 

tests/expected/function-contract/interior-mutability/transmute/cell.expected → tests/expected/function-contract/transmute/cell.expected

@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| *unsafe{ im.x.expose() } < 101"\
+- Description: "|_| *unsafe{ x.expose() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL

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

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct
+/// This is a valid but not recommended alternative to havocing Cell
 
 /// ---------------------------------------------------
 ///        Abstraction Breaking Functionality
@@ -26,23 +26,16 @@ impl<T: ?Sized> Exposeable<T> for Cell<T> {
 ///                      Test Case
 /// ---------------------------------------------------
 
-/// This struct is contains Cell which can be mutated
-struct InteriorMutability {
-    x: Cell<u32>,
-}
-
-/// contracts need to access im.x internal data through the unsafe function im.x.expose()
-#[kani::requires(*unsafe{im.x.expose()} < 100)]
-#[kani::modifies(im.x.expose())]
-#[kani::ensures(|_| *unsafe{im.x.expose()} < 101)]
-///im is an immutable reference with interior mutability
-fn modify(im: &InteriorMutability) {
+#[kani::requires(*unsafe{x.expose()} < 100)]
+#[kani::modifies(x.expose())]
+#[kani::ensures(|_| *unsafe{x.expose()} < 101)]
+fn modify(x: &Cell<u32>) {
     // valid rust methodology for getting and setting value without breaking encapsulation
-    im.x.set(im.x.get() + 1)
+    x.set(x.get() + 1)
 }
 
 #[kani::proof_for_contract(modify)]
 fn harness_for_modify() {
-    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
-    modify(&im)
+    let x = Cell::new(kani::any());
+    modify(&x)
 }

tests/expected/function-contract/interior-mutability/transmute/unsafecell.expected → tests/expected/function-contract/transmute/unsafecell.expected

@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| *unsafe{ im.x.expose() } < 101"\
+- Description: "|_| *unsafe{ x.expose() } < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL

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

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct
+/// This is a valid but not recommended alternative to havocing UnsafeCell
 
 /// ---------------------------------------------------
 ///        Abstraction Breaking Functionality
@@ -26,22 +26,15 @@ impl<T: ?Sized> Exposeable<T> for UnsafeCell<T> {
 ///                      Test Case
 /// ---------------------------------------------------
 
-/// This struct is contains UnsafeCell which can be mutated
-struct InteriorMutability {
-    x: UnsafeCell<u32>,
-}
-
-/// contracts need to access im.x internal data through the unsafe function im.x.expose()
-#[kani::requires(*unsafe{im.x.expose()} < 100)]
-#[kani::modifies(im.x.expose())]
-#[kani::ensures(|_| *unsafe{im.x.expose()} < 101)]
-///im is an immutable reference with interior mutability
-fn modify(im: &InteriorMutability) {
-    unsafe { *im.x.get() += 1 }
+#[kani::requires(*unsafe{x.expose()} < 100)]
+#[kani::modifies(x.expose())]
+#[kani::ensures(|_| *unsafe{x.expose()} < 101)]
+fn modify(x: &UnsafeCell<u32>) {
+    unsafe { *x.get() += 1 }
 }
 
 #[kani::proof_for_contract(modify)]
 fn harness_for_modify() {
-    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
-    modify(&im)
+    let x = UnsafeCell::new(kani::any());
+    modify(&x)
 }