Skip to content

Commit 8902a9c

Browse files
committed
Remove test that can no longer be expected to compile, fmt
1 parent 1980ac0 commit 8902a9c

File tree

2 files changed

+5
-81
lines changed

2 files changed

+5
-81
lines changed

library/kani_core/src/mem.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@
1212
macro_rules! kani_mem {
1313
($core:tt) => {
1414
use super::kani_intrinsic;
15-
use $core::ptr::{DynMetadata, NonNull, Pointee};
1615
use $core::marker::MetaSized;
16+
use $core::ptr::{DynMetadata, NonNull, Pointee};
1717

1818
/// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2
1919
/// and 3.
@@ -122,7 +122,10 @@ macro_rules! kani_mem {
122122
}
123123

124124
#[allow(clippy::not_unsafe_ptr_arg_deref)]
125-
pub(super) fn same_allocation_internal<T: MetaSized>(ptr1: *const T, ptr2: *const T) -> bool {
125+
pub(super) fn same_allocation_internal<T: MetaSized>(
126+
ptr1: *const T,
127+
ptr2: *const T,
128+
) -> bool {
126129
let addr1 = ptr1 as *const ();
127130
let addr2 = ptr2 as *const ();
128131
cbmc::same_allocation(addr1, addr2)

tests/kani/MemPredicates/foreign_type.rs

Lines changed: 0 additions & 79 deletions
This file was deleted.

0 commit comments

Comments
 (0)