Skip to content

Commit d28ca19

Browse files
committed
fixup! Disable unsupported harnesses of trait contracts
1 parent b1bad7a commit d28ca19

File tree

1 file changed

+8
-4
lines changed

1 file changed

+8
-4
lines changed

library/alloc/src/alloc.rs

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -469,7 +469,8 @@ mod verify {
469469
}
470470
}
471471

472-
// TODO: disabled as Kani does not currently support contracts on traits
472+
// TODO: disabled as Kani does not currently support contracts on traits. See
473+
// https://github.com/model-checking/kani/issues/1997
473474
// // unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout)
474475
// #[kani::proof_for_contract(Allocator::deallocate)]
475476
// pub fn check_deallocate() {
@@ -481,7 +482,8 @@ mod verify {
481482
// }
482483
// }
483484

484-
// TODO: disabled as Kani does not currently support contracts on traits
485+
// TODO: disabled as Kani does not currently support contracts on traits. See
486+
// https://github.com/model-checking/kani/issues/1997
485487
// // unsafe fn grow(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
486488
// #[kani::proof_for_contract(Allocator::grow)]
487489
// pub fn check_grow() {
@@ -493,7 +495,8 @@ mod verify {
493495
// }
494496
// }
495497

496-
// TODO: disabled as Kani does not currently support contracts on traits
498+
// TODO: disabled as Kani does not currently support contracts on traits. See
499+
// https://github.com/model-checking/kani/issues/1997
497500
// // unsafe fn grow_zeroed(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
498501
// #[kani::proof_for_contract(Allocator::grow_zeroed)]
499502
// pub fn check_grow_zeroed() {
@@ -505,7 +508,8 @@ mod verify {
505508
// }
506509
// }
507510

508-
// TODO: disabled as Kani does not currently support contracts on traits
511+
// TODO: disabled as Kani does not currently support contracts on traits. See
512+
// https://github.com/model-checking/kani/issues/1997
509513
// // unsafe fn shrink(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
510514
// #[kani::proof_for_contract(Allocator::shrink)]
511515
// pub fn check_shrink() {

0 commit comments

Comments
 (0)