fix rustc attribute issue

verus-lang · Feb 25, 2025 · 0ca21a4 · 0ca21a4
1 parent 1ad6468
commit 0ca21a4
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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 {