@@ -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