Summary
When running autoharness over a large target (the Rust standard library), the compiler logs (per crate):
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(SliceValidityAssume)
ERROR kani_compiler::kani_middle::kani_functions Failed to find `1` Kani functions
validate_kani_functions (kani-compiler/src/kani_middle/kani_functions.rs:359) emits this via tracing::error! but does not abort — it is non-fatal. The SliceValidityAssumeHook marker (kani::slice_validity_assume, library/kani/src/arbitrary.rs) simply isn't monomorphized into every crate being compiled.
Why file it anyway
It is misleading noise: it is logged at ERROR level, repeated once per crate, and reads like a fatal "failed to find" — but the build succeeds and verification proceeds normally. During the verify-rust-std nightly bump (PR model-checking/verify-rust-std#687) this obscured the real blocker (see companion issue for the autoharness E0080).
Ask
Either:
- downgrade to
debug/warn (or suppress) when the only missing entries are optional hooks not reachable in the current crate, or
- clarify the message so it is clearly non-fatal and names which crate/hook is affected.
Notes
SliceValidityAssume is not in the existing "optional model" allowlist (is_optional()), so it always counts toward missing. Confirmed non-fatal in a local autoharness run over the std library.
Summary
When running autoharness over a large target (the Rust standard library), the compiler logs (per crate):
validate_kani_functions(kani-compiler/src/kani_middle/kani_functions.rs:359) emits this viatracing::error!but does not abort — it is non-fatal. TheSliceValidityAssumeHookmarker (kani::slice_validity_assume,library/kani/src/arbitrary.rs) simply isn't monomorphized into every crate being compiled.Why file it anyway
It is misleading noise: it is logged at
ERRORlevel, repeated once per crate, and reads like a fatal "failed to find" — but the build succeeds and verification proceeds normally. During the verify-rust-std nightly bump (PR model-checking/verify-rust-std#687) this obscured the real blocker (see companion issue for the autoharness E0080).Ask
Either:
debug/warn(or suppress) when the only missing entries are optional hooks not reachable in the current crate, orNotes
SliceValidityAssumeis not in the existing "optional model" allowlist (is_optional()), so it always counts towardmissing. Confirmed non-fatal in a local autoharness run over the std library.