From 52e703a97caef2631749a2f751549fd32c573a67 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 31 Jan 2024 22:56:50 -0500 Subject: [PATCH] Forgot that this now needs formatting --- tests/expected/function-contract/modifies/unsafe_rc.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/expected/function-contract/modifies/unsafe_rc.rs b/tests/expected/function-contract/modifies/unsafe_rc.rs index e3e210f73a8b..81cc65ce9957 100644 --- a/tests/expected/function-contract/modifies/unsafe_rc.rs +++ b/tests/expected/function-contract/modifies/unsafe_rc.rs @@ -2,10 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts +use std::ops::Deref; /// Illustrates the problem from https://github.com/model-checking/kani/issues/2907 - use std::rc::Rc; -use std::ops::Deref; #[kani::modifies({ let intref : &u32 = ptr.deref().deref(); @@ -19,7 +18,7 @@ fn modify(ptr: Rc<&mut u32>) { #[kani::proof_for_contract(modify)] fn main() { - let mut i : u32 = kani::any(); + let mut i: u32 = kani::any(); let ptr = Rc::new(&mut i); modify(ptr.clone()); }