Skip to content

Commit 12ff35f

Browse files
Add tests checking if Kani detects dangling pointer dereference inside println macro (rust-lang#3280)
Extract tests from the discussion in rust-lang#3235. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val <celinval@amazon.com>
1 parent cce55d4 commit 12ff35f

File tree

2 files changed

+60
-0
lines changed

2 files changed

+60
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
Checking harness unsafe_block...
2+
3+
Status: FAILURE\
4+
Description: "dereference failure: pointer invalid"\
5+
in function unsafe_block
6+
7+
VERIFICATION:- FAILED
8+
9+
Checking harness general_unsafe...
10+
11+
Status: FAILURE\
12+
Description: "dereference failure: pointer invalid"\
13+
in function general_unsafe
14+
15+
VERIFICATION:- FAILED
16+
17+
Checking harness local_unsafe...
18+
19+
Status: FAILURE\
20+
Description: "dereference failure: dead object"\
21+
in function local_unsafe
22+
23+
VERIFICATION:- FAILED
24+
25+
Summary:
26+
Verification failed for - unsafe_block
27+
Verification failed for - general_unsafe
28+
Verification failed for - local_unsafe
29+
Complete - 0 successfully verified harnesses, 3 failures, 3 total.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
// kani-flags: -Z ptr-to-ref-cast-checks
4+
5+
//! These tests check that Kani correctly detects dangling pointer dereference inside println macro.
6+
//! Related issue: <https://github.com/model-checking/kani/issues/3235>.
7+
8+
fn reference_dies() -> *mut i32 {
9+
let mut x: i32 = 2;
10+
&mut x as *mut i32
11+
}
12+
13+
#[kani::proof]
14+
fn local_unsafe() {
15+
let x = reference_dies();
16+
println!("My pointer, {}", unsafe { *x });
17+
}
18+
19+
#[kani::proof]
20+
unsafe fn general_unsafe() {
21+
let x = reference_dies();
22+
println!("My pointer, {}", *x);
23+
}
24+
25+
#[kani::proof]
26+
fn unsafe_block() {
27+
let x = reference_dies();
28+
unsafe {
29+
println!("{}", *x);
30+
}
31+
}

0 commit comments

Comments
 (0)