File tree Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Original file line number Diff line number Diff line change 230
230
#![ feature( unboxed_closures) ]
231
231
#![ feature( unsized_fn_params) ]
232
232
#![ feature( with_negative_coherence) ]
233
+ // Required for Kani loop contracts, which are annotated as custom stmt attributes.
233
234
#![ feature( proc_macro_hygiene) ]
234
235
// tidy-alphabetical-end
235
236
//
Original file line number Diff line number Diff line change @@ -209,6 +209,7 @@ impl<'a> Iterator for Utf8Chunks<'a> {
209
209
let mut valid_up_to = 0 ;
210
210
// TODO: remove `LEN` and use `self.source.len()` directly once
211
211
// fix the issue that Kani loop contracts doesn't support `self`.
212
+ // Tracked in https://github.com/model-checking/kani/issues/3700
212
213
#[ cfg( kani) ]
213
214
let LEN = self . source . len ( ) ;
214
215
#[ safety:: loop_invariant( i <= LEN && valid_up_to == i) ]
@@ -301,9 +302,7 @@ impl FusedIterator for Utf8Chunks<'_> {}
301
302
#[ stable( feature = "utf8_chunks" , since = "1.79.0" ) ]
302
303
impl fmt:: Debug for Utf8Chunks < ' _ > {
303
304
fn fmt ( & self , f : & mut Formatter < ' _ > ) -> fmt:: Result {
304
- f. debug_struct ( "Utf8Chunks" )
305
- . field ( "source" , & self . debug ( ) )
306
- . finish ( )
305
+ f. debug_struct ( "Utf8Chunks" ) . field ( "source" , & self . debug ( ) ) . finish ( )
307
306
}
308
307
}
309
308
You can’t perform that action at this time.
0 commit comments