Kani scanner fails to detect harnesses that are gated behind #[cfg(kani)] #463
Description
I found the time of some harnesses exists in ubuntu-latest-results.json/results.json, but not in dv's UI
Then I noticed the crate is null in results.json for such harnesses who locate in #[cfg(kani)] modules. src file
{
"thread_id": 2,
"result": {
"harness": "time::duration_verify::duration_as_nanos_panics",
"is_autoharness": false,
"autoharness_result": null,
"with_contract": false,
"crate": null,
"function": "time::duration::as_nanos",
"function_safeness": null,
"public_target": null,
"file_name": "/home/runner/work/verify-rust-std/verify-rust-std/library/core/src/time.rs",
"n_failed_properties": 1,
"n_total_properties": 25,
"result": "SUCCESSFUL (encountered one or more panics as expected)",
"time": "0.075194955s",
"output": [
"Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime",
" File: \"/home/runner/work/verify-rust-std/verify-rust-std/library/core/src/option.rs\", line 2139, in option::expect_failed"
]
}
},The culprit is that kani's scan doesn't enable kani cfg in RUST_FLAGS to incoporate these harnesses in compilation:
verify-rust-std/scripts/kani-std-analysis/std-analysis.sh
Lines 80 to 87 in f66ba41