Skip to content

Commit 84a39b9

Browse files
authored
Add a test that deallocates a stack variable (rust-lang#2717)
1 parent 94eb92b commit 84a39b9

File tree

2 files changed

+21
-0
lines changed

2 files changed

+21
-0
lines changed

tests/expected/dealloc/stack/expected

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
Status: FAILURE\
2+
Description: "free argument must be dynamic object"
3+
4+
VERIFICATION:- FAILED

tests/expected/dealloc/stack/test.rs

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
use std::alloc::{dealloc, Layout};
5+
6+
// This test checks that Kani flags the deallocation of a stack-allocated
7+
// variable
8+
9+
#[kani::proof]
10+
fn check_dealloc_stack() {
11+
let mut x = 6;
12+
let layout = Layout::new::<i32>();
13+
let p = &mut x as *mut i32;
14+
unsafe {
15+
dealloc(p as *mut u8, layout);
16+
}
17+
}

0 commit comments

Comments
 (0)