Allow open_inv attribute on functions

Author: voidc

creusot/src/ctx.rs

@@ -209,6 +209,10 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         def_id: DefId,
         ty: Ty<'tcx>,
     ) -> Option<(DefId, SubstsRef<'tcx>)> {
+        if util::is_open_ty_inv(self.tcx, def_id) {
+            return None;
+        }
+
         debug!("resolving type invariant of {ty:?} in {def_id:?}");
         let param_env = self.param_env(def_id);
         let trait_did = self.get_diagnostic_item(Symbol::intern("creusot_invariant_method"))?;

creusot/src/util.rs

@@ -93,6 +93,10 @@ pub(crate) fn is_extern_spec(tcx: TyCtxt, def_id: DefId) -> bool {
     get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "extern_spec"]).is_some()
 }
 
+pub(crate) fn is_open_ty_inv(tcx: TyCtxt, def_id: DefId) -> bool {
+    get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "open_inv"]).is_some()
+}
+
 pub(crate) fn is_type_invariant(tcx: TyCtxt, def_id: DefId) -> bool {
     let Some(assoc_item) = tcx.opt_associated_item(def_id) else { return false };
     let Some(trait_item_did) = (match assoc_item.container {