From ec9c3d5bdf04fa07b5f3d84bd758997364b20d19 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 Dec 2024 10:53:52 +0000 Subject: [PATCH] Cleanup stray comment With https://github.com/model-checking/kani/issues/3670 having been addressed we re-enabled harnesses in #211. Yet the comment explaining previously-commented-out-harnesses stayed in place. Removing it for it no longer applies. --- library/core/src/slice/iter.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 5ea9204a28fd0..fcf901e3c9f43 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3607,10 +3607,6 @@ mod verify { check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); - // FIXME: The functions that are commented out are currently failing verification. - // Debugging the issue is currently blocked by: - // https://github.com/model-checking/kani/issues/3670 - // // Public functions that call safe abstraction `make_slice`. check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| { iter.as_slice();