The LLBC backend names a method by appending the implementing type to its name, because the {impl} path element is dropped: test::getCounter for impl Counter { fn get() }, core::num::wrapping_addu8 for u8::wrapping_add, test::get_valA for impl T for A { fn get_val() }.
Charon's own translation keeps the impl in the path instead (PathElem::Impl(ImplElem::Ty(..)) / ImplElem::Trait(..)), which is what Aeneas and Charon's name matching expect — compute_short_names, for instance, looks for PathElem::Impl(ImplElem::Trait(..)) to shorten trait impl names.
Worth switching once the Charon bump (#4883) lands. It renames every method in the output, so it's better as its own change than folded into the bump. The name builder is defid_to_name / def_to_name in kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs (consolidated in #4882).
The LLBC backend names a method by appending the implementing type to its name, because the
{impl}path element is dropped:test::getCounterforimpl Counter { fn get() },core::num::wrapping_addu8foru8::wrapping_add,test::get_valAforimpl T for A { fn get_val() }.Charon's own translation keeps the impl in the path instead (
PathElem::Impl(ImplElem::Ty(..))/ImplElem::Trait(..)), which is what Aeneas and Charon's name matching expect —compute_short_names, for instance, looks forPathElem::Impl(ImplElem::Trait(..))to shorten trait impl names.Worth switching once the Charon bump (#4883) lands. It renames every method in the output, so it's better as its own change than folded into the bump. The name builder is
defid_to_name/def_to_nameinkani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs(consolidated in #4882).