Skip to content

Commit d689ea2

Browse files
author
Carolyn Zech
committed
Add test for pointer to constant memory allocation
This isn't related to issue 3904. In codegen_alloc_pointer, the GlobalAlloc::from call returns GlobalAlloc::Memory, so we already codegened it as a constant allocation prior to this PR. But I thought it would be good to have a test that exercises this case explicitly, and that demonstrates the difference between this case and the nested statics case, so I added it in this PR.
1 parent 21e9454 commit d689ea2

File tree

1 file changed

+24
-0
lines changed

1 file changed

+24
-0
lines changed
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Test that Kani can codegen statics that contain pointers to constant allocations.
5+
// Test taken from https://github.com/rust-lang/rust/issues/79738#issuecomment-1946578159
6+
7+
// alloc4 (static: BAR, size: 16, align: 8) {
8+
// ╾─────alloc3<imm>─────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........
9+
// }
10+
11+
// alloc3 (size: 4, align: 4) {
12+
// 2a 00 00 00 │ *...
13+
// }
14+
15+
// alloc1 (static: FOO, size: 16, align: 8) {
16+
// ╾─────alloc3<imm>─────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........
17+
// }
18+
pub static FOO: &[i32] = &[42];
19+
pub static BAR: &[i32] = &*FOO;
20+
21+
#[kani::proof]
22+
fn main() {
23+
assert_eq!(FOO.as_ptr(), BAR.as_ptr());
24+
}

0 commit comments

Comments
 (0)