Skip to content

Commit 4b925fd

Browse files
authored
Avoid undefined behavior in AnySlice::new() (rust-lang#2288)
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 878e5b9 commit 4b925fd

File tree

2 files changed

+26
-1
lines changed

2 files changed

+26
-1
lines changed

library/kani/src/slice.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
7171
// *(ptr as *mut T).add(i) = any();
7272
// }
7373
while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
74-
*any_slice.ptr.add(i) = any();
74+
std::ptr::write(any_slice.ptr.add(i), any());
7575
i += 1;
7676
}
7777
}

tests/kani/Slice/slice-drop.rs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Assigning to a memory location via pointer dereferencing causes Drop::drop to be called for the location to which the pointer points.
5+
// Here, kani::Arbitrary implementation for MyStruct deterministically sets MyStruct.0 to 1.
6+
// We check whether AnySlice will properly initialize memory making the assertion in drop() to pass.
7+
8+
struct MyStruct(i32);
9+
10+
impl Drop for MyStruct {
11+
fn drop(&mut self) {
12+
assert!(self.0 == 1);
13+
}
14+
}
15+
16+
impl kani::Arbitrary for MyStruct {
17+
fn any() -> Self {
18+
MyStruct(1)
19+
}
20+
}
21+
22+
#[kani::proof]
23+
fn my_proof() {
24+
let my_slice = kani::slice::any_slice::<MyStruct, 1>();
25+
}

0 commit comments

Comments
 (0)