From 7889a8988d76f5307d683f1781b6e918cd2091b8 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 16:57:11 -0600 Subject: [PATCH] Address comments --- library/core/src/lib.rs | 1 + library/core/src/str/lossy.rs | 5 ++--- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 7c0596768b784..2c813ca0cb412 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,6 +230,7 @@ #![feature(unboxed_closures)] #![feature(unsized_fn_params)] #![feature(with_negative_coherence)] +// Required for Kani loop contracts, which are annotated as custom stmt attributes. #![feature(proc_macro_hygiene)] // tidy-alphabetical-end // diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs index e1ede32295962..d6786eff487f3 100644 --- a/library/core/src/str/lossy.rs +++ b/library/core/src/str/lossy.rs @@ -209,6 +209,7 @@ impl<'a> Iterator for Utf8Chunks<'a> { let mut valid_up_to = 0; // TODO: remove `LEN` and use `self.source.len()` directly once // fix the issue that Kani loop contracts doesn't support `self`. + // Tracked in https://github.com/model-checking/kani/issues/3700 #[cfg(kani)] let LEN = self.source.len(); #[safety::loop_invariant(i <= LEN && valid_up_to == i)] @@ -301,9 +302,7 @@ impl FusedIterator for Utf8Chunks<'_> {} #[stable(feature = "utf8_chunks", since = "1.79.0")] impl fmt::Debug for Utf8Chunks<'_> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - f.debug_struct("Utf8Chunks") - .field("source", &self.debug()) - .finish() + f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish() } }