Skip to content

Commit

Permalink
Add comment explaining test case
Browse files Browse the repository at this point in the history
  • Loading branch information
karkhaz committed Mar 13, 2024
1 parent d77ac68 commit 5ba148a
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions tests/expected/dead-invalid-access-via-raw/main.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,17 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// This test checks an issue reported in github.com/model-checking/kani#3063.
// The access of the raw pointer should fail because the value being dereferenced has gone out of
// scope at the time of access.

#[kani::proof]
pub fn check_invalid_ptr() {
let raw_ptr = {
let var = 10;
&var as *const _
};

// This should fail since it is de-referencing a dead object.
assert_eq!(unsafe { *raw_ptr }, 10);
}

0 comments on commit 5ba148a

Please sign in to comment.