File tree Expand file tree Collapse file tree 1 file changed +15
-15
lines changed
library/kani_macros/src/sysroot/loop_contracts Expand file tree Collapse file tree 1 file changed +15
-15
lines changed Original file line number Diff line number Diff line change @@ -234,24 +234,24 @@ fn transform_break_continue(block: &mut Block) {
234234
235235fn while_let_rewrite ( loopexpr : Stmt ) -> Stmt {
236236 if let Stmt :: Expr ( ref expr, _) = loopexpr {
237- if let Expr :: While ( ExprWhile { cond, body, .. } ) = expr {
238- if let Expr :: Let ( ref let_expr) = * * cond {
239- let pat = & let_expr . pat ;
240- let scrutinee = & let_expr. expr ;
241-
242- // Transform to loop with match
243- return parse_quote ! {
244- loop {
245- match #scrutinee {
246- #pat => #body ,
247- _ => break ,
248- }
249- } ;
237+ if let Expr :: While ( ExprWhile { cond, body, .. } ) = expr
238+ && let Expr :: Let ( ref let_expr) = * * cond
239+ {
240+ let pat = & let_expr. pat ;
241+ let scrutinee = & let_expr . expr ;
242+
243+ // Transform to loop with match
244+ return parse_quote ! {
245+ loop {
246+ match #scrutinee {
247+ #pat => #body ,
248+ _ => break ,
249+ }
250250 } ;
251- }
251+ } ;
252252 }
253253 }
254- return loopexpr. clone ( ) ;
254+ loopexpr. clone ( )
255255}
256256
257257pub fn loop_invariant ( attr : TokenStream , item : TokenStream ) -> TokenStream {
You can’t perform that action at this time.
0 commit comments