Span differs a lot and is not intuitive

[zjp-CN]

Both of stable_mir's Instance and rustc_middle's Instance points to a function, but the span doesn't point to the whole function in source code.

for item in stable_mir::all_local_items() {
    let inst = Instance::try_from(item).unwrap();

    let TyKind::RigidTy(RigidTy::FnDef(fn_def, _)) = inst.ty().kind() else {
        continue;
    };
    let span = fn_def.span();
    let src = functions::source_code(internal(tcx, span), &src_map);
    println!(" - {:?} ({:?}): {src} ({span:?})", item.name(), item.span());

    // or this:
    //let fn_defid = internal(tcx, inst).def_id();
    //let span = tcx.def_span(fn_defid);
    //let src = functions::source_code(span, &src_map);
    //println!(" - {:?} ({:?}): {src} ({span:?})", item.name(), item.span());
}

Telling from the output, stable item and rustc_middle instance point to the same location, but only limited to fn without body.

 - "verify::standard_proof" (Span { id: 13, repr: "tests/standard_proof.rs:4:5: 4:24" }): fn standard_proof() (tests/standard_proof.rs:4:5: 4:
24 (#0))
 - "verify::standard_proof_empty" (Span { id: 17, repr: "tests/standard_proof.rs:11:5: 11:30" }): fn standard_proof_empty() (tests/standard_pr
oof.rs:11:5: 11:30 (#0))
 - "verify::recursive_callees" (Span { id: 23, repr: "tests/standard_proof.rs:14:5: 14:27" }): fn recursive_callees() (tests/standard_proof.rs
:14:5: 14:27 (#0))
 - "top_level" (Span { id: 29, repr: "tests/standard_proof.rs:19:1: 19:19" }): pub fn top_level() (tests/standard_proof.rs:19:1: 19:19 (#0))
 - "m::func1" (Span { id: 37, repr: "tests/standard_proof.rs:24:5: 24:19" }): pub fn func1() (tests/standard_proof.rs:24:5: 24:19 (#0))

While hir body gives the span of whole fn including name and sigature (example).

[zjp-CN]

It turns out the whole function source code can be obtained from the span of fn_def.body():

for item in stable_mir::all_local_items() {
    let inst = Instance::try_from(item).unwrap();
    let TyKind::RigidTy(RigidTy::FnDef(fn_def, _)) = inst.ty().kind() else {
        continue;
    };
    let Some(body) = fn_def.body() else {
        continue;
    };
    let src_whole_fn = source_code_with(body.span, tcx, &src_map);
    println!(" - {:?} ({:?}): {src_whole_fn}", item.name(), item.span());
}

 - "verify::standard_proof" (Span { id: 13, repr: "tests/standard_proof.rs:4:5: 4:24" }): fn standard_proof() {
        let val: u8 = kani::any();
        assert_eq!(val, 1, "Not eq to 1.");
    }
 - "verify::standard_proof_empty" (Span { id: 17, repr: "tests/standard_proof.rs:11:5: 11:30" }): fn standard_proof_empty() {}
 - "verify::recursive_callees" (Span { id: 23, repr: "tests/standard_proof.rs:14:5: 14:27" }): fn recursive_callees() {
        crate::top_level();
    }
 - "top_level" (Span { id: 29, repr: "tests/standard_proof.rs:19:1: 19:19" }): pub fn top_level() {
    m::func1();
}
 - "m::func1" (Span { id: 37, repr: "tests/standard_proof.rs:24:5: 24:19" }): pub fn func1() {
        let _a = "".trim();
    }