@@ -92,16 +92,15 @@ impl<'tcx> GotocCtx<'tcx> {
9292 format ! ( "{}::global::{}::" , self . crate_name( ) , c)
9393 }
9494
95- /// For the vtable field name, we need exactly the dyn trait name and the function
96- /// name. The table itself already is scoped by the object type.
97- /// Example: ::Shape::vol
98- /// Note: this is _not_ the same name for top-level entry into the symbol table,
99- /// which does need more crate/type information and uses the full symbol_name(...)
100- pub fn vtable_field_name ( & self , def_id : DefId ) -> String {
101- // `to_string_no_crate_verbose` is from Rust proper, we use it here because it
102- // always includes the dyn trait name and function name.
103- // Tracking a less brittle solution here: https://github.com/model-checking/rmc/issues/187
104- self . tcx . def_path ( def_id) . to_string_no_crate_verbose ( )
95+ /// The name for the struct field on a vtable for a given function. Because generic
96+ /// functions can share the same name, we need to use the index of the entry in the
97+ /// vtable. This is the same index that will be passed in virtual function calls as
98+ /// InstanceDef::Virtual(def_id, idx). We could use solely the index as a key into
99+ /// the vtable struct, but we add the trait and function names for debugging
100+ /// readability.
101+ /// Example: 3_Shape::vol
102+ pub fn vtable_field_name ( & self , def_id : DefId , idx : usize ) -> String {
103+ format ! ( "{}_{}" , idx, with_no_trimmed_paths( || self . tcx. def_path_str( def_id) ) )
105104 }
106105
107106 /// A human readable name in Rust for reference, should not be used as a key.
0 commit comments