diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index ba2e18b76..1ab0d4668 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.124" +let supported_charon_version = "0.1.125" diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 2ebe3d20b..241db025e 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -318,30 +318,28 @@ and generic_args_to_string (env : 'a fmt_env) (generics : generic_args) : string params ^ trait_refs and trait_ref_to_string (env : 'a fmt_env) (tr : trait_ref) : string = - trait_instance_id_to_string env tr.trait_id - -and trait_decl_ref_to_string (env : 'a fmt_env) (tr : trait_decl_ref) : string = - let trait_id = trait_decl_id_to_string env tr.id in - let generics = generic_args_to_string env tr.generics in - trait_id ^ generics - -and trait_instance_id_to_string (env : 'a fmt_env) (id : trait_instance_id) : - string = - match id with + match tr.trait_id with | Self -> "Self" | TraitImpl impl_ref -> trait_impl_ref_to_string env impl_ref - | BuiltinOrAuto (trait, _, _) -> - region_binder_to_string trait_decl_ref_to_string env trait + | BuiltinOrAuto _ -> + region_binder_to_string trait_decl_ref_to_string env tr.trait_decl_ref | Clause id -> trait_db_var_to_string env id | ParentClause (tref, clause_id) -> - let inst_id = trait_instance_id_to_string env tref.trait_id in + let inst_id = trait_ref_to_string env tref in let clause_id = trait_clause_id_to_string env clause_id in "parent(" ^ inst_id ^ ")::" ^ clause_id - | Dyn trait -> - let trait = region_binder_to_string trait_decl_ref_to_string env trait in + | Dyn -> + let trait = + region_binder_to_string trait_decl_ref_to_string env tr.trait_decl_ref + in "dyn(" ^ trait ^ ")" | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")" +and trait_decl_ref_to_string (env : 'a fmt_env) (tr : trait_decl_ref) : string = + let trait_id = trait_decl_id_to_string env tr.id in + let generics = generic_args_to_string env tr.generics in + trait_id ^ generics + and impl_elem_to_string (env : 'a fmt_env) (elem : impl_elem) : string = match elem with | ImplElemTy bound_ty -> diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 1ec710f0a..86cc1a0e2 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -1738,15 +1738,8 @@ and trait_instance_id_of_json (ctx : of_json_ctx) (js : json) : [ ( "BuiltinOrAuto", `Assoc - [ - ("trait_decl_ref", trait_decl_ref); - ("parent_trait_refs", parent_trait_refs); - ("types", types); - ] ); + [ ("parent_trait_refs", parent_trait_refs); ("types", types) ] ); ] -> - let* trait_decl_ref = - region_binder_of_json trait_decl_ref_of_json ctx trait_decl_ref - in let* parent_trait_refs = vector_of_json trait_clause_id_of_json trait_ref_of_json ctx parent_trait_refs @@ -1757,10 +1750,8 @@ and trait_instance_id_of_json (ctx : of_json_ctx) (js : json) : (vector_of_json trait_clause_id_of_json trait_ref_of_json)) ctx types in - Ok (BuiltinOrAuto (trait_decl_ref, parent_trait_refs, types)) - | `Assoc [ ("Dyn", dyn) ] -> - let* dyn = region_binder_of_json trait_decl_ref_of_json ctx dyn in - Ok (Dyn dyn) + Ok (BuiltinOrAuto (parent_trait_refs, types)) + | `String "Dyn" -> Ok Dyn | `Assoc [ ("Unknown", unknown) ] -> let* unknown = string_of_json ctx unknown in Ok (UnknownTrait unknown) diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index bbb34ecfe..2ccdaacab 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -461,22 +461,18 @@ and trait_instance_id = including trait method declarations. Not present in trait implementations as we can use [TraitImpl] intead. *) | BuiltinOrAuto of - trait_decl_ref region_binder - * trait_ref list - * (trait_item_name * ty * trait_ref list) list + trait_ref list * (trait_item_name * ty * trait_ref list) list (** A trait implementation that is computed by the compiler, such as for built-in trait [Sized]. This morally points to an invisible [impl] block; as such it contains the information we may need from one. Fields: - - [trait_decl_ref] - [parent_trait_refs]: Exactly like the same field on [TraitImpl]: the [TraitRef]s required to satisfy the implied predicates on the trait declaration. E.g. since [FnMut: FnOnce], a built-in [T: FnMut] impl would have a [TraitRef] for [T: FnOnce]. - [types]: The values of the associated types for this trait. *) - | Dyn of trait_decl_ref region_binder - (** The automatically-generated implementation for [dyn Trait]. *) + | Dyn (** The automatically-generated implementation for [dyn Trait]. *) | UnknownTrait of string (** For error reporting. *) (** A constraint over a trait associated type. diff --git a/charon/Cargo.lock b/charon/Cargo.lock index cae85d0d5..f53bf0342 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -201,7 +201,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.124" +version = "0.1.125" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index e9e4021d9..dc46e3051 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.124" +version = "0.1.125" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index b73eca55d..35b6296e6 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -109,7 +109,6 @@ pub enum TraitRefKind { /// `Sized`. This morally points to an invisible `impl` block; as such it contains /// the information we may need from one. BuiltinOrAuto { - trait_decl_ref: PolyTraitDeclRef, /// Exactly like the same field on `TraitImpl`: the `TraitRef`s required to satisfy the /// implied predicates on the trait declaration. E.g. since `FnMut: FnOnce`, a built-in `T: /// FnMut` impl would have a `TraitRef` for `T: FnOnce`. @@ -119,7 +118,7 @@ pub enum TraitRefKind { }, /// The automatically-generated implementation for `dyn Trait`. - Dyn(PolyTraitDeclRef), + Dyn, /// For error reporting. #[charon::rename("UnknownTrait")] diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 02c402c85..71ad476fc 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -711,7 +711,6 @@ impl TraitRef { }); TraitRef { kind: TraitRefKind::BuiltinOrAuto { - trait_decl_ref: trait_decl_ref.clone(), parent_trait_refs: parents, types: Default::default(), }, diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index d0221d92e..c8aece2ad 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -283,7 +283,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { } } ImplExprAtom::Dyn => TraitRef { - kind: TraitRefKind::Dyn(trait_decl_ref.clone()), + kind: TraitRefKind::Dyn, trait_decl_ref, }, ImplExprAtom::Builtin { @@ -352,7 +352,6 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { }) .try_collect()?; TraitRefKind::BuiltinOrAuto { - trait_decl_ref: trait_decl_ref.clone(), parent_trait_refs, types, } diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index b5a1efbbb..6059bb90a 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -20,10 +20,17 @@ fn usize_ty() -> Ty { } /// Takes a `T` valid in the context of a trait ref and transforms it into a `T` valid in the -/// context of its vtable definition, i.e. no longer mentions `Self`. If `new_self` is `Some`, we -/// replace any mention of `Self` with it; otherwise we panic if `Self` is mentioned. -fn dynify(mut x: T, new_self: Option) -> T { - struct ReplaceSelfVisitor(Option); +/// context of its vtable definition, i.e. no longer mentions the `Self` type or `Self` clause. If +/// `new_self` is `Some`, we replace any mention of the `Self` type with it; otherwise we panic if +/// `Self` is mentioned. +/// If `for_method` is true, we're handling a value coming from a `AssocFn`, which takes the `Self` +/// clause as its first clause parameter. Otherwise we're in trait scope, where the `Self` clause +/// is represented with `TraitRefKind::SelfId`. +fn dynify(mut x: T, new_self: Option, for_method: bool) -> T { + struct ReplaceSelfVisitor { + new_self: Option, + for_method: bool, + } impl VarsVisitor for ReplaceSelfVisitor { fn visit_type_var(&mut self, v: TypeDbVar) -> Option { if let DeBruijnVar::Bound(DeBruijnId::ZERO, type_id) = v { @@ -32,7 +39,7 @@ fn dynify(mut x: T, new_self: Option) -> T { TyKind::TypeVar(DeBruijnVar::Bound(DeBruijnId::ZERO, TypeVarId::new(new_id))) .into_ty() } else { - self.0.clone().expect( + self.new_self.clone().expect( "Found unexpected `Self` type when constructing vtable", ) @@ -41,8 +48,28 @@ fn dynify(mut x: T, new_self: Option) -> T { None } } + + fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option { + if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v { + if self.for_method && clause_id == TraitClauseId::ZERO { + // That's the `Self` clause. + Some(TraitRefKind::Dyn) + } else { + panic!("Found unexpected clause var when constructing vtable: {v}") + } + } else { + None + } + } + + fn visit_self_clause(&mut self) -> Option { + Some(TraitRefKind::Dyn) + } } - x.visit_vars(&mut ReplaceSelfVisitor(new_self)); + x.visit_vars(&mut ReplaceSelfVisitor { + new_self, + for_method, + }); x } @@ -126,22 +153,8 @@ impl ItemTransCtx<'_, '_> { pub fn trait_is_dyn_compatible(&mut self, def_id: &hax::DefId) -> Result { let def = self.poly_hax_def(def_id)?; Ok(match def.kind() { - hax::FullDefKind::Trait { - dyn_self: Some(dyn_self), - .. - } - | hax::FullDefKind::TraitAlias { - dyn_self: Some(dyn_self), - .. - } => { - match dyn_self.kind() { - // `dyn_self` looks like `dyn Trait`. The first - // predicate is `_: Trait`, the rest are type constraints. Hence the - // trait recursively has no assoc types iff `preds.len() == 1`. - hax::TyKind::Dynamic(_, preds, _) => preds.predicates.len() == 1, - _ => panic!("unexpected `dyn_self`: {dyn_self:?}"), - } - } + hax::FullDefKind::Trait { dyn_self, .. } + | hax::FullDefKind::TraitAlias { dyn_self, .. } => dyn_self.is_some(), _ => false, }) } @@ -186,6 +199,15 @@ impl ItemTransCtx<'_, '_> { .generics .types .remove_and_shift_ids(TypeVarId::ZERO); + + // The vtable type also takes associated types as parameters. + let assoc_tys: Vec<_> = tref + .trait_associated_types(&self.hax_state_with_id()) + .iter() + .map(|ty| self.translate_ty(span, ty)) + .try_collect()?; + vtable_ref.generics.types.extend(assoc_tys); + Ok(Some(vtable_ref)) } @@ -329,7 +351,6 @@ impl ItemTransCtx<'_, '_> { } self.translate_def_generics(span, trait_def)?; - // TODO(dyn): add the associated types. let (hax::FullDefKind::Trait { dyn_self, @@ -349,7 +370,36 @@ impl ItemTransCtx<'_, '_> { }; // The `dyn Trait` type for this trait. - let mut dyn_self = self.translate_ty(span, dyn_self)?; + let mut dyn_self = { + let dyn_self = self.translate_ty(span, dyn_self)?; + let TyKind::DynTrait(mut dyn_pred) = dyn_self.kind().clone() else { + panic!("incorrect `dyn_self`") + }; + + // Add one generic parameter for each associated type of this trait and its parents. We + // then use that in `dyn_self` + for (i, ty_constraint) in dyn_pred + .binder + .params + .trait_type_constraints + .iter_mut() + .enumerate() + { + let name = format!("Ty{i}"); + let new_ty = self + .the_only_binder_mut() + .params + .types + .push_with(|index| TypeVar { index, name }); + // Moving that type under two levels of binders: the `DynPredicate` binder and the + // type constraint binder. + let new_ty = + TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::new(2), new_ty)).into_ty(); + ty_constraint.skip_binder.ty = new_ty; + } + TyKind::DynTrait(dyn_pred).into_ty() + }; + // First construct fields that use the real method signatures (which may use the `Self` // type). We fixup the types and generics below. let fields = self.gen_vtable_struct_fields(span, trait_def, implied_predicates)?; @@ -360,9 +410,9 @@ impl ItemTransCtx<'_, '_> { // from the generic parameters. let mut generics = self.into_generics(); { - dyn_self = dynify(dyn_self, None); - generics = dynify(generics, Some(dyn_self.clone())); - kind = dynify(kind, Some(dyn_self.clone())); + dyn_self = dynify(dyn_self, None, false); + generics = dynify(generics, Some(dyn_self.clone()), false); + kind = dynify(kind, Some(dyn_self.clone()), true); generics.types.remove_and_shift_ids(TypeVarId::ZERO); generics.types.iter_mut().for_each(|ty| { ty.index -= 1; @@ -434,17 +484,15 @@ impl ItemTransCtx<'_, '_> { } /// E.g., - /// global - /// trait::{vtable_instance}::> : - /// trait::{vtable} = trait::{vtable} { - /// drop: &ignore / & as Drop>::drop, - /// size: size_of(>), - /// align: align_of(>), - /// method_0: & as Trait>::method_0::{shim}, - /// method_1: & as Trait>::method_1::{shim}, + /// global {impl Trait for Foo}::vtable: Trait::{vtable} { + /// size: size_of(Foo), + /// align: align_of(Foo), + /// drop: ::drop, + /// method_0: ::method_0::{shim}, + /// method_1: ::method_1::{shim}, /// ... - /// super_trait_0: &SuperTrait0::{vtable_instance}::>, - /// super_trait_1: &SuperTrait1::{vtable_instance}::>, + /// super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>, + /// super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>, /// ... /// } pub(crate) fn translate_vtable_instance( @@ -539,11 +587,12 @@ impl ItemTransCtx<'_, '_> { }; for ((clause, _), impl_expr) in implied_predicates.predicates.iter().zip(implied_impl_exprs) { - if let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() { - // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait. - if !self.pred_is_for_self(&pred.trait_ref) { - continue; - } + let hax::ClauseKind::Trait(pred) = clause.kind.hax_skip_binder_ref() else { + continue; + }; + // If a clause looks like `Self: OtherTrait<...>`, we consider it a supertrait. + if !self.pred_is_for_self(&pred.trait_ref) { + continue; } let vtable_def_ref = self diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 7747ac508..62fa4af81 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1687,9 +1687,9 @@ impl Display for TraitItemName { } } -impl FmtWithCtx for TraitRefKind { +impl FmtWithCtx for TraitRef { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { + match &self.kind { TraitRefKind::SelfId => write!(f, "Self"), TraitRefKind::ParentClause(sub, clause_id) => { let sub = sub.with_ctx(ctx); @@ -1706,12 +1706,8 @@ impl FmtWithCtx for TraitRefKind { write!(f, "{}", impl_ref.with_ctx(ctx)) } TraitRefKind::Clause(id) => write!(f, "{}", id.with_ctx(ctx)), - TraitRefKind::BuiltinOrAuto { - trait_decl_ref: tr, - types, - .. - } => { - write!(f, "{}", tr.with_ctx(ctx))?; + TraitRefKind::BuiltinOrAuto { types, .. } => { + write!(f, "{}", self.trait_decl_ref.with_ctx(ctx))?; if !types.is_empty() { let types = types .iter() @@ -1724,18 +1720,12 @@ impl FmtWithCtx for TraitRefKind { } Ok(()) } - TraitRefKind::Dyn(tr) => write!(f, "{}", tr.with_ctx(ctx)), + TraitRefKind::Dyn { .. } => write!(f, "{}", self.trait_decl_ref.with_ctx(ctx)), TraitRefKind::Unknown(msg) => write!(f, "UNKNOWN({msg})"), } } } -impl FmtWithCtx for TraitRef { - fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - self.kind.fmt_with_ctx(ctx, f) - } -} - impl FmtWithCtx for TraitTypeConstraint { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { let trait_ref = self.trait_ref.with_ctx(ctx); diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 0a64c6877..caa75ad7f 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -225,19 +225,18 @@ impl VisitAst for CheckGenericsVisitor<'_> { } } } - fn enter_trait_ref_kind(&mut self, x: &TraitRefKind) { - match x { + fn enter_trait_ref(&mut self, x: &TraitRef) { + match &x.kind { TraitRefKind::Clause(var) => { if self.binder_stack.get_var(*var).is_none() { self.error(format!("Found incorrect clause var: {var}")); } } TraitRefKind::BuiltinOrAuto { - trait_decl_ref, parent_trait_refs, types, } => { - let trait_id = trait_decl_ref.skip_binder.id; + let trait_id = x.trait_decl_ref.skip_binder.id; let target = GenericsSource::item(trait_id); let Some(tdecl) = self.ctx.translated.trait_decls.get(trait_id) else { return; diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs index 525bc9d34..91c6ab96f 100644 --- a/charon/src/transform/expand_associated_types.rs +++ b/charon/src/transform/expand_associated_types.rs @@ -224,7 +224,7 @@ mod trait_ref_path { TraitRefKind::ItemClause(..) => unreachable!(), TraitRefKind::TraitImpl(..) | TraitRefKind::BuiltinOrAuto { .. } - | TraitRefKind::Dyn(..) + | TraitRefKind::Dyn { .. } | TraitRefKind::Unknown(..) => None, } } @@ -874,7 +874,7 @@ impl<'a> ComputeItemModifications<'a> { ) } } - TraitRefKind::Dyn(..) => { + TraitRefKind::Dyn { .. } => { register_error!( self.ctx, span, @@ -990,7 +990,7 @@ impl UpdateItemBody<'_> { } }, // TODO: add enough info to recover assoc types. - TraitRefKind::Dyn(..) => None, + TraitRefKind::Dyn { .. } => None, TraitRefKind::Unknown(..) => None, } } @@ -1126,23 +1126,9 @@ impl VisitAstMut for UpdateItemBody<'_> { // Process trait refs fn enter_trait_ref(&mut self, tref: &mut TraitRef) { self.process_poly_trait_decl_ref(&mut tref.trait_decl_ref, tref.kind.clone()); - } - fn enter_trait_ref_kind(&mut self, kind: &mut TraitRefKind) { - // There are some stray `TraitDeclRef`s that we have to update. - // TODO: we should make `TraitRefKind` recursively contain full `TraitRef`s so we have the - // implemented trait info at each level. This would require hax to give us more info. - let kind_clone = kind.clone(); - match kind { - TraitRefKind::Dyn(tref) => { - self.process_poly_trait_decl_ref(tref, kind_clone); - } - TraitRefKind::BuiltinOrAuto { - trait_decl_ref: tref, - types, - .. - } => { - self.process_poly_trait_decl_ref(tref, kind_clone); - let target = GenericsSource::item(tref.skip_binder.id); + match &mut tref.kind { + TraitRefKind::BuiltinOrAuto { types, .. } => { + let target = GenericsSource::item(tref.trait_decl_ref.skip_binder.id); if let Some(decl_modifs) = self.item_modifications.get(&target) { assert!(decl_modifs.required_extra_assoc_types().count() == 0); if decl_modifs.add_type_params { diff --git a/charon/tests/cargo/dependencies.out b/charon/tests/cargo/dependencies.out index ac1c8600c..71b08e3fe 100644 --- a/charon/tests/cargo/dependencies.out +++ b/charon/tests/cargo/dependencies.out @@ -36,7 +36,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 2833fa515..16b06f3c9 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -12,7 +12,7 @@ pub trait Index parent_clause1 : [@TraitClause1]: MetaSized parent_clause2 : [@TraitClause2]: MetaSized fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx, Self_Output>[Self] - non-dyn-compatible + vtable: core::ops::index::Index::{vtable} } // Full name: core::marker::Sized @@ -41,7 +41,7 @@ where parent_clause1 = @TraitClause1::parent_clause0 parent_clause2 = @TraitClause2::parent_clause2 fn index<'_0> = {impl Index for Array}::index<'_0_0, T, I, Clause2_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl Index for Array}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::ops::index::IndexMut @@ -52,7 +52,7 @@ pub trait IndexMut parent_clause1 : [@TraitClause1]: Index parent_clause2 : [@TraitClause2]: MetaSized fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx, Self_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::index::IndexMut::{vtable} } // Full name: core::array::{impl IndexMut for Array}::index_mut @@ -73,7 +73,7 @@ where parent_clause1 = {impl Index for Array}[@TraitClause0, @TraitClause1, @TraitClause2::parent_clause1] parent_clause2 = @TraitClause1::parent_clause0 fn index_mut<'_0> = {impl IndexMut for Array}::index_mut<'_0_0, T, I, Clause2_Clause1_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl IndexMut for Array}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::ops::drop::Drop @@ -139,7 +139,7 @@ pub trait SliceIndex fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut[Self] fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T, Self_Output>[Self] fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T, Self_Output>[Self] - non-dyn-compatible + vtable: core::slice::index::SliceIndex::{vtable} } // Full name: core::slice::index::{impl Index for Slice}::index @@ -160,7 +160,7 @@ where parent_clause1 = @TraitClause1::parent_clause0 parent_clause2 = @TraitClause2::parent_clause3 fn index<'_0> = {impl Index for Slice}::index<'_0_0, T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl Index for Slice}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::slice::index::{impl IndexMut for Slice}::index_mut @@ -181,7 +181,7 @@ where parent_clause1 = {impl Index for Slice}[@TraitClause0, @TraitClause1, @TraitClause2] parent_clause2 = @TraitClause1::parent_clause0 fn index_mut<'_0> = {impl IndexMut for Slice}::index_mut<'_0_0, T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl IndexMut for Slice}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::slice::index::private_slice_index::{impl Sealed for Range[Sized]} @@ -259,7 +259,7 @@ where fn get_unchecked_mut = {impl SliceIndex, Slice> for Range[Sized]}::get_unchecked_mut[@TraitClause0] fn index<'_0> = {impl SliceIndex, Slice> for Range[Sized]}::index<'_0_0, T>[@TraitClause0] fn index_mut<'_0> = {impl SliceIndex, Slice> for Range[Sized]}::index_mut<'_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl SliceIndex, Slice> for Range[Sized]}::{vtable}[@TraitClause0] } // Full name: core::slice::{Slice}::len diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out index 2106d83aa..6258d21eb 100644 --- a/charon/tests/ui/associated-types.out +++ b/charon/tests/ui/associated-types.out @@ -321,14 +321,14 @@ trait test_crate::loopy::Bar { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::loopy::Bar::{vtable} } // Full name: test_crate::loopy::{impl test_crate::loopy::Bar for ()} impl test_crate::loopy::Bar for () { parent_clause0 = MetaSized<()> parent_clause1 = Sized - non-dyn-compatible + vtable: {impl test_crate::loopy::Bar for ()}::{vtable} } trait test_crate::loopy::Foo @@ -339,7 +339,7 @@ trait test_crate::loopy::Foo parent_clause3 : [@TraitClause3]: test_crate::loopy::Bar type FooTy type Self_Clause3_BarTy - non-dyn-compatible + vtable: test_crate::loopy::Foo::{vtable} } // Full name: test_crate::loopy::{impl test_crate::loopy::Foo for ()} @@ -350,7 +350,7 @@ impl test_crate::loopy::Foo for () { parent_clause3 = {impl test_crate::loopy::Bar for ()} type FooTy = () type Self_Clause3_BarTy = bool - non-dyn-compatible + vtable: {impl test_crate::loopy::Foo for ()}::{vtable} } // Full name: test_crate::loopy::Baz @@ -363,7 +363,7 @@ trait Baz parent_clause4 : [@TraitClause4]: Sized type BazTy type Self_Clause3_BarTy - non-dyn-compatible + vtable: test_crate::loopy::Baz::{vtable} } // Full name: test_crate::loopy::{impl Baz<()> for ()} @@ -375,7 +375,7 @@ impl Baz<()> for () { parent_clause4 = Sized type BazTy = usize type Self_Clause3_BarTy = bool - non-dyn-compatible + vtable: {impl Baz<()> for ()}::{vtable} } trait test_crate::loopy_with_generics::Bar<'a, Self, T, U, Self_BarTy> @@ -384,7 +384,7 @@ trait test_crate::loopy_with_generics::Bar<'a, Self, T, U, Self_BarTy> parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Sized - non-dyn-compatible + vtable: test_crate::loopy_with_generics::Bar::{vtable}<'a, T, U, Self_BarTy> } // Full name: test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Bar<'a, u8, T, &'a (T)> for ()} @@ -397,7 +397,7 @@ where parent_clause1 = Sized parent_clause2 = @TraitClause0 parent_clause3 = Sized<&'_ (T)> - non-dyn-compatible + vtable: {impl test_crate::loopy_with_generics::Bar<'a, u8, T, &'a (T)> for ()}::{vtable}<'a, T>[@TraitClause0] } trait test_crate::loopy_with_generics::Foo<'b, Self, T> @@ -409,7 +409,7 @@ trait test_crate::loopy_with_generics::Foo<'b, Self, T> parent_clause4 : [@TraitClause4]: test_crate::loopy_with_generics::Bar<'b, Self::FooTy, u8, Option[Self::parent_clause1], Self::Self_Clause4_BarTy> type FooTy type Self_Clause4_BarTy - non-dyn-compatible + vtable: test_crate::loopy_with_generics::Foo::{vtable}<'b, T, Self::FooTy> } // Full name: test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Foo<'static, u16> for ()} @@ -421,7 +421,7 @@ impl test_crate::loopy_with_generics::Foo<'static, u16> for () { parent_clause4 = {impl test_crate::loopy_with_generics::Bar<'a, u8, T, &'a (T)> for ()}<'_, Option[Sized]>[Sized[Sized]>] type FooTy = () type Self_Clause4_BarTy = &'_ (Option[Sized]) - non-dyn-compatible + vtable: {impl test_crate::loopy_with_generics::Foo<'static, u16> for ()}::{vtable} } // Full name: test_crate::cow::Cow @@ -445,7 +445,7 @@ where parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Sized - non-dyn-compatible + vtable: test_crate::params::Foo::{vtable}<'a, T, Self_X, Self_Item> } // Full name: test_crate::params::{impl test_crate::params::Foo<'a, Option[@TraitClause0], &'a (()), &'a ((Option[@TraitClause0], &'a (())))> for ()} @@ -458,7 +458,7 @@ where parent_clause1 = Sized[@TraitClause0]> parent_clause2 = Sized<&'_ (())> parent_clause3 = Sized<&'_ ((Option[@TraitClause0], &'_ (())))> - non-dyn-compatible + vtable: {impl test_crate::params::Foo<'a, Option[@TraitClause0], &'a (()), &'a ((Option[@TraitClause0], &'a (())))> for ()}::{vtable}<'a, T>[@TraitClause0] } diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out index e1f7927ae..28981feac 100644 --- a/charon/tests/ui/closure-as-fn.out +++ b/charon/tests/ui/closure-as-fn.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -68,7 +68,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index 3a2fd7a36..f85a55196 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -29,7 +29,7 @@ pub trait FnOnce parent_clause2 : [@TraitClause2]: Tuple parent_clause3 : [@TraitClause3]: Sized fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -41,7 +41,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args, Self_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::array::{Array}::map @@ -106,7 +106,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args, Self_Clause1_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args, Clause0_Clause1_Clause1_Output>(@1: &'_0 (Self), @2: Args) -> Clause0_Clause1_Clause1_Output diff --git a/charon/tests/ui/closures_with_where.out b/charon/tests/ui/closures_with_where.out index 1fef36c1c..25ee8b690 100644 --- a/charon/tests/ui/closures_with_where.out +++ b/charon/tests/ui/closures_with_where.out @@ -30,7 +30,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -42,7 +42,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::array::from_fn diff --git a/charon/tests/ui/dictionary_passing_style_woes.out b/charon/tests/ui/dictionary_passing_style_woes.out index afa84658c..60ad2b1f2 100644 --- a/charon/tests/ui/dictionary_passing_style_woes.out +++ b/charon/tests/ui/dictionary_passing_style_woes.out @@ -63,7 +63,7 @@ trait Iterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::Iterator::{vtable} } // Full name: test_crate::IntoIterator @@ -73,7 +73,7 @@ trait IntoIterator parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Iterator - non-dyn-compatible + vtable: test_crate::IntoIterator::{vtable} } // Full name: test_crate::{impl IntoIterator for I} @@ -86,7 +86,7 @@ where parent_clause1 = @TraitClause1::parent_clause1 parent_clause2 = @TraitClause0 parent_clause3 = @TraitClause1 - non-dyn-compatible + vtable: {impl IntoIterator for I}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: test_crate::callee @@ -128,7 +128,7 @@ trait X parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized fn method<'_0> = method<'_0_0, Self, Self_Assoc>[Self] - non-dyn-compatible + vtable: test_crate::X::{vtable} } // Full name: test_crate::X::method @@ -141,7 +141,7 @@ trait A { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: X - non-dyn-compatible + vtable: test_crate::A::{vtable} } // Full name: test_crate::B @@ -149,7 +149,7 @@ trait B { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: X - non-dyn-compatible + vtable: test_crate::B::{vtable} } // Full name: test_crate::a diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index 2c3106dae..c113a4024 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -86,7 +86,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -98,7 +98,16 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), + method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable} [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output>), } // Full name: core::ops::function::Fn @@ -110,7 +119,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } // Full name: core::ops::function::Fn::call diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index 5e596cc2d..9487c2f5e 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -1,11 +1,357 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: core::ops::arith::Add +#[lang_item("add")] +pub trait Add +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Sized + type Output + fn add = core::ops::arith::Add::add[Self] + vtable: core::ops::arith::Add::{vtable} +} + +// Full name: core::ops::arith::{impl Add for &'a (i32)}::add +pub fn {impl Add for &'a (i32)}::add<'a>(@1: &'a (i32), @2: i32) -> i32 + +// Full name: core::ops::arith::{impl Add for &'a (i32)} +impl<'a> Add for &'a (i32) { + parent_clause0 = MetaSized<&'_ (i32)> + parent_clause1 = Sized + parent_clause2 = Sized + type Output = i32 + fn add = {impl Add for &'a (i32)}::add<'a> + vtable: {impl Add for &'a (i32)}::{vtable}<'a> +} + +#[lang_item("add")] +pub fn core::ops::arith::Add::add(@1: Self, @2: Rhs) -> @TraitClause0::Output +where + [@TraitClause0]: Add, + +// Full name: test_crate::Super +trait Super +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + fn super_method<'_0> = test_crate::Super::super_method<'_0_0, Self, T>[Self] + vtable: test_crate::Super::{vtable} +} + +fn test_crate::Super::super_method<'_0, Self, T>(@1: &'_0 (Self), @2: T) -> i32 +where + [@TraitClause0]: Super, + +// Full name: test_crate::Internal +trait Internal +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + type Internal + fn internal_method<'_0> = test_crate::Internal::internal_method<'_0_0, Self>[Self] + vtable: test_crate::Internal::{vtable} +} + +fn test_crate::Internal::internal_method<'_0, Self>(@1: &'_0 (Self)) -> @TraitClause0::Internal +where + [@TraitClause0]: Internal, + +// Full name: test_crate::Left +trait Left +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Internal + parent_clause2 : [@TraitClause2]: Sized + type Left + fn left_method<'_0> = test_crate::Left::left_method<'_0_0, Self>[Self] + vtable: test_crate::Left::{vtable} +} + +fn test_crate::Left::left_method<'_0, Self>(@1: &'_0 (Self)) -> @TraitClause0::Left +where + [@TraitClause0]: Left, + +// Full name: test_crate::Right +trait Right +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Internal + parent_clause2 : [@TraitClause2]: Super + parent_clause3 : [@TraitClause3]: Sized + parent_clause4 : [@TraitClause4]: Sized + type Right + fn right_method<'_0> = test_crate::Right::right_method<'_0_0, Self, T>[Self] + vtable: test_crate::Right::{vtable} +} + +fn test_crate::Right::right_method<'_0, Self, T>(@1: &'_0 (Self)) -> @TraitClause0::Right +where + [@TraitClause0]: Right, + +struct test_crate::Join::{vtable} { + size: usize, + align: usize, + drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3)), + method_join_method: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3))) -> (Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3), T>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3), T>::parent_clause2::Right), + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (test_crate::Left::{vtable} [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3), T>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3), T>::parent_clause1::parent_clause1::Internal>), + super_trait_2: &'static (test_crate::Right::{vtable} [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3), T>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = Ty0 + @TraitClause1_0::parent_clause2::Right = Ty1 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty2 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty3), T>::parent_clause1::parent_clause1::Internal>), +} + +// Full name: test_crate::Join +trait Join +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Left + parent_clause2 : [@TraitClause2]: Right + parent_clause3 : [@TraitClause3]: Sized + fn join_method<'_0> = test_crate::Join::join_method<'_0_0, Self, T>[Self] + vtable: test_crate::Join::{vtable} +} + +fn test_crate::Join::join_method<'_0, Self, T>(@1: &'_0 (Self)) -> (@TraitClause0::parent_clause1::Left, @TraitClause0::parent_clause2::Right) +where + [@TraitClause0]: Join, + +// Full name: test_crate::{impl Super for i32}::super_method +fn {impl Super for i32}::super_method<'_0>(@1: &'_0 (i32), @2: i32) -> i32 +{ + let @0: i32; // return + let self@1: &'_ (i32); // arg #1 + let arg@2: i32; // arg #2 + let @3: &'_ (i32); // anonymous local + let @4: i32; // anonymous local + + storage_live(@3) + @3 := copy (self@1) + storage_live(@4) + @4 := copy (arg@2) + @0 := {impl Add for &'a (i32)}::add<'_>(move (@3), move (@4)) + storage_dead(@4) + storage_dead(@3) + return +} + +// Full name: test_crate::{impl Super for i32} +impl Super for i32 { + parent_clause0 = MetaSized + parent_clause1 = Sized + fn super_method<'_0> = {impl Super for i32}::super_method<'_0_0> + vtable: {impl Super for i32}::{vtable} +} + +// Full name: test_crate::{impl Internal for i32}::internal_method +fn {impl Internal for i32}::internal_method<'_0>(@1: &'_0 (i32)) -> i32 +{ + let @0: i32; // return + let self@1: &'_ (i32); // arg #1 + let @2: i32; // anonymous local + let @3: i32; // anonymous local + + storage_live(@3) + storage_live(@2) + @2 := copy (*(self@1)) + @3 := copy (@2) panic.+ const (1 : i32) + @0 := move (@3) + storage_dead(@2) + return +} + +// Full name: test_crate::{impl Internal for i32} +impl Internal for i32 { + parent_clause0 = MetaSized + parent_clause1 = Sized + type Internal = i32 + fn internal_method<'_0> = {impl Internal for i32}::internal_method<'_0_0> + vtable: {impl Internal for i32}::{vtable} +} + +// Full name: test_crate::{impl Left for i32}::left_method +fn {impl Left for i32}::left_method<'_0>(@1: &'_0 (i32)) -> i32 +{ + let @0: i32; // return + let self@1: &'_ (i32); // arg #1 + let @2: i32; // anonymous local + let @3: i32; // anonymous local + + storage_live(@3) + storage_live(@2) + @2 := copy (*(self@1)) + @3 := copy (@2) panic.+ const (2 : i32) + @0 := move (@3) + storage_dead(@2) + return +} + +// Full name: test_crate::{impl Left for i32} +impl Left for i32 { + parent_clause0 = MetaSized + parent_clause1 = {impl Internal for i32} + parent_clause2 = Sized + type Left = i32 + fn left_method<'_0> = {impl Left for i32}::left_method<'_0_0> + vtable: {impl Left for i32}::{vtable} +} + +// Full name: test_crate::{impl Right for i32}::right_method +fn {impl Right for i32}::right_method<'_0>(@1: &'_0 (i32)) -> i32 +{ + let @0: i32; // return + let self@1: &'_ (i32); // arg #1 + let @2: i32; // anonymous local + let @3: i32; // anonymous local + let @4: i32; // anonymous local + let @5: i32; // anonymous local + let @6: i32; // anonymous local + let @7: &'_ (i32); // anonymous local + let @8: i32; // anonymous local + let @9: i32; // anonymous local + let @10: &'_ (i32); // anonymous local + let @11: i32; // anonymous local + + storage_live(@5) + storage_live(@8) + storage_live(@11) + storage_live(@2) + storage_live(@3) + storage_live(@4) + @4 := copy (*(self@1)) + @5 := copy (@4) panic.+ const (3 : i32) + @3 := move (@5) + storage_dead(@4) + storage_live(@6) + storage_live(@7) + @7 := &*(self@1) + @6 := {impl Internal for i32}::internal_method<'_>(move (@7)) + storage_dead(@7) + @8 := copy (@3) panic.+ copy (@6) + @2 := move (@8) + storage_dead(@6) + storage_dead(@3) + storage_live(@9) + storage_live(@10) + @10 := &*(self@1) + @9 := {impl Super for i32}::super_method<'_>(move (@10), const (10 : i32)) + storage_dead(@10) + @11 := copy (@2) panic.+ copy (@9) + @0 := move (@11) + storage_dead(@9) + storage_dead(@2) + return +} + +// Full name: test_crate::{impl Right for i32} +impl Right for i32 { + parent_clause0 = MetaSized + parent_clause1 = {impl Internal for i32} + parent_clause2 = {impl Super for i32} + parent_clause3 = Sized + parent_clause4 = Sized + type Right = i32 + fn right_method<'_0> = {impl Right for i32}::right_method<'_0_0> + vtable: {impl Right for i32}::{vtable} +} + +// Full name: test_crate::{impl Join for i32}::join_method +fn {impl Join for i32}::join_method<'_0>(@1: &'_0 (i32)) -> (i32, i32) +{ + let @0: (i32, i32); // return + let self@1: &'_ (i32); // arg #1 + let @2: i32; // anonymous local + let @3: &'_ (i32); // anonymous local + let @4: i32; // anonymous local + let @5: &'_ (i32); // anonymous local + + storage_live(@2) + storage_live(@3) + @3 := &*(self@1) + @2 := {impl Left for i32}::left_method<'_>(move (@3)) + storage_dead(@3) + storage_live(@4) + storage_live(@5) + @5 := &*(self@1) + @4 := {impl Right for i32}::right_method<'_>(move (@5)) + storage_dead(@5) + @0 := (move (@2), move (@4)) + storage_dead(@4) + storage_dead(@2) + return +} + +// Full name: test_crate::{impl Join for i32}::{vtable} +fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} +{ + let ret@0: test_crate::Join::{vtable}; // return + let @1: &'static (test_crate::Left::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32), i32>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + let @2: &'static (test_crate::Right::{vtable} [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32), i32>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local + + storage_live(@1) + storage_live(@2) + @1 := &{impl Left for i32}::{vtable} + @2 := &{impl Right for i32}::{vtable} + ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({impl Join for i32}::join_method), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@1), super_trait_2: move (@2) } + return +} + +// Full name: test_crate::{impl Join for i32}::{vtable} +static {impl Join for i32}::{vtable}: test_crate::Join::{vtable} = {impl Join for i32}::{vtable}() + +// Full name: test_crate::{impl Join for i32} +impl Join for i32 { + parent_clause0 = MetaSized + parent_clause1 = {impl Left for i32} + parent_clause2 = {impl Right for i32} + parent_clause3 = Sized + fn join_method<'_0> = {impl Join for i32}::join_method<'_0_0> + vtable: {impl Join for i32}::{vtable} +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let v@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32)); // local + let @2: &'_ (i32); // anonymous local + let @3: &'_ (i32); // anonymous local + let @4: i32; // anonymous local + let @5: (i32, i32); // anonymous local + let @6: &'_ ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32)); // anonymous local + + storage_live(v@1) + storage_live(@2) + storage_live(@3) + storage_live(@4) + @4 := const (97 : i32) + @3 := &@4 + @2 := &*(@3) + v@1 := unsize_cast<&'_ (i32), &'_ ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32)), {impl Join for i32}>(move (@2)) + storage_dead(@2) + storage_dead(@3) + storage_live(@5) + storage_live(@6) + @6 := &*(v@1) + @5 := Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::Left = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32), i32>::join_method<'_>(move (@6)) + storage_dead(@6) + storage_dead(@5) + @0 := () + storage_dead(@4) + storage_dead(v@1) + @0 := () + return +} + -thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:426:14: -trait should be dyn-compatible -note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace -error: Thread panicked when extracting item `test_crate::{impl#4}`. - --> tests/ui/dyn-with-diamond-supertraits.rs:47:1 - | -47 | impl Join for i32 { - | ^^^^^^^^^^^^^^^^^^^^^^ -ERROR Charon failed to translate this code (1 errors) diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.rs b/charon/tests/ui/dyn-with-diamond-supertraits.rs index 67e845c74..b990247b4 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.rs +++ b/charon/tests/ui/dyn-with-diamond-supertraits.rs @@ -1,4 +1,3 @@ -//@ known-failure /// This tests `dyn` with a diamond hierarchy between supertraits. Fails for now because we don't /// support dyn with associated types. diff --git a/charon/tests/ui/gosim-demo.out b/charon/tests/ui/gosim-demo.out index ff6ad063b..32bfecab0 100644 --- a/charon/tests/ui/gosim-demo.out +++ b/charon/tests/ui/gosim-demo.out @@ -194,7 +194,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::iter::traits::accum::Sum @@ -242,7 +242,7 @@ where type Item type IntoIter fn into_iter = core::iter::traits::collect::IntoIterator::into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -293,7 +293,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -306,7 +306,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } #[lang_item("next")] @@ -360,7 +360,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -372,7 +372,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -439,7 +439,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::slice::iter::Iter @@ -464,7 +464,7 @@ where parent_clause1 = Sized<&'_ (T)> type Item = &'a (T) fn next<'_0> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::next<'a, '_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for Iter<'a, T>[@TraitClause0]}::{vtable}<'a, T>[@TraitClause0] } // Full name: core::slice::iter::{impl IntoIterator for &'a (Slice)}::into_iter @@ -484,7 +484,7 @@ where type Item = &'a (T) type IntoIter = Iter<'a, T>[@TraitClause0] fn into_iter = {impl IntoIterator for &'a (Slice)}::into_iter<'a, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl IntoIterator for &'a (Slice)}::{vtable}<'a, T>[@TraitClause0] } // Full name: std::io::stdio::_eprint diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out index 9bc69b23a..f61eaa900 100644 --- a/charon/tests/ui/impl-trait.out +++ b/charon/tests/ui/impl-trait.out @@ -87,7 +87,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output @@ -102,7 +102,7 @@ pub trait Foo parent_clause2 : [@TraitClause2]: Clone type Type fn get_ty<'_0> = test_crate::Foo::get_ty<'_0_0, Self>[Self] - non-dyn-compatible + vtable: test_crate::Foo::{vtable} } pub fn test_crate::Foo::get_ty<'_0, Self>(@1: &'_0 (Self)) -> &'_0 (@TraitClause0::Type) @@ -134,7 +134,7 @@ impl Foo for () { parent_clause2 = {impl Clone for u32} type Type = u32 fn get_ty<'_0> = {impl Foo for ()}::get_ty<'_0_0> - non-dyn-compatible + vtable: {impl Foo for ()}::{vtable} } // Full name: test_crate::mk_foo diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out index fc9967a0e..ffc8cb293 100644 --- a/charon/tests/ui/issue-118-generic-copy.out +++ b/charon/tests/ui/issue-118-generic-copy.out @@ -118,7 +118,7 @@ trait Trait parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Copy type Ty - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::copy_assoc_ty diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out index 7714b807e..f7cd8f1b1 100644 --- a/charon/tests/ui/issue-297-cfg.out +++ b/charon/tests/ui/issue-297-cfg.out @@ -126,7 +126,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::iter::traits::accum::Sum @@ -174,7 +174,7 @@ where type Item type IntoIter fn into_iter = core::iter::traits::collect::IntoIterator::into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -220,7 +220,7 @@ where type Item = @TraitClause1::Item type IntoIter = I fn into_iter = {impl IntoIterator for I}::into_iter[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl IntoIterator for I}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::collect::Extend @@ -247,7 +247,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -260,7 +260,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } #[lang_item("next")] @@ -314,7 +314,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -326,7 +326,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -393,7 +393,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::slice::iter::Chunks @@ -417,7 +417,7 @@ where parent_clause1 = Sized<&'_ (Slice)> type Item = &'a (Slice) fn next<'_0> = {impl Iterator for Chunks<'a, T>[@TraitClause0]}::next<'a, '_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for Chunks<'a, T>[@TraitClause0]}::{vtable}<'a, T>[@TraitClause0] } // Full name: core::slice::{Slice}::chunks diff --git a/charon/tests/ui/issue-323-closure-borrow.out b/charon/tests/ui/issue-323-closure-borrow.out index 680cb5e98..56fcacc86 100644 --- a/charon/tests/ui/issue-323-closure-borrow.out +++ b/charon/tests/ui/issue-323-closure-borrow.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output diff --git a/charon/tests/ui/issue-369-mismatched-genericparams.out b/charon/tests/ui/issue-369-mismatched-genericparams.out index 550a4c703..f8597f608 100644 --- a/charon/tests/ui/issue-369-mismatched-genericparams.out +++ b/charon/tests/ui/issue-369-mismatched-genericparams.out @@ -37,7 +37,7 @@ pub trait Try parent_clause1 : [@TraitClause1]: FromResidual parent_clause2 : [@TraitClause2]: Sized type Residual - non-dyn-compatible + vtable: test_crate::Try::{vtable} } // Full name: test_crate::{impl FromResidual<()> for Option[@TraitClause0]} @@ -59,7 +59,7 @@ where parent_clause1 = {impl FromResidual<()> for Option[@TraitClause0]}[@TraitClause0] parent_clause2 = Sized<()> type Residual = () - non-dyn-compatible + vtable: {impl Try for Option[@TraitClause0]}::{vtable}[@TraitClause0] } diff --git a/charon/tests/ui/issue-372-type-param-out-of-range.out b/charon/tests/ui/issue-372-type-param-out-of-range.out index 74ed84641..ab6f0e8c8 100644 --- a/charon/tests/ui/issue-372-type-param-out-of-range.out +++ b/charon/tests/ui/issue-372-type-param-out-of-range.out @@ -30,7 +30,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -42,7 +42,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.out b/charon/tests/ui/issue-394-rpit-with-lifetime.out index fa6adc83b..10bf2aeaf 100644 --- a/charon/tests/ui/issue-394-rpit-with-lifetime.out +++ b/charon/tests/ui/issue-394-rpit-with-lifetime.out @@ -30,7 +30,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -42,7 +42,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::option::Option diff --git a/charon/tests/ui/issue-395-failed-to-normalize.out b/charon/tests/ui/issue-395-failed-to-normalize.out index d09116703..d6d50f21a 100644 --- a/charon/tests/ui/issue-395-failed-to-normalize.out +++ b/charon/tests/ui/issue-395-failed-to-normalize.out @@ -126,7 +126,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::iter::traits::accum::Sum @@ -174,7 +174,7 @@ where type Item type IntoIter fn into_iter = into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -226,7 +226,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -239,7 +239,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } // Full name: core::iter::traits::iterator::Iterator::next @@ -294,7 +294,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -306,7 +306,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -373,7 +373,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: test_crate::Trait @@ -382,7 +382,7 @@ pub trait Trait parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized type AssocType - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::Alias diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 507ec5f94..eda42f771 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -30,7 +30,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -42,7 +42,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } pub fn core::array::{Array}::map(@1: Array, @2: F) -> Array @@ -246,7 +246,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::ops::range::Range @@ -275,7 +275,7 @@ where parent_clause1 = @TraitClause0 type Item = A fn next<'_0> = {impl Iterator for Range[@TraitClause0]}::next<'_0_0, A>[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl Iterator for Range[@TraitClause0]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::accum::Sum @@ -323,7 +323,7 @@ where type Item type IntoIter fn into_iter = core::iter::traits::collect::IntoIterator::into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -369,7 +369,7 @@ where type Item = @TraitClause1::Item type IntoIter = I fn into_iter = {impl IntoIterator for I}::into_iter[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl IntoIterator for I}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::collect::Extend @@ -396,7 +396,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -409,7 +409,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } #[lang_item("next")] @@ -521,7 +521,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::panicking::AssertKind diff --git a/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out b/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out index 59a0c27c2..51fd22559 100644 --- a/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out +++ b/charon/tests/ui/issue-93-recursive-traits-with-assoc-types.out @@ -19,7 +19,7 @@ pub trait Trait1 parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Trait2 type T - non-dyn-compatible + vtable: test_crate::Trait1::{vtable} } // Full name: test_crate::Trait2 @@ -29,7 +29,7 @@ pub trait Trait2 parent_clause1 : [@TraitClause1]: Trait1 parent_clause2 : [@TraitClause2]: Sized type U - non-dyn-compatible + vtable: test_crate::Trait2::{vtable} } diff --git a/charon/tests/ui/issue-94-recursive-trait-defns.out b/charon/tests/ui/issue-94-recursive-trait-defns.out index 7b3e95a61..5a203b78a 100644 --- a/charon/tests/ui/issue-94-recursive-trait-defns.out +++ b/charon/tests/ui/issue-94-recursive-trait-defns.out @@ -55,7 +55,7 @@ pub trait T3 parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: T5 type T - non-dyn-compatible + vtable: test_crate::T3::{vtable} } // Full name: test_crate::T5 @@ -65,7 +65,7 @@ pub trait T5 parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: T4 type T - non-dyn-compatible + vtable: test_crate::T5::{vtable} } // Full name: test_crate::T4 @@ -73,7 +73,7 @@ pub trait T4 { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: T3 - non-dyn-compatible + vtable: test_crate::T4::{vtable} } // Full name: test_crate::T6 diff --git a/charon/tests/ui/iterator.out b/charon/tests/ui/iterator.out index d483620c1..11853ce9b 100644 --- a/charon/tests/ui/iterator.out +++ b/charon/tests/ui/iterator.out @@ -191,7 +191,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -203,7 +203,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::iter::adapters::map::Map @@ -323,7 +323,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::default::Default @@ -424,7 +424,7 @@ where type Item type IntoIter fn into_iter = core::iter::traits::collect::IntoIterator::into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::iterator::Iterator @@ -511,7 +511,7 @@ pub trait Iterator fn is_sorted_by, [@TraitClause1]: Sized, [@TraitClause2]: for<'_0, '_1> FnMut, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = core::iter::traits::iterator::Iterator::is_sorted_by[Self, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn is_sorted_by_key, [@TraitClause1]: Sized, [@TraitClause2]: Sized, [@TraitClause3]: FnMut, [@TraitClause4]: PartialOrd, @TraitClause1_3::parent_clause1::Output = K> = is_sorted_by_key[Self, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn __iterator_get_unchecked<'_0, [@TraitClause0]: TrustedRandomAccessNoCoerce> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[Self, @TraitClause0_0] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -548,7 +548,7 @@ pub trait DoubleEndedIterator fn try_rfold<'_0, B, F, R, [@TraitClause0]: Sized, [@TraitClause1]: Sized, [@TraitClause2]: Sized, [@TraitClause3]: Sized, [@TraitClause4]: FnMut, [@TraitClause5]: Try, @TraitClause1_4::parent_clause1::Output = R, @TraitClause1_5::Output = B> = try_rfold<'_0_0, Self, B, F, R>[Self, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4, @TraitClause0_5] fn rfold, [@TraitClause1]: Sized, [@TraitClause2]: Sized, [@TraitClause3]: FnMut, @TraitClause1_3::parent_clause1::Output = B> = rfold[Self, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3] fn rfind<'_0, P, [@TraitClause0]: Sized

, [@TraitClause1]: Sized, [@TraitClause2]: for<'_0> FnMut, for<'_0> @TraitClause1_2::parent_clause1::Output = bool> = rfind<'_0_0, Self, P>[Self, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::exact_size::ExactSizeIterator @@ -558,7 +558,7 @@ pub trait ExactSizeIterator parent_clause1 : [@TraitClause1]: Iterator fn len<'_0> = len<'_0_0, Self>[Self] fn is_empty<'_0> = is_empty<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } // Full name: core::iter::traits::accum::Sum @@ -1336,7 +1336,7 @@ where fn is_sorted_by, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> FnMut, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = core::array::iter::{impl Iterator for IntoIter[@TraitClause0]}::is_sorted_by[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn is_sorted_by_key, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, [@TraitClause4]: PartialOrd, @TraitClause1_3::parent_clause1::Output = K> = core::array::iter::{impl Iterator for IntoIter[@TraitClause0]}::is_sorted_by_key[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn __iterator_get_unchecked<'_0> = {impl Iterator for IntoIter[@TraitClause0]}::__iterator_get_unchecked<'_0_0, T, const N : usize>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for IntoIter[@TraitClause0]}::{vtable}[@TraitClause0] } // Full name: core::array::iter::{impl IntoIterator for Array}::into_iter @@ -1356,7 +1356,7 @@ where type Item = T type IntoIter = IntoIter[@TraitClause0] fn into_iter = {impl IntoIterator for Array}::into_iter[@TraitClause0] - non-dyn-compatible + vtable: {impl IntoIterator for Array}::{vtable}[@TraitClause0] } // Full name: core::ops::drop::Drop @@ -1563,7 +1563,7 @@ where type Item = @TraitClause1::Item type IntoIter = I fn into_iter = {impl IntoIterator for I}::into_iter[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl IntoIterator for I}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::collect::Extend::extend @@ -3064,7 +3064,7 @@ where fn is_sorted_by, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> FnMut, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn is_sorted_by_key, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut, [@TraitClause4]: PartialOrd, @TraitClause1_3::parent_clause1::Output = K> = core::slice::iter::{impl Iterator for Iter<'a, T>[@TraitClause0]}::is_sorted_by_key<'a, T, F, K>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn __iterator_get_unchecked<'_0> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for Iter<'a, T>[@TraitClause0]}::{vtable}<'a, T>[@TraitClause0] } // Full name: core::slice::iter::Chunks @@ -3772,7 +3772,7 @@ where fn is_sorted_by, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> FnMut)), &'_0_1 (&'a (Slice)))>, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = core::slice::iter::{impl Iterator for Chunks<'a, T>[@TraitClause0]}::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn is_sorted_by_key, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut))>, [@TraitClause4]: PartialOrd, @TraitClause1_3::parent_clause1::Output = K> = core::slice::iter::{impl Iterator for Chunks<'a, T>[@TraitClause0]}::is_sorted_by_key<'a, T, F, K>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn __iterator_get_unchecked<'_0> = {impl Iterator for Chunks<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for Chunks<'a, T>[@TraitClause0]}::{vtable}<'a, T>[@TraitClause0] } // Full name: core::slice::iter::ChunksExact @@ -4480,7 +4480,7 @@ where fn is_sorted_by, [@TraitClause1]: Sized[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> FnMut)), &'_0_1 (&'a (Slice)))>, for<'_0, '_1> @TraitClause1_2::parent_clause1::Output = bool> = core::slice::iter::{impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2] fn is_sorted_by_key, [@TraitClause1]: Sized, [@TraitClause2]: Sized[@TraitClause0]>, [@TraitClause3]: FnMut))>, [@TraitClause4]: PartialOrd, @TraitClause1_3::parent_clause1::Output = K> = core::slice::iter::{impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::is_sorted_by_key<'a, T, F, K>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4] fn __iterator_get_unchecked<'_0> = {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for ChunksExact<'a, T>[@TraitClause0]}::{vtable}<'a, T>[@TraitClause0] } // Full name: core::slice::{Slice}::iter diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index 09a383c3c..058d7c675 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -297,7 +297,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::ops::range::Range @@ -326,7 +326,7 @@ where parent_clause1 = @TraitClause0 type Item = A fn next<'_0> = {impl Iterator for Range[@TraitClause0]}::next<'_0_0, A>[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl Iterator for Range[@TraitClause0]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::accum::Sum @@ -374,7 +374,7 @@ where type Item type IntoIter fn into_iter = core::iter::traits::collect::IntoIterator::into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -420,7 +420,7 @@ where type Item = @TraitClause1::Item type IntoIter = I fn into_iter = {impl IntoIterator for I}::into_iter[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl IntoIterator for I}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::collect::Extend @@ -447,7 +447,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -460,7 +460,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } #[lang_item("next")] @@ -514,7 +514,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -526,7 +526,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -548,7 +548,7 @@ pub trait Index parent_clause2 : [@TraitClause2]: MetaSized type Output fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>[Self] - non-dyn-compatible + vtable: core::ops::index::Index::{vtable} } pub fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (@TraitClause0::Output) @@ -563,7 +563,7 @@ pub trait IndexMut parent_clause1 : [@TraitClause1]: Index parent_clause2 : [@TraitClause2]: MetaSized fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx>[Self] - non-dyn-compatible + vtable: core::ops::index::IndexMut::{vtable} } pub fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (@TraitClause0::parent_clause1::Output) @@ -624,7 +624,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::slice::index::private_slice_index::Sealed @@ -655,7 +655,7 @@ pub trait SliceIndex fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut[Self] fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T>[Self] fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T>[Self] - non-dyn-compatible + vtable: core::slice::index::SliceIndex::{vtable} } pub fn core::slice::index::SliceIndex::get<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> Option<&'_0 (@TraitClause0::Output)>[Sized<&'_0 (@TraitClause0::Output)>] @@ -728,7 +728,7 @@ where fn get_unchecked_mut = {impl SliceIndex> for usize}::get_unchecked_mut[@TraitClause0] fn index<'_0> = {impl SliceIndex> for usize}::index<'_0_0, T>[@TraitClause0] fn index_mut<'_0> = {impl SliceIndex> for usize}::index_mut<'_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl SliceIndex> for usize}::{vtable}[@TraitClause0] } // Full name: alloc::alloc::Global @@ -768,7 +768,7 @@ where parent_clause2 = @TraitClause3::parent_clause3 type Output = @TraitClause3::Output fn index<'_0> = {impl Index for Vec[@TraitClause0, @TraitClause2]}::index<'_0_0, T, I, A>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] - non-dyn-compatible + vtable: {impl Index for Vec[@TraitClause0, @TraitClause2]}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] } // Full name: alloc::vec::{impl IndexMut for Vec[@TraitClause0, @TraitClause2]}::index_mut @@ -791,7 +791,7 @@ where parent_clause1 = {impl Index for Vec[@TraitClause0, @TraitClause2]}[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] parent_clause2 = @TraitClause1::parent_clause0 fn index_mut<'_0> = {impl IndexMut for Vec[@TraitClause0, @TraitClause2]}::index_mut<'_0_0, T, I, A>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] - non-dyn-compatible + vtable: {impl IndexMut for Vec[@TraitClause0, @TraitClause2]}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] } // Full name: test_crate::test_loop1 diff --git a/charon/tests/ui/ml-name-matcher-tests.out b/charon/tests/ui/ml-name-matcher-tests.out index 171ee4d09..2c2e015c8 100644 --- a/charon/tests/ui/ml-name-matcher-tests.out +++ b/charon/tests/ui/ml-name-matcher-tests.out @@ -21,7 +21,7 @@ pub trait Index parent_clause2 : [@TraitClause2]: MetaSized type Output fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>[Self] - non-dyn-compatible + vtable: core::ops::index::Index::{vtable} } pub fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (@TraitClause0::Output) @@ -74,7 +74,7 @@ pub trait SliceIndex fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut[Self] fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T>[Self] fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T>[Self] - non-dyn-compatible + vtable: core::slice::index::SliceIndex::{vtable} } // Full name: core::slice::index::{impl Index for Slice}::index @@ -96,7 +96,7 @@ where parent_clause2 = @TraitClause2::parent_clause3 type Output = @TraitClause2::Output fn index<'_0> = {impl Index for Slice}::index<'_0_0, T, I>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl Index for Slice}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::slice::index::private_slice_index::{impl Sealed for RangeFrom[Sized]} @@ -175,7 +175,7 @@ where fn get_unchecked_mut = {impl SliceIndex> for RangeFrom[Sized]}::get_unchecked_mut[@TraitClause0] fn index<'_0> = {impl SliceIndex> for RangeFrom[Sized]}::index<'_0_0, T>[@TraitClause0] fn index_mut<'_0> = {impl SliceIndex> for RangeFrom[Sized]}::index_mut<'_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl SliceIndex> for RangeFrom[Sized]}::{vtable}[@TraitClause0] } // Full name: alloc::alloc::Global diff --git a/charon/tests/ui/monomorphization/closure-fn.out b/charon/tests/ui/monomorphization/closure-fn.out index 1f23a513d..5ac030516 100644 --- a/charon/tests/ui/monomorphization/closure-fn.out +++ b/charon/tests/ui/monomorphization/closure-fn.out @@ -58,7 +58,7 @@ pub trait FnOnce::, (u8, u8)> parent_clause1 : [@TraitClause1]: Sized::<(u8, u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8, u8)> fn call_once = core::ops::function::FnOnce::call_once::, (u8, u8)> - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable}::, (u8, u8)> } // Full name: core::ops::function::FnMut::, (u8, u8)> @@ -70,7 +70,7 @@ pub trait FnMut::, (u8, u8)> parent_clause2 : [@TraitClause2]: Sized::<(u8, u8)> parent_clause3 : [@TraitClause3]: Tuple::<(u8, u8)> fn call_mut<'_0> = core::ops::function::FnMut::call_mut::, (u8, u8)><'_0_0> - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable}::, (u8, u8)> } // Full name: core::ops::function::Fn::, (u8, u8)> @@ -82,7 +82,7 @@ pub trait Fn::, (u8, u8)> parent_clause2 : [@TraitClause2]: Sized::<(u8, u8)> parent_clause3 : [@TraitClause3]: Tuple::<(u8, u8)> fn call<'_0> = core::ops::function::Fn::call::, (u8, u8)><'_0_0> - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable}::, (u8, u8)> } pub fn core::ops::function::Fn::call<'_0>(@1: &'_0 (closure<'_, '_>), @2: (u8, u8)) -> u8 diff --git a/charon/tests/ui/monomorphization/closure-fnonce.out b/charon/tests/ui/monomorphization/closure-fnonce.out index 6e81c6444..4187da696 100644 --- a/charon/tests/ui/monomorphization/closure-fnonce.out +++ b/charon/tests/ui/monomorphization/closure-fnonce.out @@ -74,7 +74,7 @@ pub trait FnOnce:: parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> fn call_once = core::ops::function::FnOnce::call_once:: - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable}:: } pub fn core::ops::function::FnOnce::call_once(@1: closure, @2: (u8)) -> u8 diff --git a/charon/tests/ui/monomorphization/closures.out b/charon/tests/ui/monomorphization/closures.out index 9bca2fa34..517a55a57 100644 --- a/charon/tests/ui/monomorphization/closures.out +++ b/charon/tests/ui/monomorphization/closures.out @@ -127,7 +127,7 @@ pub trait FnOnce::, (u8)> parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> fn call_once = core::ops::function::FnOnce::call_once::, (u8)> - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable}::, (u8)> } // Full name: core::ops::function::FnMut::, (u8)> @@ -139,7 +139,7 @@ pub trait FnMut::, (u8)> parent_clause2 : [@TraitClause2]: Sized::<(u8)> parent_clause3 : [@TraitClause3]: Tuple::<(u8)> fn call_mut<'_0> = core::ops::function::FnMut::call_mut::, (u8)><'_0_0> - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable}::, (u8)> } // Full name: core::ops::function::Fn::, (u8)> @@ -151,7 +151,7 @@ pub trait Fn::, (u8)> parent_clause2 : [@TraitClause2]: Sized::<(u8)> parent_clause3 : [@TraitClause3]: Tuple::<(u8)> fn call<'_0> = core::ops::function::Fn::call::, (u8)><'_0_0> - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable}::, (u8)> } pub fn core::ops::function::Fn::call<'_0>(@1: &'_0 (test_crate::main::closure<'_>), @2: (u8)) -> u8 @@ -166,7 +166,7 @@ pub trait FnOnce::, (u8)> parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> fn call_once = core::ops::function::FnOnce::call_once::, (u8)> - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable}::, (u8)> } // Full name: core::ops::function::FnMut::, (u8)> @@ -178,7 +178,7 @@ pub trait FnMut::, (u8)> parent_clause2 : [@TraitClause2]: Sized::<(u8)> parent_clause3 : [@TraitClause3]: Tuple::<(u8)> fn call_mut<'_0> = core::ops::function::FnMut::call_mut::, (u8)><'_0_0> - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable}::, (u8)> } pub fn core::ops::function::FnMut::call_mut<'_0>(@1: &'_0 mut (test_crate::main::closure#1<'_>), @2: (u8)) -> u8 @@ -197,7 +197,7 @@ pub trait FnOnce:: parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> fn call_once = core::ops::function::FnOnce::call_once:: - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable}:: } pub fn core::ops::function::FnOnce::call_once(@1: test_crate::main::closure#2, @2: (u8)) -> u8 diff --git a/charon/tests/ui/monomorphization/dyn-trait.out b/charon/tests/ui/monomorphization/dyn-trait.out index b5c91c4bb..0d96eb9bb 100644 --- a/charon/tests/ui/monomorphization/dyn-trait.out +++ b/charon/tests/ui/monomorphization/dyn-trait.out @@ -97,7 +97,7 @@ note: the error occurred when translating `core::fmt::Display::{vtable}:: foo::<'_0_0>, (&'_ (u32))> parent_clause1 : [@TraitClause1]: Sized::<(&'_ (u32))> parent_clause2 : [@TraitClause2]: Tuple::<(&'_ (u32))> fn call_once = call_once:: foo::<'_0_0>, (&'_ (u32))> - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable}:: foo::<'_0_0>, (&'_ (u32))><()> } // Full name: core::ops::function::FnMut:: foo::<'_0_0>, (&'_ (u32))> @@ -123,7 +123,7 @@ pub trait FnMut:: foo::<'_0_0>, (&'_ (u32))> parent_clause2 : [@TraitClause2]: Sized::<(&'_ (u32))> parent_clause3 : [@TraitClause3]: Tuple::<(&'_ (u32))> fn call_mut<'_0> = call_mut:: foo::<'_0_0>, (&'_ (u32))><'_0_0> - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable}:: foo::<'_0_0>, (&'_ (u32))><()> } // Full name: core::ops::function::Fn:: foo::<'_0_0>, (&'_ (u32))> @@ -135,7 +135,7 @@ pub trait Fn:: foo::<'_0_0>, (&'_ (u32))> parent_clause2 : [@TraitClause2]: Sized::<(&'_ (u32))> parent_clause3 : [@TraitClause3]: Tuple::<(&'_ (u32))> fn call<'_0> = call:: foo::<'_0_0>, (&'_ (u32))><'_0_0> - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable}:: foo::<'_0_0>, (&'_ (u32))><()> } // Full name: core::ops::function::Fn::call diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index 0158e6fb7..a93cf75a0 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -19,7 +19,7 @@ pub trait Deref parent_clause0 : [@TraitClause0]: MetaSized type Target fn deref<'_0> = core::ops::deref::Deref::deref<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::ops::deref::Deref::{vtable} } #[lang_item("deref_method")] @@ -33,7 +33,7 @@ pub trait DerefMut { parent_clause0 : [@TraitClause0]: Deref fn deref_mut<'_0> = core::ops::deref::DerefMut::deref_mut<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::ops::deref::DerefMut::{vtable} } #[lang_item("deref_mut_method")] @@ -90,7 +90,7 @@ where parent_clause0 = @TraitClause0 type Target = T fn deref<'_0> = {impl Deref for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::deref<'_0_0, T, A>[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl Deref for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: alloc::boxed::{impl DerefMut for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::deref_mut @@ -107,7 +107,7 @@ where { parent_clause0 = {impl Deref for alloc::boxed::Box[@TraitClause0, @TraitClause1]}[@TraitClause0, @TraitClause1] fn deref_mut<'_0> = {impl DerefMut for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::deref_mut<'_0_0, T, A>[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl DerefMut for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: test_crate::Pair diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index 66f096799..4f5f8107a 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -118,7 +118,7 @@ pub trait BuildHasher parent_clause2 : [@TraitClause2]: Hasher type Hasher fn build_hasher<'_0> = core::hash::BuildHasher::build_hasher<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::hash::BuildHasher::{vtable} } pub fn core::hash::BuildHasher::build_hasher<'_0, Self>(@1: &'_0 (Self)) -> @TraitClause0::Hasher @@ -146,7 +146,7 @@ pub trait Index parent_clause2 : [@TraitClause2]: MetaSized type Output fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>[Self] - non-dyn-compatible + vtable: core::ops::index::Index::{vtable} } pub fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (@TraitClause0::Output) @@ -229,7 +229,7 @@ where parent_clause2 = @TraitClause2::parent_clause0 type Output = V fn index<'_0> = {impl Index<&'_0 (Q)> for HashMap[@TraitClause0, @TraitClause2, @TraitClause3]}::index<'_0, '_0_0, K, Q, V, S>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause4, @TraitClause5, @TraitClause6, @TraitClause7, @TraitClause8, @TraitClause9] - non-dyn-compatible + vtable: {impl Index<&'_0 (Q)> for HashMap[@TraitClause0, @TraitClause2, @TraitClause3]}::{vtable}<'_0, K, Q, V, S>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause4, @TraitClause5, @TraitClause6, @TraitClause7, @TraitClause8, @TraitClause9] } // Full name: std::hash::random::RandomState @@ -262,7 +262,7 @@ impl BuildHasher for RandomState { parent_clause2 = {impl Hasher for DefaultHasher} type Hasher = DefaultHasher fn build_hasher<'_0> = {impl BuildHasher for RandomState}::build_hasher<'_0_0> - non-dyn-compatible + vtable: {impl BuildHasher for RandomState}::{vtable} } // Full name: test_crate::get_or_insert diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index c252ca8f1..fe940d74c 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/charon/tests/ui/predicates-on-late-bound-vars.out @@ -172,7 +172,7 @@ trait Foo parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized type S - non-dyn-compatible + vtable: test_crate::Foo::{vtable} } // Full name: test_crate::f diff --git a/charon/tests/ui/ptr_no_provenance.out b/charon/tests/ui/ptr_no_provenance.out index 64295cf23..429bc6a34 100644 --- a/charon/tests/ui/ptr_no_provenance.out +++ b/charon/tests/ui/ptr_no_provenance.out @@ -258,7 +258,7 @@ pub trait Pointee parent_clause7 : [@TraitClause7]: Unpin parent_clause8 : [@TraitClause8]: Freeze type Metadata - non-dyn-compatible + vtable: core::ptr::metadata::Pointee::{vtable} } // Full name: core::ptr::metadata::Thin @@ -267,7 +267,7 @@ where Self::parent_clause0::Metadata = (), { parent_clause0 : [@TraitClause0]: Pointee - non-dyn-compatible + vtable: core::ptr::metadata::Thin::{vtable}<()> } // Full name: core::ptr::metadata::Thin::{impl Thin for Self} diff --git a/charon/tests/ui/quantified-clause.out b/charon/tests/ui/quantified-clause.out index ef98ef194..8bcdfe3f9 100644 --- a/charon/tests/ui/quantified-clause.out +++ b/charon/tests/ui/quantified-clause.out @@ -126,7 +126,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::iter::traits::accum::Sum @@ -174,7 +174,7 @@ where type Item type IntoIter fn into_iter = into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -226,7 +226,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -239,7 +239,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } // Full name: core::iter::traits::iterator::Iterator::next @@ -308,7 +308,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -320,7 +320,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -387,7 +387,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::result::Result diff --git a/charon/tests/ui/region-inference-vars.out b/charon/tests/ui/region-inference-vars.out index fd1103a05..fc8a6dfc3 100644 --- a/charon/tests/ui/region-inference-vars.out +++ b/charon/tests/ui/region-inference-vars.out @@ -31,7 +31,7 @@ pub trait MyTryFrom parent_clause2 : [@TraitClause2]: Sized type Error fn from<[@TraitClause0]: Sized> = test_crate::MyTryFrom::from[Self, @TraitClause0_0] - non-dyn-compatible + vtable: test_crate::MyTryFrom::{vtable} } pub fn test_crate::MyTryFrom::from(@1: T) -> Result[@TraitClause1, @TraitClause0::parent_clause2] @@ -60,7 +60,7 @@ impl<'_0> MyTryFrom<&'_0 (bool)> for bool { parent_clause2 = Sized<()> type Error = () fn from = {impl MyTryFrom<&'_0 (bool)> for bool}::from<'_0> - non-dyn-compatible + vtable: {impl MyTryFrom<&'_0 (bool)> for bool}::{vtable}<'_0> } diff --git a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out index 756d9d808..a9d7dabf8 100644 --- a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out +++ b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out @@ -43,7 +43,7 @@ pub trait FnOnce parent_clause2 : [@TraitClause2]: Tuple parent_clause3 : [@TraitClause3]: Sized fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -55,7 +55,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args, Self_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -67,7 +67,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args, Self_Clause1_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args, Clause0_Clause1_Clause1_Output>(@1: &'_0 (Self), @2: Args) -> Clause0_Clause1_Clause1_Output @@ -87,7 +87,7 @@ pub trait PrimeField { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::PrimeField::{vtable} } // Full name: test_crate::SqrtTables diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index 0ae79b852..7a8ed7288 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -67,7 +67,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -79,7 +79,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -91,7 +91,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out index 6c6732c89..56c1071e0 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty-nested.out @@ -17,7 +17,7 @@ trait Trait { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::IntoIterator @@ -26,7 +26,7 @@ trait IntoIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Trait - non-dyn-compatible + vtable: test_crate::IntoIterator::{vtable} } // Full name: test_crate::IntoIntoIterator @@ -35,7 +35,7 @@ trait IntoIntoIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: IntoIterator - non-dyn-compatible + vtable: test_crate::IntoIntoIterator::{vtable} } // Full name: test_crate::foo diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out index e34c3d66b..394812fee 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.2.out @@ -17,7 +17,7 @@ trait Trait { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::IntoIterator @@ -26,7 +26,7 @@ trait IntoIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Trait - non-dyn-compatible + vtable: test_crate::IntoIterator::{vtable} } // Full name: test_crate::foo diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out index 495b3e1f8..d137bc3b4 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out @@ -31,7 +31,7 @@ trait Trait { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::takes_trait @@ -55,7 +55,7 @@ trait IntoIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Trait - non-dyn-compatible + vtable: test_crate::IntoIterator::{vtable} } // Full name: test_crate::collect diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out index d9c54339d..920370008 100644 --- a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out +++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out @@ -17,14 +17,14 @@ pub trait HasOutput { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::HasOutput::{vtable} } // Full name: test_crate::{impl HasOutput<()> for ()} impl HasOutput<()> for () { parent_clause0 = MetaSized<()> parent_clause1 = Sized<()> - non-dyn-compatible + vtable: {impl HasOutput<()> for ()}::{vtable} } // Full name: test_crate::HasOutput2 @@ -32,14 +32,14 @@ pub trait HasOutput2 { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: HasOutput - non-dyn-compatible + vtable: test_crate::HasOutput2::{vtable} } // Full name: test_crate::{impl HasOutput2<()> for ()} impl HasOutput2<()> for () { parent_clause0 = MetaSized<()> parent_clause1 = {impl HasOutput<()> for ()} - non-dyn-compatible + vtable: {impl HasOutput2<()> for ()}::{vtable} } // Full name: test_crate::Wrapper @@ -58,7 +58,7 @@ where { parent_clause0 = MetaSized[@TraitClause0]> parent_clause1 = @TraitClause1::parent_clause1 - non-dyn-compatible + vtable: {impl HasOutput for Wrapper[@TraitClause0]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: test_crate::{impl HasOutput2 for Wrapper[@TraitClause0]} @@ -69,7 +69,7 @@ where { parent_clause0 = MetaSized[@TraitClause0]> parent_clause1 = {impl HasOutput for Wrapper[@TraitClause0]}[@TraitClause0, @TraitClause1::parent_clause1] - non-dyn-compatible + vtable: {impl HasOutput2 for Wrapper[@TraitClause0]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: test_crate::take diff --git a/charon/tests/ui/simple/assoc-type-with-fn-bound.out b/charon/tests/ui/simple/assoc-type-with-fn-bound.out index 81eeaa05f..ce386396f 100644 --- a/charon/tests/ui/simple/assoc-type-with-fn-bound.out +++ b/charon/tests/ui/simple/assoc-type-with-fn-bound.out @@ -29,7 +29,7 @@ pub trait FnOnce parent_clause2 : [@TraitClause2]: Tuple parent_clause3 : [@TraitClause3]: Sized fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -41,7 +41,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args, Self_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -53,7 +53,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args, Self_Clause1_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args, Clause0_Clause1_Clause1_Output>(@1: &'_0 (Self), @2: Args) -> Clause0_Clause1_Clause1_Output @@ -77,7 +77,7 @@ pub trait Trait parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Fn fn call<'_0> = test_crate::Trait::call<'_0_0, Self, Self_Foo>[Self] - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } pub fn test_crate::Trait::call<'_0, Self, Clause0_Foo>(@1: &'_0 (Self)) @@ -116,7 +116,7 @@ where parent_clause1 = @TraitClause1 parent_clause2 = @TraitClause0 fn call<'_0> = {impl Trait for F}::call<'_0_0, F>[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl Trait for F}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: test_crate::use_foo diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out index 0a8a70f63..542842267 100644 --- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out @@ -30,14 +30,14 @@ pub trait Trait { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::{impl Trait<()> for ()} impl Trait<()> for () { parent_clause0 = MetaSized<()> parent_clause1 = Sized<()> - non-dyn-compatible + vtable: {impl Trait<()> for ()}::{vtable} } // Full name: test_crate::HashMap diff --git a/charon/tests/ui/simple/closure-capture-ref-by-move.out b/charon/tests/ui/simple/closure-capture-ref-by-move.out index 2c32812f9..771331da1 100644 --- a/charon/tests/ui/simple/closure-capture-ref-by-move.out +++ b/charon/tests/ui/simple/closure-capture-ref-by-move.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output diff --git a/charon/tests/ui/simple/closure-fn.out b/charon/tests/ui/simple/closure-fn.out index 3e61c9b3f..edd1cbb44 100644 --- a/charon/tests/ui/simple/closure-fn.out +++ b/charon/tests/ui/simple/closure-fn.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -68,7 +68,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/closure-fnmut.out b/charon/tests/ui/simple/closure-fnmut.out index 48f34d0c0..e1bdded29 100644 --- a/charon/tests/ui/simple/closure-fnmut.out +++ b/charon/tests/ui/simple/closure-fnmut.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output diff --git a/charon/tests/ui/simple/closure-fnonce.out b/charon/tests/ui/simple/closure-fnonce.out index 37b608f4f..a4892b9e2 100644 --- a/charon/tests/ui/simple/closure-fnonce.out +++ b/charon/tests/ui/simple/closure-fnonce.out @@ -48,7 +48,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output diff --git a/charon/tests/ui/simple/closure-inside-impl.out b/charon/tests/ui/simple/closure-inside-impl.out index ff8dda662..657d18778 100644 --- a/charon/tests/ui/simple/closure-inside-impl.out +++ b/charon/tests/ui/simple/closure-inside-impl.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -68,7 +68,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out index ca8ebd9d1..8656a284b 100644 --- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out +++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -68,7 +68,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/closure-with-drops.out b/charon/tests/ui/simple/closure-with-drops.out index d1dcffc47..4e0e13c03 100644 --- a/charon/tests/ui/simple/closure-with-drops.out +++ b/charon/tests/ui/simple/closure-with-drops.out @@ -52,7 +52,7 @@ pub trait FnOnce parent_clause6 : [@TraitClause6]: Drop type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -66,7 +66,7 @@ pub trait FnMut parent_clause4 : [@TraitClause4]: Drop parent_clause5 : [@TraitClause5]: Drop fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -80,7 +80,7 @@ pub trait Fn parent_clause4 : [@TraitClause4]: Drop parent_clause5 : [@TraitClause5]: Drop fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out index 057e558a4..964dd7a06 100644 --- a/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out +++ b/charon/tests/ui/simple/default-method-with-clause-and-marker-trait.out @@ -4,7 +4,7 @@ trait HasAssoc { type Assoc - non-dyn-compatible + vtable: test_crate::HasAssoc::{vtable} } // Full name: test_crate::Trait diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index 83b69cb44..519aa3648 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,16 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), + method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable} [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output>), } // Full name: core::ops::function::Fn @@ -68,7 +77,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out index 924a5d6c2..677d275bd 100644 --- a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out @@ -1,92 +1,41 @@ -# Final LLBC before serialization: - -// Full name: core::marker::MetaSized -#[lang_item("meta_sized")] -pub trait MetaSized - -// Full name: core::marker::Sized -#[lang_item("sized")] -pub trait Sized -{ - parent_clause0 : [@TraitClause0]: MetaSized - non-dyn-compatible -} - -// Full name: core::clone::Clone -#[lang_item("clone")] -pub trait Clone -{ - parent_clause0 : [@TraitClause0]: Sized - fn clone<'_0> = clone<'_0_0, Self>[Self] - non-dyn-compatible -} - -// Full name: core::clone::Clone::clone -#[lang_item("clone_fn")] -pub fn clone<'_0, Self>(@1: &'_0 (Self)) -> Self -where - [@TraitClause0]: Clone, - -// Full name: core::marker::Copy -#[lang_item("copy")] -pub trait Copy -{ - parent_clause0 : [@TraitClause0]: MetaSized - parent_clause1 : [@TraitClause1]: Clone - non-dyn-compatible -} - -// Full name: core::marker::Destruct -#[lang_item("destruct")] -pub trait Destruct -{ - parent_clause0 : [@TraitClause0]: MetaSized - vtable: core::marker::Destruct::{vtable} -} - -// Full name: test_crate::Trait -trait Trait -{ - parent_clause0 : [@TraitClause0]: MetaSized - fn method, [@TraitClause1]: Copy> = test_crate::Trait::method[Self, @TraitClause0_0, @TraitClause0_1] - non-dyn-compatible -} - -fn test_crate::Trait::method() -where - [@TraitClause0]: Trait, - [@TraitClause1]: Sized, - [@TraitClause2]: Copy, - -// Full name: test_crate::{impl Trait for ()}::method -fn {impl Trait for ()}::method() -where - [@TraitClause0]: Sized, - [@TraitClause1]: Clone, -{ - let @0: (); // return - - @0 := () - @0 := () - return -} - -// Full name: test_crate::{impl Trait for ()} -impl Trait for () { - parent_clause0 = MetaSized<()> - fn method, [@TraitClause1]: Clone> = {impl Trait for ()}::method[@TraitClause0_0, @TraitClause0_1] - non-dyn-compatible -} - -// Full name: test_crate::main -fn main() -{ - let @0: (); // return - - @0 := {impl Trait for ()}::method<()>[Sized<()>, Copy<()>]() - @0 := () - return -} - - - +disabled backtrace +warning[E9999]: Could not find a clause for `Binder { value: , bound_vars: [] }` in the current context: `Unimplemented` + --> tests/ui/simple/fewer-clauses-in-method-impl.rs:8:5 + | +8 | fn method() {} + | ^^^^^^^^^^^^^^^^^^^^^ + | + = note: ⚠️ This is a bug in Hax's frontend. + Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! + +warning: 1 warning emitted + +error: Found inconsistent generics after transformations: + Mismatched builtin trait parent clauses: + target: Clone + expected: [[@TraitClause0]: Sized] + got: [MetaSized<()>, Clone<()>] + Visitor stack: + charon_lib::ast::types::TraitRef + charon_lib::ids::vector::Vector + charon_lib::ast::types::GenericArgs + alloc::boxed::Box + charon_lib::ast::expressions::FnPtr + charon_lib::ast::gast::FnOperand + charon_lib::ast::gast::Call + charon_lib::ast::llbc_ast::StatementKind + charon_lib::ast::llbc_ast::Statement + alloc::vec::Vec + charon_lib::ast::llbc_ast::Block + charon_lib::ast::gast::GExprBody + charon_lib::ast::gast::Body + core::result::Result + charon_lib::ast::gast::FunDecl + Binding stack (depth 1): + 0: + --> tests/ui/simple/fewer-clauses-in-method-impl.rs:12:5 + | +12 | <() as Trait>::method::<()>() + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +ERROR Charon failed to translate this code (1 errors) diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs b/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs index cbd9fafe6..b35a5e923 100644 --- a/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs @@ -1,3 +1,4 @@ +//@ known-failure //@ charon-args=--remove-associated-types=* trait Trait { fn method(); diff --git a/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out b/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out index 4899641bc..1cae97af2 100644 --- a/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out +++ b/charon/tests/ui/simple/generic-impl-with-defaulted-method-with-clause-with-assoc-ty.out @@ -27,7 +27,7 @@ trait HasType { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::HasType::{vtable} } // Full name: test_crate::HasMethod diff --git a/charon/tests/ui/simple/mem-discriminant-from-derive.out b/charon/tests/ui/simple/mem-discriminant-from-derive.out index b8a4944d7..64f25ab98 100644 --- a/charon/tests/ui/simple/mem-discriminant-from-derive.out +++ b/charon/tests/ui/simple/mem-discriminant-from-derive.out @@ -169,7 +169,7 @@ pub trait DiscriminantKind parent_clause9 : [@TraitClause9]: Sync parent_clause10 : [@TraitClause10]: Unpin type Discriminant - non-dyn-compatible + vtable: core::marker::DiscriminantKind::{vtable} } // Full name: core::intrinsics::discriminant_value diff --git a/charon/tests/ui/simple/method-with-assoc-type-constraint.out b/charon/tests/ui/simple/method-with-assoc-type-constraint.out index a3c7d9793..de0725d0b 100644 --- a/charon/tests/ui/simple/method-with-assoc-type-constraint.out +++ b/charon/tests/ui/simple/method-with-assoc-type-constraint.out @@ -31,7 +31,7 @@ pub trait IntoIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::IntoIterator::{vtable} } // Full name: test_crate::FromIterator diff --git a/charon/tests/ui/simple/multiple-promoteds.out b/charon/tests/ui/simple/multiple-promoteds.out index 897b19f7d..f2acf9271 100644 --- a/charon/tests/ui/simple/multiple-promoteds.out +++ b/charon/tests/ui/simple/multiple-promoteds.out @@ -21,7 +21,7 @@ pub trait Add parent_clause2 : [@TraitClause2]: Sized type Output fn add = core::ops::arith::Add::add[Self] - non-dyn-compatible + vtable: core::ops::arith::Add::{vtable} } // Full name: core::ops::arith::{impl Add<&'_0 (u32)> for &'_1 (u32)}::add @@ -34,7 +34,7 @@ impl<'_0, '_1> Add<&'_0 (u32)> for &'_1 (u32) { parent_clause2 = Sized type Output = u32 fn add = {impl Add<&'_0 (u32)> for &'_1 (u32)}::add<'_0, '_1> - non-dyn-compatible + vtable: {impl Add<&'_0 (u32)> for &'_1 (u32)}::{vtable}<'_0, '_1> } #[lang_item("add")] diff --git a/charon/tests/ui/simple/nested-closure-trait-ref.out b/charon/tests/ui/simple/nested-closure-trait-ref.out index a020c2df0..2e16f573a 100644 --- a/charon/tests/ui/simple/nested-closure-trait-ref.out +++ b/charon/tests/ui/simple/nested-closure-trait-ref.out @@ -67,7 +67,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -79,7 +79,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -91,7 +91,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/nested-closure.out b/charon/tests/ui/simple/nested-closure.out index 7f3f5515d..91f00d841 100644 --- a/charon/tests/ui/simple/nested-closure.out +++ b/charon/tests/ui/simple/nested-closure.out @@ -67,7 +67,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -79,7 +79,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -91,7 +91,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out index 839f5876b..5db65e5b3 100644 --- a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out @@ -43,7 +43,7 @@ pub trait FnOnce parent_clause2 : [@TraitClause2]: Tuple parent_clause3 : [@TraitClause3]: Sized fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -55,7 +55,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args, Self_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -67,7 +67,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args, Self_Clause1_Clause1_Output>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args, Clause0_Clause1_Clause1_Output>(@1: &'_0 (Self), @2: Args) -> Clause0_Clause1_Clause1_Output diff --git a/charon/tests/ui/simple/pointee_metadata.out b/charon/tests/ui/simple/pointee_metadata.out index 19ce3ad41..878431dcb 100644 --- a/charon/tests/ui/simple/pointee_metadata.out +++ b/charon/tests/ui/simple/pointee_metadata.out @@ -206,7 +206,7 @@ pub trait Pointee parent_clause7 : [@TraitClause7]: Unpin parent_clause8 : [@TraitClause8]: Freeze type Metadata - non-dyn-compatible + vtable: core::ptr::metadata::Pointee::{vtable} } // Full name: core::ptr::const_ptr::{*const T}::to_raw_parts diff --git a/charon/tests/ui/simple/promoted-closure-no-warns.out b/charon/tests/ui/simple/promoted-closure-no-warns.out index e8b65e201..c521d40b7 100644 --- a/charon/tests/ui/simple/promoted-closure-no-warns.out +++ b/charon/tests/ui/simple/promoted-closure-no-warns.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -68,7 +68,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/promoted-closure.out b/charon/tests/ui/simple/promoted-closure.out index e8b65e201..c521d40b7 100644 --- a/charon/tests/ui/simple/promoted-closure.out +++ b/charon/tests/ui/simple/promoted-closure.out @@ -44,7 +44,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -56,7 +56,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -68,7 +68,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output diff --git a/charon/tests/ui/simple/ptr_metadata.out b/charon/tests/ui/simple/ptr_metadata.out index ae6b40dc9..877654e79 100644 --- a/charon/tests/ui/simple/ptr_metadata.out +++ b/charon/tests/ui/simple/ptr_metadata.out @@ -258,7 +258,7 @@ pub trait Pointee parent_clause7 : [@TraitClause7]: Unpin parent_clause8 : [@TraitClause8]: Freeze type Metadata - non-dyn-compatible + vtable: core::ptr::metadata::Pointee::{vtable} } // Full name: core::ptr::metadata::Thin @@ -267,7 +267,7 @@ where Self::parent_clause0::Metadata = (), { parent_clause0 : [@TraitClause0]: Pointee - non-dyn-compatible + vtable: core::ptr::metadata::Thin::{vtable}<()> } // Full name: core::ptr::metadata::Thin::{impl Thin for Self} diff --git a/charon/tests/ui/simple/quantified-trait-type-constraint.out b/charon/tests/ui/simple/quantified-trait-type-constraint.out index 948c2db4f..8d078c0d4 100644 --- a/charon/tests/ui/simple/quantified-trait-type-constraint.out +++ b/charon/tests/ui/simple/quantified-trait-type-constraint.out @@ -17,7 +17,7 @@ trait Trait<'a, Self, Self_Type> { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized - non-dyn-compatible + vtable: test_crate::Trait::{vtable}<'a, Self_Type> } // Full name: test_crate::foo diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index a3222a3ee..572a44534 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -148,7 +148,7 @@ pub trait Index parent_clause2 : [@TraitClause2]: MetaSized type Output fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>[Self] - non-dyn-compatible + vtable: core::ops::index::Index::{vtable} } pub fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (@TraitClause0::Output) @@ -251,7 +251,7 @@ pub trait SliceIndex fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut[Self] fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T>[Self] fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T>[Self] - non-dyn-compatible + vtable: core::slice::index::SliceIndex::{vtable} } pub fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> &'_0 (@TraitClause0::Output) @@ -285,7 +285,7 @@ where parent_clause2 = @TraitClause2::parent_clause3 type Output = @TraitClause2::Output fn index<'_0> = {impl Index for Slice}::index<'_0_0, T, I>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl Index for Slice}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::slice::index::slice_end_index_len_fail @@ -953,7 +953,7 @@ where fn get_unchecked_mut = {impl SliceIndex> for Range[Sized]}::get_unchecked_mut[@TraitClause0] fn index<'_0> = {impl SliceIndex> for Range[Sized]}::index<'_0_0, T>[@TraitClause0] fn index_mut<'_0> = {impl SliceIndex> for Range[Sized]}::index_mut<'_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl SliceIndex> for Range[Sized]}::{vtable}[@TraitClause0] } // Full name: core::slice::index::{impl SliceIndex> for RangeInclusive[Sized]}::get @@ -1466,7 +1466,7 @@ where fn get_unchecked_mut = {impl SliceIndex> for RangeInclusive[Sized]}::get_unchecked_mut[@TraitClause0] fn index<'_0> = {impl SliceIndex> for RangeInclusive[Sized]}::index<'_0_0, T>[@TraitClause0] fn index_mut<'_0> = {impl SliceIndex> for RangeInclusive[Sized]}::index_mut<'_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl SliceIndex> for RangeInclusive[Sized]}::{vtable}[@TraitClause0] } // Full name: test_crate::slice_index_range diff --git a/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out b/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out index a856652c3..e00f1fd97 100644 --- a/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out +++ b/charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out @@ -18,7 +18,7 @@ trait HasAssoc parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized type Assoc - non-dyn-compatible + vtable: test_crate::HasAssoc::{vtable} } // Full name: test_crate::SuperTrait diff --git a/charon/tests/ui/simple/trait-alias.out b/charon/tests/ui/simple/trait-alias.out index 4b6c195fb..3df1ecc94 100644 --- a/charon/tests/ui/simple/trait-alias.out +++ b/charon/tests/ui/simple/trait-alias.out @@ -64,7 +64,7 @@ trait Trait parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: Sized - non-dyn-compatible + vtable: test_crate::Trait::{vtable} } // Full name: test_crate::Struct @@ -95,7 +95,7 @@ where parent_clause0 = MetaSized parent_clause1 = @TraitClause0 parent_clause2 = Sized - non-dyn-compatible + vtable: {impl Trait for Struct}::{vtable}[@TraitClause0] } // Full name: test_crate::Alias diff --git a/charon/tests/ui/slice-index-range.out b/charon/tests/ui/slice-index-range.out index 11de3f1da..1fecedb13 100644 --- a/charon/tests/ui/slice-index-range.out +++ b/charon/tests/ui/slice-index-range.out @@ -13,7 +13,7 @@ pub trait Index parent_clause2 : [@TraitClause2]: MetaSized type Output fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>[Self] - non-dyn-compatible + vtable: core::ops::index::Index::{vtable} } // Full name: core::marker::Sized @@ -43,7 +43,7 @@ where parent_clause2 = @TraitClause2::parent_clause2 type Output = @TraitClause2::Output fn index<'_0> = {impl Index for Array}::index<'_0_0, T, I, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl Index for Array}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::fmt::Arguments @@ -144,7 +144,7 @@ pub trait SliceIndex fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut[Self] fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T>[Self] fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T>[Self] - non-dyn-compatible + vtable: core::slice::index::SliceIndex::{vtable} } pub fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> &'_0 (@TraitClause0::Output) @@ -178,7 +178,7 @@ where parent_clause2 = @TraitClause2::parent_clause3 type Output = @TraitClause2::Output fn index<'_0> = {impl Index for Slice}::index<'_0_0, T, I>[@TraitClause0, @TraitClause1, @TraitClause2] - non-dyn-compatible + vtable: {impl Index for Slice}::{vtable}[@TraitClause0, @TraitClause1, @TraitClause2] } // Full name: core::slice::index::slice_end_index_len_fail @@ -801,7 +801,7 @@ where fn get_unchecked_mut = {impl SliceIndex> for Range[Sized]}::get_unchecked_mut[@TraitClause0] fn index<'_0> = {impl SliceIndex> for Range[Sized]}::index<'_0_0, T>[@TraitClause0] fn index_mut<'_0> = {impl SliceIndex> for Range[Sized]}::index_mut<'_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl SliceIndex> for Range[Sized]}::{vtable}[@TraitClause0] } // Full name: test_crate::main diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 295ef2190..9c657da2a 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -43,7 +43,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = core::ops::function::FnOnce::call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -55,7 +55,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::Fn @@ -67,7 +67,7 @@ pub trait Fn parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::Fn::{vtable} } pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output @@ -893,7 +893,7 @@ pub trait ParentTrait0 type W fn get_name<'_0> = get_name<'_0_0, Self>[Self] fn get_w<'_0> = test_crate::ParentTrait0::get_w<'_0_0, Self>[Self] - non-dyn-compatible + vtable: test_crate::ParentTrait0::{vtable} } // Full name: test_crate::ParentTrait0::get_name @@ -918,7 +918,7 @@ pub trait ChildTrait parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: ParentTrait0 parent_clause2 : [@TraitClause2]: ParentTrait1 - non-dyn-compatible + vtable: test_crate::ChildTrait::{vtable} } // Full name: test_crate::test_child_trait1 @@ -998,7 +998,7 @@ pub trait Iterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized type Item - non-dyn-compatible + vtable: test_crate::Iterator::{vtable} } // Full name: test_crate::IntoIterator @@ -1013,7 +1013,7 @@ where type Item type IntoIter fn into_iter = into_iter[Self] - non-dyn-compatible + vtable: test_crate::IntoIterator::{vtable} } // Full name: test_crate::IntoIterator::into_iter @@ -1045,7 +1045,7 @@ pub trait WithTarget parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized type Target - non-dyn-compatible + vtable: test_crate::WithTarget::{vtable} } // Full name: test_crate::ParentTrait2 @@ -1055,7 +1055,7 @@ pub trait ParentTrait2 parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: WithTarget type U - non-dyn-compatible + vtable: test_crate::ParentTrait2::{vtable} } // Full name: test_crate::ChildTrait2 @@ -1076,7 +1076,7 @@ impl WithTarget for u32 { parent_clause0 = MetaSized parent_clause1 = Sized type Target = u32 - non-dyn-compatible + vtable: {impl WithTarget for u32}::{vtable} } // Full name: test_crate::{impl ParentTrait2 for u32} @@ -1085,7 +1085,7 @@ impl ParentTrait2 for u32 { parent_clause1 = Sized parent_clause2 = {impl WithTarget for u32} type U = u32 - non-dyn-compatible + vtable: {impl ParentTrait2 for u32}::{vtable} } // Full name: test_crate::{impl ChildTrait2 for u32}::convert @@ -1114,7 +1114,7 @@ pub trait CFnOnce parent_clause2 : [@TraitClause2]: Sized type Output fn call_once = test_crate::CFnOnce::call_once[Self] - non-dyn-compatible + vtable: test_crate::CFnOnce::{vtable} } pub fn test_crate::CFnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output @@ -1128,7 +1128,7 @@ pub trait CFnMut parent_clause1 : [@TraitClause1]: CFnOnce parent_clause2 : [@TraitClause2]: Sized fn call_mut<'_0> = test_crate::CFnMut::call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: test_crate::CFnMut::{vtable} } pub fn test_crate::CFnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output @@ -1142,7 +1142,7 @@ pub trait CFn parent_clause1 : [@TraitClause1]: CFnMut parent_clause2 : [@TraitClause2]: Sized fn call<'_0> = test_crate::CFn::call<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: test_crate::CFn::{vtable} } pub fn test_crate::CFn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output @@ -1156,7 +1156,7 @@ pub trait GetTrait parent_clause1 : [@TraitClause1]: Sized type W fn get_w<'_0> = test_crate::GetTrait::get_w<'_0_0, Self>[Self] - non-dyn-compatible + vtable: test_crate::GetTrait::{vtable} } pub fn test_crate::GetTrait::get_w<'_0, Self>(@1: &'_0 (Self)) -> @TraitClause0::W @@ -1321,7 +1321,7 @@ trait RecursiveImpl parent_clause1 : [@TraitClause1]: Sized parent_clause2 : [@TraitClause2]: RecursiveImpl type Item - non-dyn-compatible + vtable: test_crate::RecursiveImpl::{vtable} } // Full name: test_crate::{impl RecursiveImpl for ()} @@ -1330,7 +1330,7 @@ impl RecursiveImpl for () { parent_clause1 = Sized<()> parent_clause2 = {impl RecursiveImpl for ()} type Item = () - non-dyn-compatible + vtable: {impl RecursiveImpl for ()}::{vtable} } // Full name: test_crate::flabada @@ -1377,7 +1377,7 @@ trait SliceIndex parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Sized type Output - non-dyn-compatible + vtable: test_crate::assoc_ty_trait_ref::SliceIndex::{vtable} } // Full name: test_crate::assoc_ty_trait_ref::index diff --git a/charon/tests/ui/traits_special.out b/charon/tests/ui/traits_special.out index 8ef91b9e6..b57479284 100644 --- a/charon/tests/ui/traits_special.out +++ b/charon/tests/ui/traits_special.out @@ -31,7 +31,7 @@ pub trait From parent_clause2 : [@TraitClause2]: Sized type Error fn from<[@TraitClause0]: Sized> = test_crate::From::from[Self, @TraitClause0_0] - non-dyn-compatible + vtable: test_crate::From::{vtable} } pub fn test_crate::From::from(@1: T) -> Result[@TraitClause1, @TraitClause0::parent_clause2] @@ -60,7 +60,7 @@ impl<'_0> From<&'_0 (bool)> for bool { parent_clause2 = Sized<()> type Error = () fn from = {impl From<&'_0 (bool)> for bool}::from<'_0> - non-dyn-compatible + vtable: {impl From<&'_0 (bool)> for bool}::{vtable}<'_0> } diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out index 21b93b932..85ebb175f 100644 --- a/charon/tests/ui/ullbc-control-flow.out +++ b/charon/tests/ui/ullbc-control-flow.out @@ -248,7 +248,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::ops::range::Range @@ -277,7 +277,7 @@ where parent_clause1 = @TraitClause0 type Item = A fn next<'_0> = {impl Iterator for Range[@TraitClause0]}::next<'_0_0, A>[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl Iterator for Range[@TraitClause0]}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::accum::Sum @@ -325,7 +325,7 @@ where type Item type IntoIter fn into_iter = core::iter::traits::collect::IntoIterator::into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -371,7 +371,7 @@ where type Item = @TraitClause1::Item type IntoIter = I fn into_iter = {impl IntoIterator for I}::into_iter[@TraitClause0, @TraitClause1] - non-dyn-compatible + vtable: {impl IntoIterator for I}::{vtable}[@TraitClause0, @TraitClause1] } // Full name: core::iter::traits::collect::Extend @@ -398,7 +398,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -411,7 +411,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } #[lang_item("next")] @@ -465,7 +465,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -477,7 +477,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -544,7 +544,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: test_crate::nested_loops_enum diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index 799f8b344..6f4a50c1c 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -265,7 +265,7 @@ pub trait Pointee parent_clause7 : [@TraitClause7]: Unpin parent_clause8 : [@TraitClause8]: Freeze type Metadata - non-dyn-compatible + vtable: core::ptr::metadata::Pointee::{vtable} } // Full name: core::ptr::null diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out index 8557d4755..53634e3fd 100644 --- a/charon/tests/ui/unsupported/issue-79-bound-regions.out +++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out @@ -126,7 +126,7 @@ pub trait Iterator parent_clause1 : [@TraitClause1]: Sized type Item fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::iterator::Iterator::{vtable} } // Full name: core::iter::traits::accum::Sum @@ -174,7 +174,7 @@ where type Item type IntoIter fn into_iter = into_iter[Self] - non-dyn-compatible + vtable: core::iter::traits::collect::IntoIterator::{vtable} } // Full name: core::iter::traits::collect::FromIterator @@ -226,7 +226,7 @@ pub trait DoubleEndedIterator parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator fn next_back<'_0> = next_back<'_0_0, Self>[Self] - non-dyn-compatible + vtable: core::iter::traits::double_ended::DoubleEndedIterator::{vtable} } // Full name: core::iter::traits::double_ended::DoubleEndedIterator::next_back @@ -239,7 +239,7 @@ pub trait ExactSizeIterator { parent_clause0 : [@TraitClause0]: MetaSized parent_clause1 : [@TraitClause1]: Iterator - non-dyn-compatible + vtable: core::iter::traits::exact_size::ExactSizeIterator::{vtable} } #[lang_item("next")] @@ -293,7 +293,7 @@ pub trait FnOnce parent_clause3 : [@TraitClause3]: Sized type Output fn call_once = call_once[Self] - non-dyn-compatible + vtable: core::ops::function::FnOnce::{vtable} } // Full name: core::ops::function::FnMut @@ -305,7 +305,7 @@ pub trait FnMut parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Tuple fn call_mut<'_0> = call_mut<'_0_0, Self, Args>[Self] - non-dyn-compatible + vtable: core::ops::function::FnMut::{vtable} } // Full name: core::ops::function::FnMut::call_mut @@ -372,7 +372,7 @@ where parent_clause2 : [@TraitClause2]: Sized parent_clause3 : [@TraitClause3]: Try type TryType - non-dyn-compatible + vtable: core::ops::try_trait::Residual::{vtable} } // Full name: core::slice::iter::Iter @@ -397,7 +397,7 @@ where parent_clause1 = Sized<&'_ (T)> type Item = &'a (T) fn next<'_0> = {impl Iterator for Iter<'a, T>[@TraitClause0]}::next<'a, '_0_0, T>[@TraitClause0] - non-dyn-compatible + vtable: {impl Iterator for Iter<'a, T>[@TraitClause0]}::{vtable}<'a, T>[@TraitClause0] } // Full name: core::slice::{Slice}::iter