Fix empty source code when verified function name is monomorphized

[zjp-CN]

Harness Name: convert::num::verify::check_f16_to_int_unchecked::f128::i128::check_float_to_int_unchecked
Verified Function: f128::<impl f128>::to_int_unchecked

[zjp-CN]

https://github.com/model-checking/verify-rust-std/blob/ca495357a162029276f9a4c7161bedc60e1b10c7/library/core/src/convert/num.rs#L819

    // Generate harnesses for `<Float as FloatToInt<Int>>::to_int_unchecked(self)`.
    macro_rules! generate_float_to_int_harness {
        ($Float:ty => $Int:ty, $harness:ident) => {
            #[kani::proof_for_contract(<$Float>::to_int_unchecked)]
            pub fn $harness() {
                let x: $Float = kani::any();
                let _: $Int = unsafe { x.to_int_unchecked() };
            }
        };
    }

    // float -> integer unchecked
    generate_float_to_int_harnesses!(
        check_f16_to_int_unchecked,
        (f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
        (f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
        (f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
        (f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
    );

Harness Name: convert::num::verify::check_f16_to_int_unchecked::f128::i128::check_float_to_int_unchecked
Verified Function: f128::<impl f128>::to_int_unchecked

There are multiple function names:

• #[kanitool::proof_for_contract = "< f16 > :: to_int_unchecked"] is specified in contract harness
• Unsure how the incomplete name would work in kani; need to check out https://model-checking.github.io/kani/reference/experimental/contracts.html or ask about this in kani repo
• f128::<impl f128>::to_int_unchecked is also incomplete due to missing last monomorphized <i128>
  • full name is f128::<impl f128>::to_int_unchecked::<i128>
  • Need to check out how the verified function name is collected in kani related tools