From 0ca21a4a1fd05570e2b3f8cf8d3459cabd796580 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 25 Feb 2025 16:15:42 +0100
Subject: [PATCH] fix rustc attribute issue

---
 source/rust_verify/src/attributes.rs         | 21 ++++++++++++++++++--
 source/rust_verify/src/context.rs            | 10 ++++++++++
 source/rust_verify/src/rust_to_vir_global.rs |  2 +-
 3 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs
index a79cbb4b61..2b969cf446 100644
--- a/source/rust_verify/src/attributes.rs
+++ b/source/rust_verify/src/attributes.rs
@@ -978,6 +978,21 @@ pub(crate) fn get_external_attrs(
 pub(crate) fn get_verifier_attrs(
     attrs: &[Attribute],
     diagnostics: Option<&mut Vec<VirErrAs>>,
+) -> Result<VerifierAttrs, VirErr> {
+    get_verifier_attrs_maybe_check(attrs, diagnostics, true)
+}
+
+pub(crate) fn get_verifier_attrs_no_check(
+    attrs: &[Attribute],
+    diagnostics: Option<&mut Vec<VirErrAs>>,
+) -> Result<VerifierAttrs, VirErr> {
+    get_verifier_attrs_maybe_check(attrs, diagnostics, false)
+}
+
+pub(crate) fn get_verifier_attrs_maybe_check(
+    attrs: &[Attribute],
+    diagnostics: Option<&mut Vec<VirErrAs>>,
+    do_check: bool,
 ) -> Result<VerifierAttrs, VirErr> {
     let mut vs = VerifierAttrs {
         verus_macro: false,
@@ -1096,8 +1111,10 @@ pub(crate) fn get_verifier_attrs(
             _ => {}
         }
     }
-    if let Some((rustc_attr, span)) = unsupported_rustc_attr {
-        return err_span(span, format!("The attribute `{rustc_attr:}` is not supported"));
+    if do_check {
+        if let Some((rustc_attr, span)) = unsupported_rustc_attr {
+            return err_span(span, format!("The attribute `{rustc_attr:}` is not supported"));
+        }
     }
     Ok(vs)
 }
diff --git a/source/rust_verify/src/context.rs b/source/rust_verify/src/context.rs
index 19d18322eb..e8f0ffcaf0 100644
--- a/source/rust_verify/src/context.rs
+++ b/source/rust_verify/src/context.rs
@@ -58,6 +58,16 @@ impl<'tcx> ContextX<'tcx> {
         crate::attributes::get_verifier_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut()))
     }
 
+    pub(crate) fn get_verifier_attrs_no_check(
+        &self,
+        attrs: &[Attribute],
+    ) -> Result<crate::attributes::VerifierAttrs, vir::ast::VirErr> {
+        crate::attributes::get_verifier_attrs_no_check(
+            attrs,
+            Some(&mut *self.diagnostics.borrow_mut()),
+        )
+    }
+
     pub(crate) fn get_external_attrs(
         &self,
         attrs: &[Attribute],
diff --git a/source/rust_verify/src/rust_to_vir_global.rs b/source/rust_verify/src/rust_to_vir_global.rs
index 2a7e532aee..af5b9bb926 100644
--- a/source/rust_verify/src/rust_to_vir_global.rs
+++ b/source/rust_verify/src/rust_to_vir_global.rs
@@ -22,7 +22,7 @@ pub(crate) fn process_const_early<'tcx>(
     item: &Item<'tcx>,
 ) -> Result<(), VirErr> {
     let attrs = ctxt.tcx.hir().attrs(item.hir_id());
-    let vattrs = ctxt.get_verifier_attrs(attrs)?;
+    let vattrs = ctxt.get_verifier_attrs_no_check(attrs)?;
     if vattrs.size_of_global {
         let err = crate::util::err_span(item.span, "invalid global size_of");
         let ItemKind::Const(_ty, generics, body_id) = item.kind else {