Skip to content

Commit

Permalink
Cleanup stray comment
Browse files Browse the repository at this point in the history
With model-checking/kani#3670 having been
addressed we re-enabled harnesses in model-checking#211. Yet the comment explaining
previously-commented-out-harnesses stayed in place.

Removing it for it no longer applies.
  • Loading branch information
tautschnig committed Dec 10, 2024
1 parent 16a155a commit ec9c3d5
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions library/core/src/slice/iter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down

0 comments on commit ec9c3d5

Please sign in to comment.