Summary
Kani now emits two different names for the same function. kani list reports ptr::align_offset; the scanner's CSVs report core::ptr::align_offset. Anything that joins the two artifacts silently matches nothing.
Cause
rust-lang/rust#149401 changed CrateDef::name() to include the crate prefix. kani-compiler compensates — strip_local_crate_prefix in kani_middle/mod.rs:66 — so kani list is unaffected. tools/scanner calls item.name() / def.name() / fn_item.name() directly and inherited the prefix without anyone choosing it.
Impact
model-checking/verify-rust-std joins these two artifacts to compute contract coverage. Every *_under_contract metric there has read 0 since the divergence: core went from 313 unsafe functions under contract to 0 in a single run, with no change to the contracts themselves.
Suggested fix
Strip the prefix where the names are created, not per-CSV — the names reach at least five dump_csv calls (analysis.rs:84, 140, 167, 219, 230), so fixing one output would leave the others inconsistent.
The wrinkle is that strip_local_crate_prefix lives in kani-compiler and tools/scanner does not depend on it, so the helper needs extracting into a crate both can reach. Please don't hand-port it: the algorithm has a non-obvious rule distinguishing a crate-root qualifier (droppable) from a path continuation segment that merely shares the crate's name, and it must handle the prefix appearing inside a type qualifier such as <char as core::ascii::AsciiExt>::is_ascii. A second copy will drift.
Not urgent for verify-rust-std
They are landing a defensive shim on their side (model-checking/verify-rust-std#696), because they pin Kani by commit and need older pins to keep producing correct metrics. That shim is a no-op on already-stripped names, so it stays correct after this is fixed and does not need reverting. This issue is about Kani's own two outputs disagreeing, which will bite the next consumer that joins them.
@Tianshu-Huang offered to fix this on the Kani side in that PR — flagging for them.
Summary
Kani now emits two different names for the same function.
kani listreportsptr::align_offset; the scanner's CSVs reportcore::ptr::align_offset. Anything that joins the two artifacts silently matches nothing.Cause
rust-lang/rust#149401 changed
CrateDef::name()to include the crate prefix.kani-compilercompensates —strip_local_crate_prefixinkani_middle/mod.rs:66— sokani listis unaffected.tools/scannercallsitem.name()/def.name()/fn_item.name()directly and inherited the prefix without anyone choosing it.Impact
model-checking/verify-rust-std joins these two artifacts to compute contract coverage. Every
*_under_contractmetric there has read 0 since the divergence:corewent from 313 unsafe functions under contract to 0 in a single run, with no change to the contracts themselves.Suggested fix
Strip the prefix where the names are created, not per-CSV — the names reach at least five
dump_csvcalls (analysis.rs:84,140,167,219,230), so fixing one output would leave the others inconsistent.The wrinkle is that
strip_local_crate_prefixlives inkani-compilerandtools/scannerdoes not depend on it, so the helper needs extracting into a crate both can reach. Please don't hand-port it: the algorithm has a non-obvious rule distinguishing a crate-root qualifier (droppable) from a path continuation segment that merely shares the crate's name, and it must handle the prefix appearing inside a type qualifier such as<char as core::ascii::AsciiExt>::is_ascii. A second copy will drift.Not urgent for verify-rust-std
They are landing a defensive shim on their side (model-checking/verify-rust-std#696), because they pin Kani by commit and need older pins to keep producing correct metrics. That shim is a no-op on already-stripped names, so it stays correct after this is fixed and does not need reverting. This issue is about Kani's own two outputs disagreeing, which will bite the next consumer that joins them.
@Tianshu-Huang offered to fix this on the Kani side in that PR — flagging for them.