Skip to content

Commit

Permalink
Forgot that this now needs formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
JustusAdam committed Feb 1, 2024
1 parent 9b17d94 commit 52e703a
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions tests/expected/function-contract/modifies/unsafe_rc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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());
}
Expand Down

0 comments on commit 52e703a

Please sign in to comment.