Warn when the CBMC on PATH does not match the pinned version

[ivmat]

Description

kani-dependencies pins a CBMC version, but the pin is only enforced at setup/CI time (install_deps.sh, kani-regression.sh). At runtime kani-driver uses whatever cbmc resolves from PATH with no check, so a locally installed CBMC can silently diverge from the pin while the user believes the pinned toolchain is in use. On a machine with several CBMC versions installed this is easy to hit and invisible when it happens — results get attributed to a toolchain that never ran.

This PR makes kani-driver resolve cbmc --version from PATH, compare it against the pin, and warn naming both versions when they differ. Design points:

• The pin is embedded at compile time (include_str! of kani-dependencies) rather than read at runtime: release bundles don't ship that file, so a runtime read would silently disable the check for exactly the users least able to audit their toolchain. rustc tracks the included file, so editing the pin still rebuilds.
• --version is handled explicitly (disable_version_flag) so kani --version / cargo kani --version actually run the check — clap's built-in flag exits during parsing, before any driver code runs. The first output line stays kani <version> / cargo-kani <version>, so scripts that parse it keep working; the CBMC lines are appended after it.
• For cargo kani, the version flag is detected on the raw arguments before project configuration is merged, so --version cannot be broken by a malformed Cargo.toml (matching the robustness of clap's built-in, whose version action previously fired inside cargo_locate_project's early parse). The scan matches whole arguments only and stops at -- or --cbmc-args; a post-parse fallback catches spellings the scan cannot see, such as -V clustered with other short flags. Known residual: a clustered -V combined with a malformed Cargo.toml reports the TOML error instead of the version — loudly, not silently.
• The warning is suppressed under --quiet during verification (preserving the zero-output contract in check-quiet.sh), but --version as an explicit query always reports.
• tools/build-kani bundling whichever cbmc is on the builder's PATH is the build-time analogue of the same problem; left as a follow-up to keep this focused. With this check, a mismatched bundle at least reports itself at runtime.

Manual testing

Unit tests cover the version parse/compare and the raw --version scan. Verified live both ways — a matching CBMC 6.10.0 is silent, a mismatched 6.8.0 fires naming both versions. Both script-based version regression tests (kani-version-flag-version, cargo-kani-version-flag-version) pass. cargo kani --version verified to work from a directory whose Cargo.toml is malformed, and a --version after --cbmc-args is forwarded to CBMC, not intercepted.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

@ivmat again, the code is massively over-narrated... version.rs is roughly half comments, and main.rs has 8-line rationale essays in front of 3-line blocks. This can be a real maintenance burden: prose comments drift from code, and this volume invites that. Let's cut them ~in half (keep the why for include_str!, --quiet, and the raw-scan; drop the paragraphs restating what the code plainly does).

[ivmat]

@feliperodri addressed the comments problem and the #4466 changes so this PR only covers CBMC pin check

[feliperodri]

Thanks @ivmat — this is a genuinely useful safety net, and I hit exactly this problem myself (a from-source CBMC on PATH silently diverging from the pin). The comment trimming from the last round looks great too.

I pushed two small cleanups directly to the branch to get it ready:

• Deduped the cbmc --version probe — get_cbmc_info now reuses version::cbmc_version_on_path instead of a second spawn + parse.
• Dropped the --version/malformed-Cargo.toml handling (and requests_version) to keep this focused on the pin check; that also removed the only merge conflict with main, so it's mergeable now.

Verified live end-to-end: a matching CBMC 6.10.0 is silent, a mismatched 6.8.0 prints the warning naming both versions, and --quiet stays silent. LGTM! 🚀