Format if-let chains

AeneasVerif · Jun 14, 2024 · ad01370 · ad01370
1 parent 442ed4c
commit ad01370
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 16 deletions.
diff --git a/charon/src/ast/llbc_ast_utils.rs b/charon/src/ast/llbc_ast_utils.rs
@@ -314,7 +314,9 @@ impl<'a, F: FnMut(&mut Statement) -> Option<Vec<Statement>>> MutAstVisitor
 
                 // Transform the current statement
                 let st_seq = (self.tr)(st1);
-                if let Some(seq) = st_seq && !seq.is_empty() {
+                if let Some(seq) = st_seq
+                    && !seq.is_empty()
+                {
                     take(st, |st| chain_statements(seq, st))
                 }
                 // TODO: we might want to apply tr to the whole resulting sequence
@@ -325,7 +327,9 @@ impl<'a, F: FnMut(&mut Statement) -> Option<Vec<Statement>>> MutAstVisitor
 
                 // Transform the current statement
                 let st_seq = (self.tr)(st);
-                if let Some(seq) = st_seq && !seq.is_empty() {
+                if let Some(seq) = st_seq
+                    && !seq.is_empty()
+                {
                     take(st, |st| chain_statements(seq, st))
                 }
             }

diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs
@@ -47,7 +47,8 @@ fn remove_dynamic_checks(ctx: &mut TransformCtx, block: &mut BlockData) {
         //   b := copy x == const 0
         //   assert(move b == false)
         [rest @ .., Statement {
-            content: RawStatement::Assign(is_zero, Rvalue::BinaryOp(BinOp::Eq, _, Operand::Const(_zero))),
+            content:
+                RawStatement::Assign(is_zero, Rvalue::BinaryOp(BinOp::Eq, _, Operand::Const(_zero))),
             ..
         }] if cond == is_zero && *expected == false => rest,
 
@@ -111,31 +112,34 @@ fn remove_dynamic_checks(ctx: &mut TransformCtx, block: &mut BlockData) {
         // blocks so we remove them in a later pass.
         [.., Statement {
             content:
-                RawStatement::Assign(result, Rvalue::BinaryOp(BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul, ..)),
+                RawStatement::Assign(
+                    result,
+                    Rvalue::BinaryOp(BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul, ..),
+                ),
             ..
         }] if cond.var_id == result.var_id
             && result.projection.is_empty()
-            && let [ProjectionElem::Field(FieldProjKind::Tuple(2), p_id)] = cond.projection.as_slice()
+            && let [ProjectionElem::Field(FieldProjKind::Tuple(2), p_id)] =
+                cond.projection.as_slice()
             && p_id.index() == 1
             && *expected == false =>
         {
             // We leave this assert intact; it will be silplified in
             // [`remove_arithmetic_overflow_checks`].
-            return
+            return;
         }
 
         _ => {
             // This can happen for the dynamic checks we don't handle, corresponding to the
             // `rustc_middle::mir::AssertKind` variants `ResumedAfterReturn`, `ResumedAfterPanic`
             // and `MisalignedPointerDereference`.
             let fmt_ctx = ctx.into_fmt();
-            let msg = format!("Found an `assert` we don't recognize:\n{}", block.fmt_with_ctx(&fmt_ctx));
-            register_error_or_panic!(
-                ctx,
-                block.terminator.span.span,
-                msg
+            let msg = format!(
+                "Found an `assert` we don't recognize:\n{}",
+                block.fmt_with_ctx(&fmt_ctx)
             );
-            return
+            register_error_or_panic!(ctx, block.terminator.span.span, msg);
+            return;
         }
     };
 

diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs
@@ -288,10 +288,11 @@ impl SharedTypeVisitor for Deps {
         // TODO: this is not very satisfying but this is the only way
         // we have of preventing mutually recursive groups between
         // method impls and trait impls in the presence of associated types...
-        if let Some(impl_id) = &self.impl_trait_id && impl_id == id {
+        if let Some(impl_id) = &self.impl_trait_id
+            && impl_id == id
+        {
             // Ignore
-        }
-        else {
+        } else {
             let id = AnyTransId::TraitImpl(*id);
             self.insert_edge(id);
         }

diff --git a/charon/src/translate/translate_traits.rs b/charon/src/translate/translate_traits.rs
@@ -516,7 +516,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             .associated_items(implemented_trait_rust_id)
             .in_definition_order()
         {
-            if let AssocKind::Fn = &item.kind && !item.defaultness(tcx).has_value() {
+            if let AssocKind::Fn = &item.kind
+                && !item.defaultness(tcx).has_value()
+            {
                 decl_required_methods.insert(item.name.to_string());
             }
         }