Prefer using the macro over calling span_err

AeneasVerif · Jan 14, 2025 · b74925f · b74925f
1 parent 44858e1
commit b74925f
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 20 deletions.
diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
@@ -98,12 +98,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             | FullDefKind::TyParam { .. }
             | FullDefKind::Variant { .. } => {
                 let span = self.def_span(def_id);
-                self.span_err(
+                register_error!(
+                    self,
                     span,
-                    &format!(
-                        "Cannot register this item: `{def_id:?}` with kind `{:?}`",
-                        def.kind()
-                    ),
+                    "Cannot register this item: `{def_id:?}` with kind `{:?}`",
+                    def.kind()
                 );
             }
         }
@@ -124,12 +123,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             let span = ctx.def_span(rust_id);
             // Catch cycles
             let res = if ctx.translate_stack.contains(&trans_id) {
-                ctx.span_err(
+                register_error!(
+                    ctx,
                     span,
-                    &format!(
-                        "Cycle detected while translating {rust_id:?}! Stack: {:?}",
-                        &ctx.translate_stack
-                    ),
+                    "Cycle detected while translating {rust_id:?}! Stack: {:?}",
+                    &ctx.translate_stack
                 );
                 Err(())
             } else {
@@ -160,10 +158,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             };
 
             if res.is_err() {
-                ctx.span_err(
-                    span,
-                    &format!("Item `{rust_id:?}` caused errors; ignoring."),
-                );
+                register_error!(ctx, span, "Item `{rust_id:?}` caused errors; ignoring.");
                 ctx.errors.borrow_mut().ignore_failed_decl(trans_id);
             }
         })

diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -588,7 +588,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             let rename = renames.next();
             if renames.next().is_some() {
                 let span = self.translate_span_from_hax(&def.span);
-                self.span_err(
+                register_error!(
+                    self,
                     span,
                     "There should be at most one `charon::rename(\"...\")` \
                     or `aeneas::rename(\"...\")` attribute per declaration",
@@ -798,7 +799,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     Ok(a) => Some(a),
                     Err(msg) => {
                         let span = self.translate_span_from_hax(&attr.span);
-                        self.span_err(span, &format!("Error parsing attribute: {msg}"));
+                        register_error!(self, span, "Error parsing attribute: {msg}");
                         None
                     }
                 }

diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -193,8 +193,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) {
             Ok(res) => Ok(res),
             Err(err) => {
-                let msg = format!("Error during trait resolution: {}", &err.msg);
-                self.span_err(span, &msg);
+                register_error!(self, span, "Error during trait resolution: {}", &err.msg);
                 Ok(TraitRef {
                     kind: TraitRefKind::Unknown(err.msg),
                     trait_decl_ref,
@@ -329,8 +328,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     trait_decl_ref,
                 };
                 if self.error_on_impl_expr_error {
-                    let error = format!("Error during trait resolution: {}", msg);
-                    self.span_err(span, &error);
+                    register_error!(self, span, "Error during trait resolution: {}", msg);
                 }
                 trait_ref
             }