diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs
index 6957de2bcd..1c96899883 100644
--- a/source/rust_verify/src/attributes.rs
+++ b/source/rust_verify/src/attributes.rs
@@ -4,6 +4,7 @@ use rustc_ast::tokenstream::{TokenStream, TokenTree};
 use rustc_hir::{AttrArgs, Attribute};
 use rustc_span::Span;
 use vir::ast::{AcceptRecursiveType, Mode, TriggerAnnotation, VirErr, VirErrAs};
+use vir::messages::WarningAllow;
 
 /// The syntax tree of an attribute.
 ///
@@ -296,6 +297,8 @@ pub(crate) enum Attr {
     Memoize,
     // Override default rlimit
     RLimit(f32),
+    // suppress warning
+    Allow(WarningAllow),
     // Suppress the recommends check for narrowing casts that may truncate
     Truncate,
     // In order to apply a specification to a method externally
@@ -621,6 +624,18 @@ pub(crate) fn parse_attrs(
                     let number = get_rlimit_arg(*span, attrs)?;
                     v.push(Attr::RLimit(number));
                 }
+                AttrTree::Fun(span, arg, Some(box [AttrTree::Fun(_, s, None)]))
+                    if arg == "allow" =>
+                {
+                    if let Some(allow) = WarningAllow::from_str(s) {
+                        v.push(Attr::Allow(allow));
+                    } else {
+                        return err_span(
+                            *span,
+                            format!("unrecognized warning name for allow attribute: {s}"),
+                        );
+                    }
+                }
                 AttrTree::Fun(_, arg, None) if arg == "truncate" => v.push(Attr::Truncate),
                 AttrTree::Fun(_, arg, None) if arg == "external_fn_specification" => {
                     v.push(Attr::ExternalFnSpecification)
@@ -881,6 +896,60 @@ pub(crate) fn parse_attrs_walk_parents<'tcx>(
     }
 }
 
+fn is_allow_walk_parents<'tcx>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+    allow: &WarningAllow,
+) -> bool {
+    for attr in parse_attrs_walk_parents(tcx, def_id) {
+        if let Attr::Allow(a) = &attr {
+            if a == allow {
+                return true;
+            }
+        }
+    }
+    false
+}
+
+struct WarningDefId<'tcx>(rustc_middle::ty::TyCtxt<'tcx>, rustc_span::def_id::DefId);
+
+impl<'tcx> vir::messages::CheckAllowForWarning for WarningDefId<'tcx> {
+    fn allowed(&self, allow: &WarningAllow) -> bool {
+        let WarningDefId(tcx, def_id) = *self;
+        is_allow_walk_parents(tcx, def_id, allow)
+    }
+}
+
+pub(crate) fn warning_maybe<'tcx, S: Into<String>>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+    span: Span,
+    allow: &WarningAllow,
+    note: impl FnOnce() -> S,
+    emit: impl FnOnce(vir::messages::Message) -> (),
+) {
+    vir::messages::warning_maybe(
+        &WarningDefId(tcx, def_id),
+        &crate::spans::err_air_span(span),
+        allow,
+        note,
+        emit,
+    );
+}
+
+pub(crate) fn warning_config_walk_parents<'tcx>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+) -> vir::context::WarningConfig {
+    let mut allows = Vec::new();
+    for attr in parse_attrs_walk_parents(tcx, def_id) {
+        if let Attr::Allow(allow) = attr {
+            allows.push(allow.clone());
+        }
+    }
+    vir::context::WarningConfig(allows)
+}
+
 pub(crate) fn get_loop_isolation_walk_parents<'tcx>(
     tcx: rustc_middle::ty::TyCtxt<'tcx>,
     def_id: rustc_span::def_id::DefId,
@@ -1084,6 +1153,7 @@ pub(crate) struct VerifierAttrs {
     pub(crate) allow_complex_invariants: bool,
     pub(crate) memoize: bool,
     pub(crate) rlimit: Option<f32>,
+    pub(crate) allow_list: Vec<WarningAllow>,
     pub(crate) truncate: bool,
     pub(crate) external_fn_specification: bool,
     pub(crate) external_type_specification: bool,
@@ -1258,6 +1328,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
         allow_complex_invariants: false,
         memoize: false,
         rlimit: None,
+        allow_list: vec![],
         truncate: false,
         external_fn_specification: false,
         external_type_specification: false,
@@ -1341,6 +1412,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
             Attr::Memoize => vs.memoize = true,
             Attr::RLimit(rlimit) => vs.rlimit = Some(rlimit),
             Attr::Truncate => vs.truncate = true,
+            Attr::Allow(name) => vs.allow_list.push(name.clone()),
             Attr::UnwrappedBinding => vs.unwrapped_binding = true,
             Attr::Mode(_) => vs.sets_mode = true,
             Attr::InternalRevealFn => vs.internal_reveal_fn = true,
diff --git a/source/rust_verify/src/automatic_derive.rs b/source/rust_verify/src/automatic_derive.rs
index f843d45d4b..0bffc87ea1 100644
--- a/source/rust_verify/src/automatic_derive.rs
+++ b/source/rust_verify/src/automatic_derive.rs
@@ -6,6 +6,7 @@ use std::sync::Arc;
 use vir::ast::{
     BinaryOp, Expr, ExprX, FunctionX, Mode, Place, PlaceX, SpannedTyped, VirErr, VirErrAs,
 };
+use vir::messages::WarningAllow;
 
 /// Traits with special handling
 #[derive(Clone, Copy, Debug)]
@@ -64,6 +65,8 @@ pub fn is_automatically_derived(attrs: &[rustc_hir::Attribute]) -> bool {
 
 pub fn modify_derived_item<'tcx>(
     ctxt: &Context<'tcx>,
+    id: rustc_span::def_id::DefId,
+    inputs: &Vec<rustc_middle::ty::Ty>,
     span: Span,
     hir_id: HirId,
     action: &AutomaticDeriveAction,
@@ -75,7 +78,7 @@ pub fn modify_derived_item<'tcx>(
     match special {
         SpecialTrait::Clone => {
             if &*function.name.path.last_segment() == "clone" {
-                return clone_add_post_condition(ctxt, span, hir_id, function);
+                return clone_add_post_condition(ctxt, id, inputs, span, hir_id, function);
             }
         }
     }
@@ -84,14 +87,30 @@ pub fn modify_derived_item<'tcx>(
 
 fn clone_add_post_condition<'tcx>(
     ctxt: &Context<'tcx>,
+    mut id: rustc_span::def_id::DefId,
+    inputs: &Vec<rustc_middle::ty::Ty>,
     span: Span,
     hir_id: HirId,
     functionx: &mut FunctionX,
 ) -> Result<(), VirErr> {
+    if inputs.len() >= 1 {
+        use rustc_middle::ty::{AdtDef, TyKind};
+        if let TyKind::Ref(_, t, _) = inputs[0].kind() {
+            if let TyKind::Adt(AdtDef(adt_def_data), _) = t.kind() {
+                // It's more convenient to put verifier::allow on the datatype than on the function
+                id = adt_def_data.did;
+            }
+        }
+    }
     let warn = |msg: &str| {
-        ctxt.diagnostics
-            .borrow_mut()
-            .push(VirErrAs::Warning(crate::util::err_span_bare(span, msg.to_string())));
+        crate::attributes::warning_maybe(
+            ctxt.tcx,
+            id,
+            span,
+            &WarningAllow::AutoderiveCloneWithoutSpec,
+            || msg,
+            |msg| ctxt.diagnostics.borrow_mut().push(VirErrAs::Warning(msg)),
+        );
     };
     let warn_unexpected = || {
         warn(
diff --git a/source/rust_verify/src/context.rs b/source/rust_verify/src/context.rs
index 82ead438f2..71a3d081c7 100644
--- a/source/rust_verify/src/context.rs
+++ b/source/rust_verify/src/context.rs
@@ -14,7 +14,7 @@ use std::rc::Rc;
 use std::sync::Arc;
 use std::sync::atomic::AtomicU64;
 use vir::ast::{CrateId, Mode, Path, Pattern, VirErr};
-use vir::messages::AstId;
+use vir::messages::{AstId, WarningAllow};
 
 pub struct ErasureInfo {
     pub(crate) hir_vir_ids: Vec<(HirId, AstId)>,
@@ -46,7 +46,7 @@ pub struct ContextX<'tcx> {
     pub(crate) no_vstd: bool,
     pub(crate) arch_word_bits: Option<vir::ast::ArchWordBits>,
     pub(crate) crate_name: CrateId,
-    pub(crate) name_def_id_map: Rc<RefCell<std::collections::HashMap<Path, DefId>>>,
+    pub(crate) name_def_id_map: Rc<RefCell<HashMap<Path, DefId>>>,
     pub(crate) next_read_kind_id: AtomicU64,
 }
 
@@ -254,4 +254,14 @@ impl<'tcx> BodyCtxt<'tcx> {
     pub(crate) fn set_header_setting(&self, s: HeaderSetting) -> BodyCtxt<'tcx> {
         BodyCtxt { header_setting: s, ..self.clone() }
     }
+
+    pub(crate) fn warning_maybe<S: Into<String>>(
+        &self,
+        span: rustc_span::Span,
+        allow: &WarningAllow,
+        note: impl FnOnce() -> S,
+        emit: impl FnOnce(vir::messages::Message) -> (),
+    ) {
+        crate::attributes::warning_maybe(self.ctxt.tcx, self.fun_id, span, allow, note, emit);
+    }
 }
diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs
index 7bf3138aec..9662c44715 100644
--- a/source/rust_verify/src/external.rs
+++ b/source/rust_verify/src/external.rs
@@ -49,6 +49,7 @@ use rustc_hir::{
 use rustc_span::Span;
 use std::collections::HashMap;
 use vir::ast::{Path, VirErr, VirErrAs};
+use vir::messages::WarningAllow;
 
 /// Main exported type of this module.
 /// Contains all item-things and their categorizations
@@ -652,12 +653,14 @@ fn get_attributes_for_automatic_derive<'tcx>(
     span: Span,
 ) -> Option<ExternalAttrs> {
     let warn_unknown = || {
-        ctxt.diagnostics.borrow_mut().push(VirErrAs::Warning(crate::util::err_span_bare(
+        crate::attributes::warning_maybe(
+            ctxt.tcx,
+            general_item.id().owner_id().to_def_id(),
             span,
-            format!(
-                "Verus doesn't known how to handle this automatically derived item; ignoring it"
-            ),
-        )));
+            &WarningAllow::UnknownAutomaticDerive,
+            || "Verus doesn't know how to handle this automatically derived item; ignoring it",
+            |msg| ctxt.diagnostics.borrow_mut().push(VirErrAs::Warning(msg)),
+        );
     };
 
     if !crate::automatic_derive::is_automatically_derived(attrs) {
diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs
index 499dc2b71a..99b3d6e3ad 100644
--- a/source/rust_verify/src/rust_to_vir.rs
+++ b/source/rust_verify/src/rust_to_vir.rs
@@ -28,15 +28,33 @@ use rustc_hir::{
 
 use std::collections::HashMap;
 use std::sync::Arc;
-use vir::ast::{CrateId, FunX, FunctionKind, Krate, KrateX, Path, VirErr};
+use vir::ast::{CrateId, Fun, FunX, FunctionKind, Krate, KrateX, Path, VirErr};
+use vir::context::{WarningConfig, WarningCtx};
+
+pub(crate) struct State {
+    pub(crate) external_info: ExternalInfo,
+    pub(crate) fun_warn_configs: HashMap<Fun, WarningConfig>,
+}
+
+impl State {
+    pub(crate) fn insert_fun_warn_config<'tcx>(
+        &mut self,
+        ctxt: &Context<'tcx>,
+        name: &Fun,
+        id: rustc_span::def_id::DefId,
+    ) {
+        self.fun_warn_configs
+            .insert(name.clone(), crate::attributes::warning_config_walk_parents(ctxt.tcx, id));
+    }
+}
 
 fn check_item<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     vir: &mut KrateX,
     module_path: &Path,
     id: &ItemId,
     item: &'tcx Item<'tcx>,
-    external_info: &mut ExternalInfo,
     crate_items: &CrateItems,
 ) -> Result<(), Vec<VirErr>> {
     let attrs = ctxt.tcx.hir_attrs(item.hir_id());
@@ -167,6 +185,7 @@ fn check_item<'tcx>(
 
         crate::rust_to_vir_func::check_item_const_or_static(
             ctxt,
+            state,
             &mut vir.functions,
             item.span,
             item.owner_id.to_def_id(),
@@ -189,6 +208,7 @@ fn check_item<'tcx>(
             //     check_fn_opaque_ty(ctxt, &mut vir.opaque_types, &item.owner_id.to_def_id()).map_err(|e| vec![e])?;
             check_item_fn(
                 ctxt,
+                state,
                 &mut vir.functions,
                 Some(&mut vir.reveal_groups),
                 item.owner_id.to_def_id(),
@@ -202,7 +222,6 @@ fn check_item<'tcx>(
                 CheckItemFnEither::BodyId(body_id),
                 None,
                 None,
-                external_info,
                 None,
                 &mut vir.opaque_types,
             )
@@ -279,11 +298,11 @@ fn check_item<'tcx>(
         ItemKind::Impl(impll) => {
             crate::rust_to_vir_impl::translate_impl(
                 ctxt,
+                state,
                 vir,
                 item,
                 impll,
                 module_path.clone(),
-                external_info,
                 crate_items,
                 attrs,
             )?;
@@ -315,6 +334,7 @@ fn check_item<'tcx>(
             let trait_def_id = item.owner_id.to_def_id();
             crate::rust_to_vir_trait::translate_trait(
                 ctxt,
+                state,
                 vir,
                 item.span,
                 trait_def_id,
@@ -323,7 +343,6 @@ fn check_item<'tcx>(
                 trait_generics,
                 trait_items,
                 &vattrs,
-                external_info,
                 crate_items,
                 *safety,
             )
@@ -347,6 +366,7 @@ fn check_item<'tcx>(
 
 fn check_foreign_item<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     vir: &mut KrateX,
     _id: &ForeignItemId,
     item: &'tcx ForeignItem<'tcx>,
@@ -356,6 +376,7 @@ fn check_foreign_item<'tcx>(
             let idents = ident_opts.iter().flatten().collect::<Vec<_>>();
             check_foreign_item_fn(
                 ctxt,
+                state,
                 vir,
                 item.owner_id.to_def_id(),
                 item.span,
@@ -381,7 +402,7 @@ pub fn crate_to_vir<'a, 'tcx>(
     mut ctxtx: ContextX<'tcx>,
     imported: &Vec<Krate>,
     crate_items: &CrateItems,
-) -> Result<(Context<'tcx>, Krate), Vec<VirErr>> {
+) -> Result<(Context<'tcx>, WarningCtx, Krate), Vec<VirErr>> {
     let mut vir: KrateX = KrateX {
         functions: Vec::new(),
         reveal_groups: Vec::new(),
@@ -397,13 +418,11 @@ pub fn crate_to_vir<'a, 'tcx>(
         arch: vir::ast::Arch { word_bits: vir::ast::ArchWordBits::Either32Or64 },
     };
 
-    let mut external_info = ExternalInfo::new();
-
     let tcx = ctxtx.tcx;
 
+    let mut external_info = ExternalInfo::new();
     // Sized is fundamental enough that we always want it even with no-vstd
     external_info.trait_id_set.insert(tcx.lang_items().sized_trait().expect("lang_item"));
-
     // TODO: remove the following when we have full support for auto traits:
     external_info.trait_id_set.insert(tcx.lang_items().unpin_trait().expect("lang_item"));
     external_info.trait_id_set.insert(tcx.lang_items().sync_trait().expect("lang_item"));
@@ -411,6 +430,9 @@ pub fn crate_to_vir<'a, 'tcx>(
         .trait_id_set
         .insert(tcx.get_diagnostic_item(rustc_span::sym::Send).expect("send"));
 
+    let fun_warn_configs = HashMap::new();
+    let mut state = State { external_info, fun_warn_configs };
+
     let mut errors = vec![];
 
     let mut typs_sizes_set: HashMap<TypIgnoreImplPaths, u128> = HashMap::new();
@@ -491,7 +513,7 @@ pub fn crate_to_vir<'a, 'tcx>(
 
     crate::rust_to_vir_trait::make_external_trait_extension_impl_map(
         &ctxt,
-        &mut external_info,
+        &mut state.external_info,
         imported,
         &crate_items,
     )
@@ -510,11 +532,11 @@ pub fn crate_to_vir<'a, 'tcx>(
                         let item = ctxt.tcx.hir_item(item_id);
                         if let Err(errs) = check_item(
                             &ctxt,
+                            &mut state,
                             &mut vir,
                             &module_path,
                             &item_id,
                             item,
-                            &mut external_info,
                             &crate_items,
                         ) {
                             errors.extend(errs);
@@ -522,9 +544,13 @@ pub fn crate_to_vir<'a, 'tcx>(
                     }
                     GeneralItemId::ForeignItemId(foreign_item_id) => {
                         let foreign_item = ctxt.tcx.hir_foreign_item(foreign_item_id);
-                        if let Err(err) =
-                            check_foreign_item(&ctxt, &mut vir, &foreign_item_id, foreign_item)
-                        {
+                        if let Err(err) = check_foreign_item(
+                            &ctxt,
+                            &mut state,
+                            &mut vir,
+                            &foreign_item_id,
+                            foreign_item,
+                        ) {
                             errors.push(err);
                         }
                     }
@@ -586,12 +612,23 @@ pub fn crate_to_vir<'a, 'tcx>(
         &ctxt,
         imported,
         &mut vir,
-        &mut external_info,
+        &mut state.external_info,
     )
     .map_err(|e| vec![e])?;
 
     crate::rust_to_vir_adts::setup_type_invariants(&mut vir).map_err(|e| vec![e])?;
     vir::traits::set_krate_dyn_compatibility(imported, &mut vir);
 
-    Ok((ctxt, Arc::new(vir)))
+    let mut fun_warn_configs: HashMap<Fun, Option<WarningConfig>> = HashMap::new();
+    for krate in imported {
+        for function in &krate.functions {
+            fun_warn_configs.insert(function.x.name.clone(), None);
+        }
+    }
+    for (f, warn) in state.fun_warn_configs {
+        fun_warn_configs.insert(f, Some(warn));
+    }
+    let warning_ctx = WarningCtx { fun_warn_configs };
+
+    Ok((ctxt, warning_ctx, Arc::new(vir)))
 }
diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs
index 451bf0af0f..85b7ab1fea 100644
--- a/source/rust_verify/src/rust_to_vir_base.rs
+++ b/source/rust_verify/src/rust_to_vir_base.rs
@@ -2139,12 +2139,18 @@ fn check_generics_bounds_main<'tcx>(
                 accept_recs.insert(name.to_string(), attr);
 
                 if let Some(diagnostics) = &mut diagnostics {
-                    diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare(
+                    crate::attributes::warning_maybe(
+                        tcx,
+                        def_id,
                         *span,
-                        format!(
-                            "use the attribute style `#[{attr_name:}({name:})]` at the item level"
-                        ),
-                    )));
+                        &vir::messages::WarningAllow::OldStyleAcceptRejectRecursiveTypes,
+                        || {
+                            format!(
+                                "use the attribute style `#[{attr_name:}({name:})]` at the item level",
+                            )
+                        },
+                        |msg| diagnostics.push(VirErrAs::Warning(msg)),
+                    );
                 }
             }
         }
diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs
index d9ff8433a5..629943d8d3 100644
--- a/source/rust_verify/src/rust_to_vir_expr.rs
+++ b/source/rust_verify/src/rust_to_vir_expr.rs
@@ -107,6 +107,7 @@ use vir::ast_util::{
     typ_to_diagnostic_str, types_equal, undecorate_typ,
 };
 use vir::def::{field_ident_from_rust, positional_field_ident};
+use vir::messages::WarningAllow;
 
 /// Enum representing either an `Expr` (value expression) or a `Place` (place expression).
 ///
@@ -3738,18 +3739,28 @@ pub(crate) fn let_stmt_to_vir<'tcx>(
                 == Some(&VerusItem::BuiltinType(verus_items::BuiltinTypeItem::Tracked))
                 && mode == Mode::Proof
             {
-                bctx.ctxt.diagnostics.borrow_mut().push(
-                    vir::ast::VirErrAs::Warning(
-                        crate::util::err_span_bare(pattern.span, format!("the right-hand side is already wrapped with `Tracked`, you likely don't need a `tracked` variable"))
-                        .help("consider `.get()` on the right-hand side, or removing `tracked` on the left-hand side")));
+                bctx.warning_maybe(
+                    pattern.span,
+                    &WarningAllow::NonExecGhostTrackedWrappers,
+                    || "the right-hand side is already wrapped with `Tracked`, you likely don't need a `tracked` variable",
+                    |msg| {
+                        let msg = msg.help("consider `.get()` on the right-hand side, or removing `tracked` on the left-hand side");
+                        bctx.ctxt.diagnostics.borrow_mut().push(vir::ast::VirErrAs::Warning(msg));
+                    }
+                );
             } else if pat_typ_verus_item
                 == Some(&VerusItem::BuiltinType(verus_items::BuiltinTypeItem::Ghost))
                 && mode == Mode::Spec
             {
-                bctx.ctxt.diagnostics.borrow_mut().push(
-                    vir::ast::VirErrAs::Warning(
-                        crate::util::err_span_bare(pattern.span, format!("the right-hand side is already wrapped with `Ghost`, you likely don't need a `ghost` variable"))
-                        .help("consider `@` on the right-hand side, or removing `ghost` on the left-hand side")));
+                bctx.warning_maybe(
+                    pattern.span,
+                    &WarningAllow::NonExecGhostTrackedWrappers,
+                    || "the right-hand side is already wrapped with `Ghost`, you likely don't need a `ghost` variable",
+                    |msg| {
+                        let msg = msg.help("consider `@` on the right-hand side, or removing `ghost` on the left-hand side");
+                        bctx.ctxt.diagnostics.borrow_mut().push(vir::ast::VirErrAs::Warning(msg));
+                    }
+                );
             }
         }
     }
diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs
index baed446856..a7135a553b 100644
--- a/source/rust_verify/src/rust_to_vir_func.rs
+++ b/source/rust_verify/src/rust_to_vir_func.rs
@@ -3,13 +3,13 @@ use crate::automatic_derive::AutomaticDeriveAction;
 use crate::config::Vstd;
 use crate::context::{BodyCtxt, Context, ContextX, HeaderSetting};
 use crate::resolve_traits::{ResolutionResult, ResolvedItem};
+use crate::rust_to_vir::State;
 use crate::rust_to_vir_base::{
     check_fn_opaque_ty, check_generics_bounds_no_polarity, def_id_to_vir_path, local_to_var,
     no_body_param_to_var,
 };
 use crate::rust_to_vir_base::{mk_visibility, qpath_to_ident};
 use crate::rust_to_vir_expr::{ExprModifier, expr_to_vir_consume, pat_to_mut_var};
-use crate::rust_to_vir_impl::ExternalInfo;
 use crate::util::{err_span, err_span_bare};
 use crate::verus_items::{BuiltinTypeItem, VerusItem};
 use crate::{unsupported_err, unsupported_err_unless};
@@ -837,6 +837,7 @@ fn compare_external_sig<'tcx>(
 
 fn handle_external_fn<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     id: DefId,
     kind: FunctionKind,
     visibility: vir::ast::Visibility,
@@ -848,7 +849,6 @@ fn handle_external_fn<'tcx>(
     vattrs: &VerifierAttrs,
     external_trait_from_to: &Option<(vir::ast::Path, vir::ast::Path, Option<vir::ast::Path>)>,
     external_fn_specification_via_external_trait: Option<DefId>,
-    external_info: &mut ExternalInfo,
     // This function is the proxy, and we need to look up the actual path.
 ) -> Result<
     (vir::ast::Path, vir::ast::Visibility, FunctionKind, bool, Safety, bool, DefId, bool),
@@ -1065,7 +1065,10 @@ fn handle_external_fn<'tcx>(
     let has_self_parameter = has_self_parameter(ctxt, external_id);
 
     if matches!(kind, FunctionKind::ForeignTraitMethodImpl { .. }) {
-        external_info.external_fn_specification_trait_method_impls.push((external_id, sig.span));
+        state
+            .external_info
+            .external_fn_specification_trait_method_impls
+            .push((external_id, sig.span));
     }
 
     let safety = ctxt.tcx.fn_sig(external_id).skip_binder().safety();
@@ -1454,6 +1457,7 @@ impl Drop for NewMutRefFixGlobal {
 
 pub(crate) fn check_item_fn<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     functions: &mut Vec<vir::ast::Function>,
     reveal_groups: Option<&mut Vec<vir::ast::RevealGroup>>,
     id: DefId,
@@ -1469,7 +1473,6 @@ pub(crate) fn check_item_fn<'tcx>(
     // (target ExternalTraitSpecificationFor name, target external_trait_extension spec trait name)
     external_trait: Option<(DefId, Option<String>)>,
     external_fn_specification_via_external_trait: Option<DefId>,
-    external_info: &mut ExternalInfo,
     autoderive_action: Option<&AutomaticDeriveAction>,
     opaque_types: &mut OpaqueTypes,
 ) -> Result<Option<Fun>, VirErr> {
@@ -1520,6 +1523,7 @@ pub(crate) fn check_item_fn<'tcx>(
 
         let fun = check_item_const_or_static(
             ctxt,
+            state,
             functions,
             sig.span,
             id,
@@ -1583,6 +1587,7 @@ pub(crate) fn check_item_fn<'tcx>(
             is_async,
         ) = handle_external_fn(
             ctxt,
+            state,
             id,
             kind,
             visibility,
@@ -1593,7 +1598,6 @@ pub(crate) fn check_item_fn<'tcx>(
             &vattrs,
             &external_trait_from_to,
             external_fn_specification_via_external_trait,
-            external_info,
         )?;
 
         let proxy = Some((*ctxt.spanned_new(sig.span, this_path.clone())).clone());
@@ -2207,6 +2211,8 @@ pub(crate) fn check_item_fn<'tcx>(
         if let Some(body_hir_id) = body_hir_id {
             crate::automatic_derive::modify_derived_item(
                 ctxt,
+                id,
+                &inputs,
                 sig.span,
                 body_hir_id,
                 action,
@@ -2228,9 +2234,11 @@ pub(crate) fn check_item_fn<'tcx>(
             autospec.redirect_to.clone();
     }
 
+    state.insert_fun_warn_config(ctxt, &function.x.name, id);
     functions.push(function);
 
     if let Some(f) = &autospec.new_func {
+        state.insert_fun_warn_config(ctxt, &f.x.name, id);
         functions.push(f.clone());
     }
 
@@ -2861,6 +2869,7 @@ fn get_external_def_id<'tcx>(
 
 pub(crate) fn check_item_const_or_static<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     functions: &mut Vec<vir::ast::Function>,
     span: Span,
     id: DefId,
@@ -3029,9 +3038,11 @@ pub(crate) fn check_item_const_or_static<'tcx>(
     }
 
     let function = ctxt.spanned_new(span, functionx);
+    state.insert_fun_warn_config(ctxt, &function.x.name, id);
     functions.push(function);
 
     if let Some(f) = &autospec.new_func {
+        state.insert_fun_warn_config(ctxt, &f.x.name, id);
         functions.push(f.clone());
     }
 
@@ -3040,6 +3051,7 @@ pub(crate) fn check_item_const_or_static<'tcx>(
 
 pub(crate) fn check_foreign_item_fn<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     vir: &mut KrateX,
     id: DefId,
     span: Span,
@@ -3151,6 +3163,7 @@ pub(crate) fn check_foreign_item_fn<'tcx>(
         async_ret: None,
     };
     let function = ctxt.spanned_new(span, func);
+    state.insert_fun_warn_config(ctxt, &function.x.name, id);
     vir.functions.push(function);
     Ok(())
 }
diff --git a/source/rust_verify/src/rust_to_vir_impl.rs b/source/rust_verify/src/rust_to_vir_impl.rs
index 9df3c787b0..2b9269dd03 100644
--- a/source/rust_verify/src/rust_to_vir_impl.rs
+++ b/source/rust_verify/src/rust_to_vir_impl.rs
@@ -1,6 +1,7 @@
 use crate::automatic_derive::is_automatically_derived;
 use crate::context::Context;
 use crate::external::CrateItems;
+use crate::rust_to_vir::State;
 use crate::rust_to_vir_base::{
     def_id_to_vir_path_option, mid_ty_const_to_vir, mk_visibility, typ_path_and_ident_to_vir_path,
 };
@@ -236,11 +237,11 @@ fn translate_assoc_type<'tcx>(
 
 pub(crate) fn translate_impl<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     vir: &mut KrateX,
     item: &'tcx Item<'tcx>,
     impll: &rustc_hir::Impl<'tcx>,
     module_path: Path,
-    external_info: &mut ExternalInfo,
     crate_items: &CrateItems,
     attrs: &[rustc_hir::Attribute],
 ) -> Result<(), Vec<VirErr>> {
@@ -353,7 +354,7 @@ pub(crate) fn translate_impl<'tcx>(
     let trait_path_typ_args =
         if let Some(TraitImplHeader { trait_ref: TraitRef { path, .. }, .. }) = &impll.of_trait {
             let impl_def_id = item.owner_id.to_def_id();
-            external_info.internal_trait_impls.insert(impl_def_id);
+            state.external_info.internal_trait_impls.insert(impl_def_id);
             let path_span = path.span.to(impll.self_ty.span);
             match trait_impl_to_vir(
                 ctxt,
@@ -361,7 +362,7 @@ pub(crate) fn translate_impl<'tcx>(
                 path_span,
                 impl_def_id,
                 Some(impll.generics),
-                external_info,
+                &mut state.external_info,
                 module_path.clone(),
                 false,
                 vattrs.external_trait_blanket,
@@ -396,11 +397,11 @@ pub(crate) fn translate_impl<'tcx>(
         }
         let r = translate_impl_item(
             ctxt,
+            state,
             vir,
             item,
             impll,
             &module_path,
-            external_info,
             crate_items,
             impl_item_id,
             &trait_path_typ_args,
@@ -417,11 +418,11 @@ pub(crate) fn translate_impl<'tcx>(
 
 pub(crate) fn translate_impl_item<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     vir: &mut KrateX,
     item: &'tcx Item<'tcx>,
     impll: &rustc_hir::Impl<'tcx>,
     module_path: &Path,
-    external_info: &mut ExternalInfo,
     crate_items: &CrateItems,
     impl_item_id: &rustc_hir::ImplItemId,
     trait_path_typ_args: &Option<(Path, Typs)>,
@@ -470,6 +471,7 @@ pub(crate) fn translate_impl_item<'tcx>(
 
                     check_item_fn(
                         ctxt,
+                        state,
                         &mut vir.functions,
                         Some(&mut vir.reveal_groups),
                         impl_item.owner_id.to_def_id(),
@@ -483,7 +485,6 @@ pub(crate) fn translate_impl_item<'tcx>(
                         CheckItemFnEither::BodyId(&body_id),
                         None,
                         None,
-                        external_info,
                         autoderive_action.as_ref(),
                         &mut vir.opaque_types,
                     )?;
@@ -531,6 +532,7 @@ pub(crate) fn translate_impl_item<'tcx>(
                 if trait_path_typ_args.is_none() {
                     crate::rust_to_vir_func::check_item_const_or_static(
                         ctxt,
+                        state,
                         &mut vir.functions,
                         impl_item.span,
                         impl_item.owner_id.to_def_id(),
@@ -546,6 +548,7 @@ pub(crate) fn translate_impl_item<'tcx>(
                     let kind = mk_trait_function_kind();
                     crate::rust_to_vir_func::check_item_fn(
                         ctxt,
+                        state,
                         &mut vir.functions,
                         Some(&mut vir.reveal_groups),
                         impl_item.owner_id.to_def_id(),
@@ -559,7 +562,6 @@ pub(crate) fn translate_impl_item<'tcx>(
                         crate::rust_to_vir_func::CheckItemFnEither::BodyId(&body_id),
                         None,
                         None,
-                        external_info,
                         None,
                         &mut vir.opaque_types,
                     )?;
diff --git a/source/rust_verify/src/rust_to_vir_trait.rs b/source/rust_verify/src/rust_to_vir_trait.rs
index eb3adc1f0a..ab00d17eea 100644
--- a/source/rust_verify/src/rust_to_vir_trait.rs
+++ b/source/rust_verify/src/rust_to_vir_trait.rs
@@ -1,6 +1,7 @@
 use crate::attributes::VerifierAttrs;
 use crate::context::Context;
 use crate::external::CrateItems;
+use crate::rust_to_vir::State;
 use crate::rust_to_vir_base::{check_generics_bounds_with_polarity, process_predicate_bounds};
 use crate::rust_to_vir_func::{CheckItemFnEither, check_item_fn};
 use crate::rust_to_vir_impl::ExternalInfo;
@@ -116,6 +117,7 @@ pub(crate) fn external_trait_specification_of<'tcx>(
 
 pub(crate) fn translate_trait<'tcx>(
     ctxt: &Context<'tcx>,
+    state: &mut State,
     vir: &mut KrateX,
     trait_span: Span,
     trait_def_id: DefId,
@@ -124,7 +126,6 @@ pub(crate) fn translate_trait<'tcx>(
     trait_generics: &'tcx Generics,
     trait_items: &'tcx [TraitItemId],
     trait_vattrs: &VerifierAttrs,
-    external_info: &mut ExternalInfo,
     crate_items: &CrateItems,
     safety: Safety,
 ) -> Result<(), VirErr> {
@@ -324,6 +325,7 @@ pub(crate) fn translate_trait<'tcx>(
                 // requires and ensures on exec functions can refer to spec extension trait:
                 let fun = check_item_fn(
                     ctxt,
+                    state,
                     &mut methods,
                     None,
                     owner_id.to_def_id(),
@@ -337,7 +339,6 @@ pub(crate) fn translate_trait<'tcx>(
                     body_id,
                     ex_trait_id_for.map(|d| (d, trait_extension_in_spec)),
                     ex_item_id_for,
-                    external_info,
                     None,
                     &mut vir.opaque_types,
                 )?;
@@ -366,6 +367,7 @@ pub(crate) fn translate_trait<'tcx>(
                 let typ = ctxt.mid_ty_to_vir(owner_id.to_def_id(), *span, &mid_ty, false, None)?;
                 let fun = crate::rust_to_vir_func::check_item_fn(
                     ctxt,
+                    state,
                     &mut methods,
                     None,
                     owner_id.to_def_id(),
@@ -379,7 +381,6 @@ pub(crate) fn translate_trait<'tcx>(
                     body_id,
                     ex_trait_id_for.map(|d| (d, trait_extension_in_spec)),
                     ex_item_id_for,
-                    external_info,
                     None,
                     &mut vir.opaque_types,
                 )?;
@@ -478,7 +479,7 @@ pub(crate) fn translate_trait<'tcx>(
     } else {
         trait_def_id
     };
-    external_info.local_trait_ids.push(target_trait_id);
+    state.external_info.local_trait_ids.push(target_trait_id);
     let external_trait_extension = if let Some((spec, imp)) = external_trait_extension {
         let spec = orig_trait_path.replace_last(Arc::new(spec.clone()));
         let imp = orig_trait_path.replace_last(Arc::new(imp.clone()));
diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs
index c3bdcf0644..73d4623301 100644
--- a/source/rust_verify/src/verifier.rs
+++ b/source/rust_verify/src/verifier.rs
@@ -338,6 +338,7 @@ pub struct Verifier {
     air_no_span: Option<vir::messages::Span>,
     current_crate_modules: Option<Vec<vir::ast::Module>>,
     crate_items: Option<Arc<crate::external::CrateItems>>,
+    warning_ctx: Option<Arc<vir::context::WarningCtx>>,
     buckets: HashMap<BucketId, Bucket>,
 
     // proof debugging purposes
@@ -516,6 +517,7 @@ impl Verifier {
             air_no_span: None,
             current_crate_modules: None,
             crate_items: None,
+            warning_ctx: None,
             buckets: HashMap::new(),
 
             expand_flag: false,
@@ -564,6 +566,7 @@ impl Verifier {
             air_no_span: self.air_no_span.clone(),
             current_crate_modules: self.current_crate_modules.clone(),
             crate_items: self.crate_items.clone(),
+            warning_ctx: self.warning_ctx.clone(),
             buckets: self.buckets.clone(),
 
             expand_flag: self.expand_flag,
@@ -2091,6 +2094,7 @@ impl Verifier {
             self.args.rlimit,
             Arc::new(std::sync::Mutex::new(None)),
             Arc::new(std::sync::Mutex::new(call_graph_log)),
+            self.warning_ctx.clone().expect("warning_ctx"),
             self.args.solver,
             false,
             self.args.check_api_safety,
@@ -2784,7 +2788,7 @@ impl Verifier {
                 .collect()
         };
 
-        let (ctxt, vir_crate) =
+        let (ctxt, mut warning_ctx, vir_crate) =
             crate::rust_to_vir::crate_to_vir(ctxtx, &other_vir_crates, &crate_items)
                 .map_err(map_errs_diagnostics)?;
 
@@ -2871,11 +2875,15 @@ impl Verifier {
         }
         let path_to_well_known_item = crate::def::path_to_well_known_item(&ctxt);
 
-        let vir_crate =
-            vir::traits::demote_external_traits(diagnostics, &path_to_well_known_item, &vir_crate)
-                .map_err(map_err_diagnostics)?;
-        let vir_crate =
-            vir::traits::inherit_default_bodies(&vir_crate).map_err(|e| (vec![e], Vec::new()))?;
+        let vir_crate = vir::traits::demote_external_traits(
+            diagnostics,
+            &warning_ctx,
+            &path_to_well_known_item,
+            &vir_crate,
+        )
+        .map_err(map_err_diagnostics)?;
+        let vir_crate = vir::traits::inherit_default_bodies(&vir_crate, &mut warning_ctx)
+            .map_err(|e| (vec![e], Vec::new()))?;
         let vir_crate = vir::traits::fixup_ens_has_return_for_trait_method_impls(vir_crate)
             .map_err(|e| (vec![e], Vec::new()))?;
 
@@ -2888,6 +2896,7 @@ impl Verifier {
             &vir_crate,
             &unpruned_crate,
             &mut *ctxt.diagnostics.borrow_mut(),
+            &warning_ctx,
             self.args.no_verify,
             self.args.no_cheating,
         );
@@ -2960,6 +2969,7 @@ impl Verifier {
                 .map_err(|e| (vec![e], Vec::new()))?;
 
         self.vir_crate = Some(vir_crate.clone());
+        self.warning_ctx = Some(Arc::new(warning_ctx));
 
         let erasure_info = ctxt.erasure_info.borrow();
         let hir_vir_ids = erasure_info.hir_vir_ids.clone();
diff --git a/source/rust_verify_test/tests/assert_forall_by.rs b/source/rust_verify_test/tests/assert_forall_by.rs
index d6ac55df00..e4a958edf7 100644
--- a/source/rust_verify_test/tests/assert_forall_by.rs
+++ b/source/rust_verify_test/tests/assert_forall_by.rs
@@ -291,3 +291,18 @@ test_verify_one_file! {
         assert!(warns.next().is_none());
     }
 }
+
+test_verify_one_file! {
+    #[test] test_forallstmt_implies_no_warning verus_code! {
+        uninterp spec fn f(x: int) -> bool;
+        uninterp spec fn g(x: int) -> bool;
+
+        #[verifier::allow(assert_forall_implication)]
+        proof fn x()
+            requires forall |x: int| f(x) ==> g(x)
+        {
+            assert forall |x: int| f(x) ==> g(x) by {
+            }
+        }
+    } => Ok(())
+}
diff --git a/source/rust_verify_test/tests/exec_termination.rs b/source/rust_verify_test/tests/exec_termination.rs
index 3c6bc8d35a..4d3cc41f73 100644
--- a/source/rust_verify_test/tests/exec_termination.rs
+++ b/source/rust_verify_test/tests/exec_termination.rs
@@ -33,6 +33,22 @@ test_verify_one_file_with_options! {
     } => Ok(err) => assert!(err.warnings.iter().find(|x| x.message.contains("if exec_allows_no_decreases_clause is set, decreases checks in exec functions do not guarantee termination of functions with loops")).is_some())
 }
 
+test_verify_one_file_with_options! {
+    #[test] recursive_exec_function_with_decreases_clause_exec_allows_no_decreases_clause_no_warning ["exec_allows_no_decreases_clause"] => verus_code! {
+        #[verifier::allow(decreases_when_exec_allows_no_decreases_clause)]
+        fn a(i: u64) -> (r: u64)
+            ensures r == i
+            decreases i
+        {
+            if i == 0 {
+                return 0;
+            } else {
+                return 1 + a(i - 1);
+            }
+        }
+    } => Ok(())
+}
+
 test_verify_one_file_with_options! {
     #[test] recursive_exec_function_with_decreases_clause_exec_allows_no_decreases_clause_fails ["exec_allows_no_decreases_clause"] => verus_code! {
         fn a(i: u64) -> (r: u64)
diff --git a/source/vir/src/ast_simplify.rs b/source/vir/src/ast_simplify.rs
index 15d3e9b106..ff2022062d 100644
--- a/source/vir/src/ast_simplify.rs
+++ b/source/vir/src/ast_simplify.rs
@@ -1703,6 +1703,7 @@ pub fn simplify_krate(ctx: &mut GlobalCtx, krate: &Krate) -> Result<Krate, VirEr
         ctx.rlimit,
         ctx.interpreter_log.clone(),
         ctx.func_call_graph_log.clone(),
+        ctx.warning_ctx.clone(),
         ctx.solver.clone(),
         true,
         ctx.check_api_safety,
diff --git a/source/vir/src/ast_to_sst.rs b/source/vir/src/ast_to_sst.rs
index 35fcd2f242..d3db5ed603 100644
--- a/source/vir/src/ast_to_sst.rs
+++ b/source/vir/src/ast_to_sst.rs
@@ -13,7 +13,7 @@ use crate::def::{Spanned, unique_local};
 use crate::fun;
 use crate::inv_masks::MaskSet;
 use crate::messages::{
-    Span, ToAny, error, error_with_label, error_with_secondary_label, internal_error, warning,
+    Span, ToAny, WarningAllow, error, error_with_label, error_with_secondary_label, internal_error,
 };
 use crate::sst::{
     Bnd, BndX, CallFun, Dest, Exp, ExpX, Exps, InternalFun, LocalDecl, LocalDeclKind, LocalDeclX,
@@ -2077,8 +2077,12 @@ pub(crate) fn expr_to_stm_opt(
             let skip = !ctx.reveal_group_set.contains(x) && !ctx.func_map.contains_key(x);
 
             if skip {
-                state.diagnostics.report(&warning(
-                    &expr.span, "this reveal/fuel statement has no effect because no verification condition in this module depends on this function").to_any());
+                ctx.warning_maybe_if_in_local_crate(
+                    &expr.span,
+                    &WarningAllow::DeadReveal,
+                    || "this reveal/fuel statement has no effect because no verification condition in this module depends on this function",
+                    |msg| state.diagnostics.report(&msg.to_any()),
+                );
             }
 
             let stms = if skip {
diff --git a/source/vir/src/context.rs b/source/vir/src/context.rs
index 982d17d469..81adea8b28 100644
--- a/source/vir/src/context.rs
+++ b/source/vir/src/context.rs
@@ -6,7 +6,7 @@ use crate::ast::{
 use crate::ast_util::{dt_as_friendly_rust_name_raw, path_as_friendly_rust_name_raw};
 use crate::datatype_to_air::is_datatype_transparent;
 use crate::def::{FUEL_ID, NameCtxt};
-use crate::messages::{Span, error};
+use crate::messages::{Span, WarningAllow, error};
 use crate::poly::MonoTyp;
 use crate::recursion::Node;
 use crate::scc::Graph;
@@ -35,6 +35,23 @@ pub struct ChosenTriggers {
     pub manual: bool,
 }
 
+#[derive(Debug, Clone)]
+pub struct WarningConfig(pub Vec<WarningAllow>);
+
+impl crate::messages::CheckAllowForWarning for WarningConfig {
+    fn allowed(&self, allow: &WarningAllow) -> bool {
+        self.0.iter().any(|a| a == allow)
+    }
+}
+
+#[derive(Debug)]
+pub struct WarningCtx {
+    // Map names of FunctionX in this crate (not imported from other crates)
+    // to Some CheckAllowForWarning to be used to check that fun,
+    // map names from other crates to None
+    pub fun_warn_configs: HashMap<Fun, Option<WarningConfig>>,
+}
+
 /// Context for across all modules
 pub struct GlobalCtx {
     pub(crate) chosen_triggers: std::cell::RefCell<Vec<ChosenTriggers>>, // diagnostics
@@ -50,6 +67,7 @@ pub struct GlobalCtx {
     pub trait_impl_to_extensions: HashMap<Path, Vec<Path>>,
     /// Map TSpec to T
     pub(crate) extension_to_trait: HashMap<Path, Path>,
+    pub(crate) warning_ctx: Arc<WarningCtx>,
     /// Connects quantifier identifiers to the original expression
     pub qid_map: RefCell<HashMap<String, BndInfo>>,
     pub(crate) rlimit: f32,
@@ -150,6 +168,23 @@ impl Ctx {
             _ => false,
         }
     }
+
+    pub(crate) fn warning_maybe_if_in_local_crate<S: Into<String>>(
+        &self,
+        span: &Span,
+        allow: &WarningAllow,
+        note: impl FnOnce() -> S,
+        emit: impl FnOnce(crate::messages::Message) -> (),
+    ) {
+        if let Some(function_ctx) = &self.fun {
+            let check_allow = &self.global.warning_ctx.fun_warn_configs[&function_ctx.current_fun];
+            crate::messages::warning_maybe_if_in_local_crate(check_allow, span, allow, note, emit);
+        } else {
+            // TODO: if we ever support verifier::allow on expressions,
+            // we can make this warning configurable:
+            emit(crate::messages::warning(span, note()));
+        }
+    }
 }
 
 fn datatypes_inv_visit(
@@ -281,6 +316,7 @@ impl GlobalCtx {
         rlimit: f32,
         interpreter_log: Arc<std::sync::Mutex<Option<File>>>,
         func_call_graph_log: Arc<std::sync::Mutex<Option<FuncCallGraphLogFiles>>>,
+        warning_ctx: Arc<WarningCtx>,
         solver: SmtSolver,
         after_simplify: bool,
         check_api_safety: bool,
@@ -690,6 +726,7 @@ impl GlobalCtx {
             datatype_graph_span_infos: span_infos,
             extension_to_trait,
             trait_impl_to_extensions,
+            warning_ctx,
             qid_map,
             rlimit,
             interpreter_log,
@@ -722,6 +759,7 @@ impl GlobalCtx {
             func_call_sccs: self.func_call_sccs.clone(),
             extension_to_trait: self.extension_to_trait.clone(),
             trait_impl_to_extensions: self.trait_impl_to_extensions.clone(),
+            warning_ctx: self.warning_ctx.clone(),
             qid_map,
             rlimit: self.rlimit,
             interpreter_log,
diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs
index 9c984f27d3..79af655a88 100644
--- a/source/vir/src/interpreter.rs
+++ b/source/vir/src/interpreter.rs
@@ -14,7 +14,7 @@ use crate::ast::{
 use crate::ast_to_sst_func::SstMap;
 use crate::ast_util::{path_as_vstd_name, undecorate_typ};
 use crate::context::GlobalCtx;
-use crate::messages::{Message, Span, ToAny, error, warning};
+use crate::messages::{Message, Span, ToAny, WarningAllow, error};
 use crate::sst::{Bnd, BndX, CallFun, Exp, ExpX, Exps, FunctionSst, Trigs, UniqueIdent};
 use crate::sst_util::subst_exp;
 use crate::unicode::valid_unicode_scalar_bigint;
@@ -201,9 +201,27 @@ struct Ctx<'a> {
     max_depth: usize,
     arch: ArchWordBits,
     global: &'a GlobalCtx,
+    current_fun: Option<Fun>,
     report_long_running: bool,
 }
 
+impl<'a> Ctx<'a> {
+    pub(crate) fn warning<S: Into<String>>(
+        &self,
+        span: &Span,
+        allow: &WarningAllow,
+        note: impl FnOnce() -> S,
+        emit: impl FnOnce(crate::messages::Message) -> (),
+    ) {
+        if let Some(current_fun) = &self.current_fun {
+            let check_allow = &self.global.warning_ctx.fun_warn_configs[current_fun];
+            crate::messages::warning_maybe_if_in_local_crate(check_allow, span, allow, note, emit);
+        } else {
+            emit(crate::messages::warning(span, note()));
+        }
+    }
+}
+
 /// Interpreter-internal expressions
 #[derive(Debug, Clone, ToDebugSNode)]
 pub enum InterpExp {
@@ -990,17 +1008,24 @@ fn eval_seq(
                     Interp(Seq(s)) => match &args[1].x {
                         Const(Constant::Int(index)) => match BigInt::to_usize(index) {
                             None => {
-                                let msg = "Computation tried to index into a sequence using a value that does not fit into usize";
-                                state.msgs.push(warning(&exp.span, msg));
+                                ctx.warning(
+                                    &exp.span,
+                                    &WarningAllow::AssertComputeUnsimplified,
+                                    || "Computation tried to index into a sequence using a value that does not fit into usize",
+                                    |msg| state.msgs.push(msg),
+                                );
                                 ok_seq(&args[0], &s, &args[1..])
                             }
                             Some(index) => {
                                 if index < s.len() {
                                     Ok(s[index].clone())
                                 } else {
-                                    let msg =
-                                        "Computation tried to index past the length of a sequence";
-                                    state.msgs.push(warning(&exp.span, msg));
+                                    ctx.warning(
+                                        &exp.span,
+                                        &WarningAllow::AssertComputeUnsimplified,
+                                        || "Computation tried to index past the length of a sequence",
+                                        |msg| state.msgs.push(msg),
+                                    );
                                     ok_seq(&args[0], &s, &args[1..])
                                 }
                             }
@@ -1046,6 +1071,7 @@ fn eval_seq(
 
 /// Custom interpretation for array_index
 fn eval_array_index(
+    ctx: &Ctx,
     state: &mut State,
     exp: &Exp,
     arr: &Exp,
@@ -1065,16 +1091,24 @@ fn eval_array_index(
         Interp(Array(s)) => match &index_exp.x {
             Const(Constant::Int(i)) => match BigInt::to_usize(i) {
                 None => {
-                    let msg = "Computation tried to index into an array using a value that does not fit into usize";
-                    state.msgs.push(warning(&exp.span, msg));
+                    ctx.warning(
+                        &exp.span,
+                        &WarningAllow::AssertComputeUnsimplified,
+                        || "Computation tried to index into an array using a value that does not fit into usize",
+                        |msg| state.msgs.push(msg),
+                    );
                     ok
                 }
                 Some(index) => {
                     if index < s.len() {
                         Ok(s[index].clone())
                     } else {
-                        let msg = "Computation tried to index past the length of an array";
-                        state.msgs.push(warning(&exp.span, msg));
+                        ctx.warning(
+                            &exp.span,
+                            &WarningAllow::AssertComputeUnsimplified,
+                            || "Computation tried to index past the length of an array",
+                            |msg| state.msgs.push(msg),
+                        );
                         ok
                     }
                 }
@@ -1208,9 +1242,12 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                                 |lower: BigInt, upper: BigInt| !(i < &lower || i > &upper);
                             let mut apply_range = |lower: BigInt, upper: BigInt| {
                                 if !in_range(lower, upper) {
-                                    let msg =
-                                        "Computation clipped an integer that was out of range";
-                                    state.msgs.push(warning(&exp.span, msg));
+                                    ctx.warning(
+                                        &exp.span,
+                                        &WarningAllow::AssertComputeUnsimplified,
+                                        || "Computation clipped an integer that was out of range",
+                                        |msg| state.msgs.push(msg),
+                                    );
                                     ok.clone()
                                 } else {
                                     // Use the type of clip, not the inner expression,
@@ -1220,9 +1257,12 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                             };
                             let apply_unicode_scalar_range = |state: &mut State| {
                                 if !valid_unicode_scalar_bigint(i) {
-                                    let msg =
-                                        "Computation clipped an integer that was out of range";
-                                    state.msgs.push(warning(&exp.span, msg));
+                                    ctx.warning(
+                                        &exp.span,
+                                        &WarningAllow::AssertComputeUnsimplified,
+                                        || "Computation clipped an integer that was out of range",
+                                        |msg| state.msgs.push(msg),
+                                    );
                                     ok.clone()
                                 } else {
                                     // Use the type of clip, not the inner expression,
@@ -1255,7 +1295,12 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                                                 apply_range(lower, upper(32))
                                             } else {
                                                 // may or may not be in range of 64, we must conservatively give up.
-                                                state.msgs.push(warning(&exp.span, "Computation clipped an arch-dependent integer that was out of range"));
+                                                ctx.warning(
+                                                    &exp.span,
+                                                    &WarningAllow::AssertComputeUnsimplified,
+                                                    || "Computation clipped an arch-dependent integer that was out of range",
+                                                    |msg| state.msgs.push(msg),
+                                                );
                                                 ok.clone()
                                             }
                                         }
@@ -1272,7 +1317,12 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                                                 apply_range(lower(32), upper(32))
                                             } else {
                                                 // may or may not be in range of 64, we must conservatively give up.
-                                                state.msgs.push(warning(&exp.span, "Computation clipped an arch-dependent integer that was out of range"));
+                                                ctx.warning(
+                                                    &exp.span,
+                                                    &WarningAllow::AssertComputeUnsimplified,
+                                                    || "Computation clipped an arch-dependent integer that was out of range",
+                                                    |msg| state.msgs.push(msg),
+                                                );
                                                 ok.clone()
                                             }
                                         }
@@ -1618,7 +1668,7 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                 }
                 Index(ArrayKind::Array, _) => {
                     let e2 = eval_expr_internal(ctx, state, e2)?;
-                    eval_array_index(state, exp, &e1, &e2)
+                    eval_array_index(ctx, state, exp, &e1, &e2)
                 }
                 Index(ArrayKind::Slice, _)
                 | HeightCompare { .. }
@@ -1959,6 +2009,7 @@ fn eval_expr_top(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Simplificati
 /// We run the interpreter on a separate thread, so that we can give it a larger-than-default stack
 fn eval_expr_launch(
     global: &GlobalCtx,
+    current_fun: Option<Fun>,
     exp: Exp,
     fun_ssts: &HashMap<Fun, FunctionSst>,
     rlimit: f32,
@@ -2003,6 +2054,7 @@ fn eval_expr_launch(
         max_depth,
         arch,
         global,
+        current_fun,
         report_long_running: global.report_long_running,
     };
     let result = eval_expr_top(&ctx, &mut state, &exp)?;
@@ -2041,11 +2093,17 @@ fn eval_expr_launch(
                 let res = cleanup_exp(&res)?;
                 // Send partial result to Z3
                 if exp.definitely_eq(&res) {
-                    let msg = format!(
-                        "Failed to simplify expression <<{}>> before sending to Z3",
-                        exp.x.to_user_string(&ctx.global)
+                    ctx.warning(
+                        &exp.span,
+                        &WarningAllow::AssertComputeUnsimplified,
+                        || {
+                            format!(
+                                "Failed to simplify expression <<{}>> before sending to Z3",
+                                exp.x.to_user_string(&ctx.global),
+                            )
+                        },
+                        |msg| state.msgs.push(msg),
                     );
-                    state.msgs.push(warning(&exp.span, msg));
                 }
                 Ok((res, state.msgs))
             }
@@ -2067,7 +2125,7 @@ fn eval_expr_launch(
 
 /// Symbolically evaluate an expression, simplifying it as much as possible
 pub fn eval_expr<D>(
-    global: &GlobalCtx,
+    ctx: &crate::context::Ctx,
     exp: &Exp,
     diagnostics: Option<&D>,
     fun_ssts: SstMap,
@@ -2080,7 +2138,8 @@ where
     D: air::messages::Diagnostics + ?Sized,
 {
     // Make a new global so we can move it into the new thread
-    let global = global.from_self_with_log(global.interpreter_log.clone());
+    let global = ctx.global.from_self_with_log(ctx.global.interpreter_log.clone());
+    let current_fun = ctx.fun.as_ref().map(|f| f.current_fun.clone());
 
     let builder =
         thread::Builder::new().name("interpreter".to_string()).stack_size(1024 * 1024 * 1024); // 1 GB
@@ -2094,6 +2153,7 @@ where
                 .spawn(move || {
                     let res = eval_expr_launch(
                         &global,
+                        current_fun,
                         exp,
                         &*fun_ssts,
                         rlimit,
diff --git a/source/vir/src/messages.rs b/source/vir/src/messages.rs
index e85de23c30..5bb3290bce 100644
--- a/source/vir/src/messages.rs
+++ b/source/vir/src/messages.rs
@@ -32,6 +32,68 @@ impl std::fmt::Debug for Span {
     }
 }
 
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum WarningAllow {
+    UndeclaredExternalTrait,
+    AssertForallImplication,
+    DecreasesWhenExecAllowsNoDecreasesClause,
+    BroadcastWithoutTrigger,
+    TriggerOnSpecFn,
+    DeadReveal,
+    AssertComputeUnsimplified,
+    OldStyleAcceptRejectRecursiveTypes,
+    UnknownAutomaticDerive,
+    AutoderiveCloneWithoutSpec,
+    NonExecGhostTrackedWrappers,
+}
+
+impl WarningAllow {
+    pub fn to_str(&self) -> &'static str {
+        match self {
+            WarningAllow::UndeclaredExternalTrait => "undeclared_external_trait",
+            WarningAllow::AssertForallImplication => "assert_forall_implication",
+            WarningAllow::DecreasesWhenExecAllowsNoDecreasesClause => {
+                "decreases_when_exec_allows_no_decreases_clause"
+            }
+            WarningAllow::BroadcastWithoutTrigger => "broadcast_without_trigger",
+            WarningAllow::TriggerOnSpecFn => "trigger_on_spec_fn",
+            WarningAllow::DeadReveal => "dead_reveal",
+            WarningAllow::AssertComputeUnsimplified => "assert_compute_unsimplified",
+            WarningAllow::OldStyleAcceptRejectRecursiveTypes => {
+                "old_style_accept_reject_recursive_types"
+            }
+            WarningAllow::UnknownAutomaticDerive => "unknown_automatic_derive",
+            WarningAllow::AutoderiveCloneWithoutSpec => "autoderive_clone_without_spec",
+            WarningAllow::NonExecGhostTrackedWrappers => "non_exec_ghost_tracked_wrappers",
+        }
+    }
+
+    pub fn from_str(s: &str) -> Option<WarningAllow> {
+        match s {
+            "undeclared_external_trait" => Some(WarningAllow::UndeclaredExternalTrait),
+            "assert_forall_implication" => Some(WarningAllow::AssertForallImplication),
+            "decreases_when_exec_allows_no_decreases_clause" => {
+                Some(WarningAllow::DecreasesWhenExecAllowsNoDecreasesClause)
+            }
+            "broadcast_without_trigger" => Some(WarningAllow::BroadcastWithoutTrigger),
+            "trigger_on_spec_fn" => Some(WarningAllow::TriggerOnSpecFn),
+            "dead_reveal" => Some(WarningAllow::DeadReveal),
+            "assert_compute_unsimplified" => Some(WarningAllow::AssertComputeUnsimplified),
+            "old_style_accept_reject_recursive_types" => {
+                Some(WarningAllow::OldStyleAcceptRejectRecursiveTypes)
+            }
+            "unknown_automatic_derive" => Some(WarningAllow::UnknownAutomaticDerive),
+            "autoderive_clone_without_spec" => Some(WarningAllow::AutoderiveCloneWithoutSpec),
+            "non_exec_ghost_tracked_wrappers" => Some(WarningAllow::NonExecGhostTrackedWrappers),
+            _ => None,
+        }
+    }
+}
+
+pub trait CheckAllowForWarning {
+    fn allowed(&self, allow: &WarningAllow) -> bool;
+}
+
 #[derive(Debug, Serialize, Deserialize, Clone, ToDebugSNode)]
 pub struct MessageLabel {
     pub span: Span,
@@ -309,6 +371,43 @@ pub fn warning<S: Into<String>>(span: &Span, note: S) -> Message {
     message(MessageLevel::Warning, note, span)
 }
 
+/// Basic warning, possibly suppressed by verifier::allow
+pub fn warning_maybe<S: Into<String>>(
+    check_allow: &(impl CheckAllowForWarning + ?Sized),
+    span: &Span,
+    allow: &WarningAllow,
+    note: impl FnOnce() -> S,
+    emit: impl FnOnce(Message) -> (),
+) {
+    if !check_allow.allowed(allow) {
+        let s = allow.to_str();
+        let msg = warning(span, note());
+        let msg = msg.help(
+            format!(
+                "to suppress this warning, use `#[verifier::allow({s})]` on the surrounding function, datatype, or module or `#![verifier::allow({s})]` in the module or crate"
+            ));
+        emit(msg);
+    }
+}
+
+/// Basic warning, possibly suppressed by verifier::allow,
+/// and possibly also suppressed by check_allow = None (which means a check for another crate's item)
+/// REVIEW: at some point, we should probably just stop checking imported items
+pub fn warning_maybe_if_in_local_crate<S: Into<String>>(
+    check_allow: &Option<crate::context::WarningConfig>,
+    span: &Span,
+    allow: &WarningAllow,
+    note: impl FnOnce() -> S,
+    emit: impl FnOnce(Message) -> (),
+) {
+    if let Some(check_allow) = check_allow {
+        // The item being checked is local to our crate, so continue with warning:
+        warning_maybe(check_allow, span, allow, note, emit);
+    }
+    // Otherwise, don't warn (it's an item from another crate,
+    // and the warning was already displayed when that crate was checked)
+}
+
 /// Bare error without any spans; use the builders below to add spans and labels
 pub fn error_bare<S: Into<String>>(note: S) -> Message {
     message_bare(MessageLevel::Error, note)
diff --git a/source/vir/src/sst_elaborate.rs b/source/vir/src/sst_elaborate.rs
index 0ee09ad8db..5159ae823e 100644
--- a/source/vir/src/sst_elaborate.rs
+++ b/source/vir/src/sst_elaborate.rs
@@ -4,7 +4,7 @@ use crate::ast::{
 use crate::ast_to_sst_func::SstMap;
 use crate::context::Ctx;
 use crate::def::{Spanned, unique_local};
-use crate::messages::{ToAny, error_with_label, warning};
+use crate::messages::{ToAny, WarningAllow, error_with_label};
 use crate::sst::{BndX, CallFun, Exp, ExpX, FuncCheckSst, FunctionSst, Stm, StmX, UniqueIdent};
 use crate::sst_visitor::{NoScoper, Rewrite, Visitor};
 use crate::triggers::build_triggers;
@@ -100,7 +100,12 @@ fn elaborate_one_exp<D: Diagnostics + ?Sized>(
                         If you think you need additional triggers, see the discussion in \
                         https://github.com/verus-lang/verus/pull/331 \
                         for alternatives.";
-                    diagnostics.report(&warning(&exp.span, msg).to_any());
+                    ctx.warning_maybe_if_in_local_crate(
+                        &exp.span,
+                        &WarningAllow::TriggerOnSpecFn,
+                        || msg,
+                        |msg| diagnostics.report(&msg.to_any()),
+                    );
                 }
                 let bnd = Spanned::new(bnd.span.clone(), BndX::Lambda(bs.clone(), trigs));
                 Ok(SpannedTyped::new(&exp.span, &exp.typ, ExpX::Bind(bnd, body.clone())))
@@ -122,7 +127,7 @@ fn elaborate_one_stm<D: Diagnostics + ?Sized>(
     match &stm.x {
         StmX::AssertCompute(id, exp, compute) => {
             let interp_exp = crate::interpreter::eval_expr(
-                &ctx.global,
+                ctx,
                 exp,
                 Some(diagnostics),
                 fun_ssts.clone(),
@@ -147,7 +152,7 @@ fn elaborate_one_stm<D: Diagnostics + ?Sized>(
             }
             let reqs = vec_map_result(requires, |e| {
                 crate::interpreter::eval_expr(
-                    &ctx.global,
+                    ctx,
                     e,
                     None::<&air::messages::Reporter>, // Don't print (internal) diagnostics
                     fun_ssts.clone(),
@@ -159,7 +164,7 @@ fn elaborate_one_stm<D: Diagnostics + ?Sized>(
             })?;
             let ens = vec_map_result(ensures, |e| {
                 crate::interpreter::eval_expr(
-                    &ctx.global,
+                    ctx,
                     e,
                     None::<&air::messages::Reporter>, // Don't print (internal) diagnostics
                     fun_ssts.clone(),
@@ -305,7 +310,7 @@ pub(crate) fn elaborate_function_rewrite_recursive<'a, 'b, D: Diagnostics>(
 fn expand<'a>(ctx: &'a Ctx, fun_ssts: &SstMap, exps: Vec<Exp>) -> Result<Vec<Exp>, VirErr> {
     vec_map_result(&exps, |e| {
         crate::interpreter::eval_expr(
-            &ctx.global,
+            ctx,
             e,
             None::<&air::messages::Reporter>,
             fun_ssts.clone(),
diff --git a/source/vir/src/traits.rs b/source/vir/src/traits.rs
index 68f8cfbf22..2de4b73821 100644
--- a/source/vir/src/traits.rs
+++ b/source/vir/src/traits.rs
@@ -8,7 +8,7 @@ use crate::ast_util::path_as_friendly_rust_name;
 use crate::ast_visitor::VisitorScopeMap;
 use crate::context::Ctx;
 use crate::def::Spanned;
-use crate::messages::{Span, ToAny, error, warning};
+use crate::messages::{Span, ToAny, error};
 use crate::sst_to_air::typ_to_ids;
 use air::ast::{Command, CommandX, Commands, DeclX};
 use air::ast_util::{ident_apply, ident_var, mk_bind_expr, mk_implies, mk_unnamed_axiom, str_typ};
@@ -138,6 +138,7 @@ fn demote_one_expr(
 // We consider methods for external traits to be static.
 pub fn demote_external_traits(
     diagnostics: &impl air::messages::Diagnostics,
+    warning_ctx: &crate::context::WarningCtx,
     path_to_well_known_item: &HashMap<Path, WellKnownItem>,
     krate: &Krate,
 ) -> Result<Krate, VirErr> {
@@ -169,17 +170,22 @@ pub fn demote_external_traits(
             };
             let our_trait = traits.contains(trait_path);
             if !our_trait {
-                diagnostics.report(
-                    &warning(
-                        &function.span,
+                let Some(warn_config) = warning_ctx.fun_warn_configs.get(&function.x.name) else {
+                    panic!("missing warn_config for function {:?}", &function.x.name);
+                };
+                crate::messages::warning_maybe_if_in_local_crate(
+                    warn_config,
+                    &function.span,
+                    &crate::messages::WarningAllow::UndeclaredExternalTrait,
+                    || {
                         format!(
                             "cannot use external trait {} as a bound without declaring the trait \
                             (use #[verifier::external_trait_specification] to declare the trait); \
                             this is a warning for now but will eventually be an error",
                             path_as_friendly_rust_name(trait_path)
-                        ),
-                    )
-                    .to_any(),
+                        )
+                    },
+                    |msg| diagnostics.report(&msg.to_any()),
                 );
             }
         }
@@ -492,7 +498,10 @@ copy by fn_call_to_vir in the rust_verify crate.  For example:
     f = vir::def::trait_inherit_default_name(&f, &impl_path)
   }
 */
-pub fn inherit_default_bodies(krate: &Krate) -> Result<Krate, VirErr> {
+pub fn inherit_default_bodies(
+    krate: &Krate,
+    warning_ctx: &mut crate::context::WarningCtx,
+) -> Result<Krate, VirErr> {
     let mut kratex = (**krate).clone();
 
     let mut trait_map: HashMap<Path, &Trait> = HashMap::new();
@@ -637,6 +646,8 @@ pub fn inherit_default_bodies(krate: &Krate) -> Result<Krate, VirErr> {
                     extra_dependencies: vec![],
                     async_ret: None,
                 };
+                let warn_config = warning_ctx.fun_warn_configs[&default_function.x.name].clone();
+                warning_ctx.fun_warn_configs.insert(inherit_functionx.name.clone(), warn_config);
                 kratex.functions.push(default_function.new_x(inherit_functionx));
             }
         }
diff --git a/source/vir/src/well_formed.rs b/source/vir/src/well_formed.rs
index c3f5566dc5..27f5875310 100644
--- a/source/vir/src/well_formed.rs
+++ b/source/vir/src/well_formed.rs
@@ -9,10 +9,11 @@ use crate::ast_util::{
     is_body_visible_to, is_visible_to_opt, path_as_friendly_rust_name, referenced_vars_expr,
     typ_to_diagnostic_str, types_equal, undecorate_typ,
 };
+use crate::context::WarningConfig;
 use crate::def::user_local_name;
 use crate::early_exit_cf::assert_no_early_exit_in_inv_block;
 use crate::internal_err;
-use crate::messages::{Message, Span, error, error_with_label};
+use crate::messages::{Message, Span, WarningAllow, error, error_with_label};
 use std::collections::HashMap;
 use std::collections::HashSet;
 use std::sync::Arc;
@@ -438,6 +439,7 @@ fn check_one_expr<Emit: EmitError>(
     disallow_private_access: Option<(&Visibility, &str)>,
     area: Area,
     emit: &mut Emit,
+    warn_config: &Option<WarningConfig>,
 ) -> Result<(), VirErr> {
     match &expr.x {
         ExprX::Var(x) => {
@@ -620,10 +622,16 @@ fn check_one_expr<Emit: EmitError>(
         ExprX::AssertBy { ensure, vars, .. } => match &ensure.x {
             ExprX::Binary(crate::ast::BinaryOp::Implies, _, _) => {
                 if !vars.is_empty() {
-                    emit.emit(None, VirErrAs::Warning(
-                        error(&expr.span, "using ==> in `assert forall` does not currently assume the antecedent in the body; consider using `implies` instead of `==>`")
-                            .help("If you didn't mean to assume the antecedent, we're very curious to hear why! To tell us, please open an issue on the Verus issue tracker on github with the title `Don't always make assert forall assume the antecedent`. If no one opens such an issue, we'll soon change the behavior of Verus to always assume the antecedent of the outermost implication")
-                    ));
+                    crate::messages::warning_maybe_if_in_local_crate(
+                        warn_config,
+                        &expr.span,
+                        &WarningAllow::AssertForallImplication,
+                        || "using ==> in `assert forall` does not currently assume the antecedent in the body; consider using `implies` instead of `==>`",
+                        |msg| {
+                            let msg = msg.help("If you didn't mean to assume the antecedent, we're very curious to hear why! To tell us, please open an issue on the Verus issue tracker on github with the title `Don't always make assert forall assume the antecedent`. If no one opens such an issue, we'll soon change the behavior of Verus to always assume the antecedent of the outermost implication");
+                            emit.emit(None, VirErrAs::Warning(msg));
+                        },
+                    );
                 }
             }
             _ => {}
@@ -888,12 +896,13 @@ fn check_expr<Emit: EmitError>(
     disallow_private_access: Option<(&Visibility, &str)>,
     area: Area,
     emit: &mut Emit,
+    warn_config: &Option<WarningConfig>,
 ) -> Result<(), VirErr> {
     let check_result = crate::ast_visitor::ast_visitor_check(
         expr,
         emit,
         &mut |emit, _scope_map, expr: &Arc<crate::ast::SpannedTyped<ExprX>>| {
-            check_one_expr(ctxt, function, expr, disallow_private_access, area, emit)
+            check_one_expr(ctxt, function, expr, disallow_private_access, area, emit, warn_config)
         },
         &mut |_emit, _scope_map, stmt| check_one_stmt(ctxt, stmt),
         &mut |emit, _scope_map, pattern: &Arc<crate::ast::SpannedTyped<PatternX>>| {
@@ -912,6 +921,7 @@ fn check_function<Emit: EmitError>(
     ctxt: &Ctxt,
     function: &Function,
     emit: &mut Emit,
+    warn_config: &Option<WarningConfig>,
     _no_verify: bool,
 ) -> Result<(), VirErr> {
     if let FunctionKind::TraitMethodImpl { method, .. } = &function.x.kind {
@@ -1286,12 +1296,28 @@ fn check_function<Emit: EmitError>(
     for req in function.x.require.iter() {
         let msg = "'requires' clause of public function";
         let disallow_private_access = Some((&function.x.visibility, msg));
-        check_expr(ctxt, function, req, disallow_private_access, Area::PreState("requires"), emit)?;
+        check_expr(
+            ctxt,
+            function,
+            req,
+            disallow_private_access,
+            Area::PreState("requires"),
+            emit,
+            warn_config,
+        )?;
     }
     for ens in function.x.ensure.0.iter().chain(function.x.ensure.1.iter()) {
         let msg = "'ensures' clause of public function";
         let disallow_private_access = Some((&function.x.visibility, msg));
-        check_expr(ctxt, function, ens, disallow_private_access, Area::PostState, emit)?;
+        check_expr(
+            ctxt,
+            function,
+            ens,
+            disallow_private_access,
+            Area::PostState,
+            emit,
+            warn_config,
+        )?;
     }
     if let Some(r) = &function.x.returns {
         if matches!(*function.x.ret.x.typ, TypX::Opaque { .. }) {
@@ -1322,7 +1348,15 @@ fn check_function<Emit: EmitError>(
 
         let msg = "'requires' clause of public function";
         let disallow_private_access = Some((&function.x.visibility, msg));
-        check_expr(ctxt, function, r, disallow_private_access, Area::PreState("returns"), emit)?;
+        check_expr(
+            ctxt,
+            function,
+            r,
+            disallow_private_access,
+            Area::PreState("returns"),
+            emit,
+            warn_config,
+        )?;
     }
     match &function.x.mask_spec {
         None => {}
@@ -1337,6 +1371,7 @@ fn check_function<Emit: EmitError>(
                     disallow_private_access,
                     Area::PreState("opens_invariants clause"),
                     emit,
+                    warn_config,
                 )?;
             }
         }
@@ -1350,6 +1385,7 @@ fn check_function<Emit: EmitError>(
                 disallow_private_access,
                 Area::PreState("opens_invariants clause"),
                 emit,
+                warn_config,
             )?
         }
     }
@@ -1365,6 +1401,7 @@ fn check_function<Emit: EmitError>(
                 disallow_private_access,
                 Area::PreState("opens_invariants clause"),
                 emit,
+                warn_config,
             )?;
         }
     }
@@ -1378,6 +1415,7 @@ fn check_function<Emit: EmitError>(
             disallow_private_access,
             Area::PreState("decreases clause"),
             emit,
+            warn_config,
         )?;
     }
     if let Some(expr) = &function.x.decrease_when {
@@ -1402,6 +1440,7 @@ fn check_function<Emit: EmitError>(
             disallow_private_access,
             Area::PreState("when clause"),
             emit,
+            warn_config,
         )?;
     }
 
@@ -1410,12 +1449,12 @@ fn check_function<Emit: EmitError>(
         && (function.x.attrs.exec_assume_termination
             || function.x.attrs.exec_allows_no_decreases_clause)
     {
-        emit.emit(
-            None,
-            VirErrAs::Warning(error(
-                &function.span,
-                "if exec_allows_no_decreases_clause is set, decreases checks in exec functions do not guarantee termination of functions with loops",
-            )),
+        crate::messages::warning_maybe_if_in_local_crate(
+            warn_config,
+            &function.span,
+            &WarningAllow::DecreasesWhenExecAllowsNoDecreasesClause,
+            || "if exec_allows_no_decreases_clause is set, decreases checks in exec functions do not guarantee termination of functions with loops",
+            |msg| emit.emit(None, VirErrAs::Warning(msg)),
         );
     }
 
@@ -1430,7 +1469,7 @@ fn check_function<Emit: EmitError>(
         } else {
             None
         };
-        check_expr(ctxt, function, body, disallow_private_access, Area::Body, emit)?;
+        check_expr(ctxt, function, body, disallow_private_access, Area::Body, emit, warn_config)?;
     }
 
     if function.x.attrs.is_type_invariant_fn {
@@ -1694,6 +1733,7 @@ pub fn check_crate(
     krate: &Krate,
     unpruned_krate: &Krate,
     diags: &mut Vec<VirErrAs>,
+    warning_ctx: &crate::context::WarningCtx,
     no_verify: bool,
     no_cheating: bool,
 ) -> Result<CheckDetails, VirErr> {
@@ -1739,6 +1779,9 @@ pub fn check_crate(
     // Check connections between decreases_by specs and proofs
     let mut decreases_by_proof_to_spec: HashMap<Fun, Fun> = HashMap::new();
     for function in krate.functions.iter() {
+        let Some(warn_config) = warning_ctx.fun_warn_configs.get(&function.x.name) else {
+            panic!("missing warn_config for function {:?}", &function.x.name);
+        };
         if let Some(proof_fun) = &function.x.decrease_by {
             let proof_function = if let Some(proof_function) = funs.get(proof_fun) {
                 proof_function
@@ -1889,10 +1932,13 @@ pub fn check_crate(
                 }
             }
             if !found_trigger {
-                diags.push(VirErrAs::Warning(error(
+                crate::messages::warning_maybe_if_in_local_crate(
+                    warn_config,
                     &function.span,
-                    "broadcast functions should have explicit #[trigger] or #![trigger ...]",
-                )));
+                    &WarningAllow::BroadcastWithoutTrigger,
+                    || "broadcast functions should have explicit #[trigger] or #![trigger ...]",
+                    |msg| diags.push(VirErrAs::Warning(msg)),
+                );
             }
         }
     }
@@ -1950,7 +1996,10 @@ pub fn check_crate(
     let ctxt = Ctxt { funs, reveal_groups, dts, traits, krate, unpruned_krate, no_cheating };
     // TODO remove once `uninterp` is enforced for uninterpreted functions
     for function in krate.functions.iter() {
-        check_function(&ctxt, function, &mut emit, no_verify)?;
+        let Some(warn_config) = warning_ctx.fun_warn_configs.get(&function.x.name) else {
+            panic!("missing warn_config for function {:?}", &function.x.name);
+        };
+        check_function(&ctxt, function, &mut emit, warn_config, no_verify)?;
     }
     for dt in krate.datatypes.iter() {
         check_datatype(&ctxt, dt, &mut emit)?;